LEADER 05933nam 22007215 450 001 9910767504603321 005 20251226195848.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 $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,$x2945-9168 ;$v4355 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$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,$x2945-9168 ;$v4355 606 $aComputer programming 606 $aSoftware engineering 606 $aComputer science 606 $aMachine theory 606 $aProgramming Techniques 606 $aSoftware Engineering 606 $aComputer Science Logic and Foundations of Programming 606 $aFormal Languages and Automata Theory 615 0$aComputer programming. 615 0$aSoftware engineering. 615 0$aComputer science. 615 0$aMachine theory. 615 14$aProgramming Techniques. 615 24$aSoftware Engineering. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aFormal Languages and Automata Theory. 676 $a004.2/4 701 $aJulliand$b Jacques$01753929 701 $aKouchnarenko$b Olga$01753930 712 12$aInternational B Conference 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910767504603321 996 $aB 2007: Formal Specification and Development in B$94522527 997 $aUNINA