LEADER 06214nam 22006855 450 001 996466126203316 005 20200630030417.0 010 $a3-540-68761-0 024 7 $a10.1007/11955757 035 $a(CKB)1000000000283752 035 $a(SSID)ssj0000316430 035 $a(PQKBManifestationID)11241384 035 $a(PQKBTitleCode)TC0000316430 035 $a(PQKBWorkID)10275512 035 $a(PQKB)10731751 035 $a(DE-He213)978-3-540-68761-0 035 $a(MiAaPQ)EBC3068532 035 $a(PPN)123140102 035 $a(EXLCZ)991000000000283752 100 $a20100301d2006 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aB 2007: Formal Specification and Development in B$b[electronic resource] $e7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings /$fedited by Jacques Julliand, Olga Kouchnarenko 205 $a1st ed. 2006. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2006. 215 $a1 online resource (XIII, 297 p.) 225 1 $aProgramming and Software Engineering ;$v4355 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-68760-2 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- E-Voting and the Need for Rigourous Software Engineering ? The Past, Present and Future -- Using B Machines for Model-Based Testing of Smartcard Software -- The Design of Spacecraft On-Board Software -- Regular Papers -- Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions -- Chorus Angelorum -- Augmenting B with Control Annotations -- Justifications for the Event-B Modelling Notation -- Automatic Translation from Combined B and CSP Specification to Java Programs -- Symmetry Reduction for B by Permutation Flooding -- Instantiation of Parameterized Data Structures for Model-Based Testing -- Verification of LTL on B Event Systems -- Patterns for B: Bridging Formal and Informal Development -- Time Constraint Patterns for Event B Development -- Modelling and Proof Analysis of Interrupt Driven Scheduling -- Refinement of Statemachines Using Event B Semantics -- Formal Transformation of Platform Independent Models into Platform Specific Models -- Refinement of eb 3 Process Patterns into B Specifications -- Security Policy Enforcement Through Refinement Process -- Integration of Security Policy into System Modeling -- Industrial Papers -- Experiences in Using B and UML in Industrial Development -- B in Large-Scale Projects: The Canarsie Line CBTC Experience -- A Tool for Firewall Administration -- The B-Method for the Construction of Microkernel-Based Systems -- Hardware Verification and Beyond: Using B at AWE -- Tool Papers -- A JAG Extension for Verifying LTL Properties on B Event Systems -- A Generic Flash-Based Animation Engine for ProB -- BE4: The B Extensible Eclipse Editing Environment -- BRAMA: A New Graphic Animation Tool for B Models -- LEIRIOS Test Generator: Automated Test Generation from B Models -- Meca: A Tool for Access Control Models -- JML2B: Checking JML Specifications with B Machines -- Invited Talk -- Plug-and-Play Nondeterminacy. 330 $aTheseproceedingsrecordthepaperspresentedattheSeventhInternationalC- ference of B Users (B 2007), held in the city of Besan¸ con in the east of France. This conference was built on the success of the previous six conferences in this series, B 1996, held at the University of Nantes, France; B 1998, held at the University of Montpellier, France; ZB 2000, held at the University of York, UK; ZB 2002, held at the University of Grenoble, France; ZB 2003, held at the U- versity of Turku, Finland; ZB 2005 held at the University of Surrey, Guildford, UK. B 2007 was held in January at the University of Franche-Comt´ e,Besan¸ con, France, hosted by the Computer Science Department (LIFC). LIFC has always placed particular emphasis on the applicability of its research and its relati- ship with industrial partners. In this context, it created in 2003 a company called LEIRIOS Technologies, which produces an automatic test generator tool (LTG) frommodels described in the B speci?cationlanguage. Other members of LIFC work on extensions of the B method for specifying and verifying dynamic properties. All the submitted papers in these proceedings were peer reviewed by at least three reviewers drawn from the B committee, depending on the subject matter of the paper. The authorsof the papersforB 2007werefrom Australia,Canada, Finland, Germany, France, Switzerland, and the UK. The conference featured a rangeof contributions by distinguished invited speakers drawn from both ind- try and academia. 410 0$aProgramming and Software Engineering ;$v4355 606 $aComputer programming 606 $aSoftware engineering 606 $aComputer logic 606 $aMathematical logic 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aComputer programming. 615 0$aSoftware engineering. 615 0$aComputer logic. 615 0$aMathematical logic. 615 14$aProgramming Techniques. 615 24$aSoftware Engineering. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 676 $a004.2/4 702 $aJulliand$b Jacques$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aKouchnarenko$b Olga$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational B Conference 906 $aBOOK 912 $a996466126203316 996 $aB 2007: Formal Specification and Development in B$9772071 997 $aUNISA