05933nam 22007215 450 991076750460332120251226195848.03-540-68761-010.1007/11955757(CKB)1000000000283752(SSID)ssj0000316430(PQKBManifestationID)11241384(PQKBTitleCode)TC0000316430(PQKBWorkID)10275512(PQKB)10731751(DE-He213)978-3-540-68761-0(MiAaPQ)EBC3068532(PPN)123140102(EXLCZ)99100000000028375220100301d2006 u| 0engurnn|008mamaatxtccrB 2007: Formal Specification and Development in B 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings /edited by Jacques Julliand, Olga Kouchnarenko1st ed. 2006.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2006.1 online resource (XIII, 297 p.) Programming and Software Engineering,2945-9168 ;4355Bibliographic Level Mode of Issuance: Monograph3-540-68760-2 Includes bibliographical references and index.Invited 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.TheseproceedingsrecordthepaperspresentedattheSeventhInternationalC- 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.Programming and Software Engineering,2945-9168 ;4355Computer programmingSoftware engineeringComputer scienceMachine theoryProgramming TechniquesSoftware EngineeringComputer Science Logic and Foundations of ProgrammingFormal Languages and Automata TheoryComputer programming.Software engineering.Computer science.Machine theory.Programming Techniques.Software Engineering.Computer Science Logic and Foundations of Programming.Formal Languages and Automata Theory.004.2/4Julliand Jacques1753929Kouchnarenko Olga1753930International B ConferenceMiAaPQMiAaPQMiAaPQBOOK9910767504603321B 2007: Formal Specification and Development in B4522527UNINA