B 2007: Formal Specification and Development in B 7th International Conference of B Users, Besançon, France, January 17-19, 2007. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Julliand, Jacques (Επιμελητής έκδοσης), Kouchnarenko, Olga (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2006.
• Σειρά: Lecture Notes in Computer Science, 4355
• Θέματα: Computer science.; Computer programming.; Software engineering.; Computer logic.; Mathematical logic.; Computer Science.; Programming Techniques.; Software Engineering.; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.

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, he...

Πίνακας περιεχομένων:

• 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.