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

Front Matter....Pages -
E-Voting and the Need for Rigourous Software Engineering – The Past, Present and Future....Pages 1-1
Using B Machines for Model-Based Testing of Smartcard Software....Pages 2-2
The Design of Spacecraft On-Board Software....Pages 3-3
Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions....Pages 4-18
Chorus Angelorum....Pages 19-33
Augmenting B with Control Annotations....Pages 34-48
Justifications for the Event-B Modelling Notation....Pages 49-63
Automatic Translation from Combined B and CSP Specification to Java Programs....Pages 64-78
Symmetry Reduction for B by Permutation Flooding....Pages 79-93
Instantiation of Parameterized Data Structures for Model-Based Testing....Pages 94-108
Verification of LTL on B Event Systems....Pages 109-124
Patterns for B: Bridging Formal and Informal Development....Pages 125-139
Time Constraint Patterns for Event B Development....Pages 140-154
Modelling and Proof Analysis of Interrupt Driven Scheduling....Pages 155-170
Refinement of Statemachines Using Event B Semantics....Pages 171-185
Formal Transformation of Platform Independent Models into Platform Specific Models....Pages 186-200
Refinement of eb 3 Process Patterns into B Specifications....Pages 201-215
Security Policy Enforcement Through Refinement Process....Pages 216-231
Integration of Security Policy into System Modeling....Pages 232-247
Experiences in Using B and UML in Industrial Development....Pages 248-251
B in Large-Scale Projects: The Canarsie Line CBTC Experience....Pages 252-254
A Tool for Firewall Administration....Pages 255-256
The B-Method for the Construction of Microkernel-Based Systems....Pages 257-259
Hardware Verification and Beyond: Using B at AWE....Pages 260-261
A JAG Extension for Verifying LTL Properties on B Event Systems....Pages 262-265
A Generic Flash-Based Animation Engine for ProB....Pages 266-269
BE 4 : The B Extensible Eclipse Editing Environment....Pages 270-273
BRAMA: A New Graphic Animation Tool for B Models....Pages 274-276
LEIRIOS Test Generator: Automated Test Generation from B Models....Pages 277-280
Meca: A Tool for Access Control Models....Pages 281-284
JML2B: Checking JML Specifications with B Machines....Pages 285-288
Plug-and-Play Nondeterminacy....Pages 289-292
Back Matter....Pages -