B 2007: Besançon, France

Invited Talks

• J. Paul Gibson:
  E-Voting and the Need for Rigourous Software Engineering - The Past, Present and Future. 1
  
• Eddie Jaffuel:
  Using B Machines for Model-Based Testing of Smartcard Software. 2
  
• David Chemouil:
  The Design of Spacecraft On-Board Software. 3
  

Regular Papers

• Sylvain Boulmé, Marie-Laure Potet:
  Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions. 4-18
  
• Steve Dunne:
  Chorus Angelorum. 19-33
  
• Wilson Ifill, Steve A. Schneider, Helen Treharne:
  Augmenting B with Control Annotations. 34-48
  
• Stefan Hallerstede:
  Justifications for the Event-B Modelling Notation. 49-63
  
• Letu Yang, Michael Poppleton:
  Automatic Translation from Combined B and CSP Specification to Java Programs. 64-78
  
• Michael Leuschel, Michael J. Butler, Corinna Spermann, Edd Turner:
  Symmetry Reduction for B by Permutation Flooding. 79-93
  
• Fabrice Bouquet, Jean-François Couchot, Frédéric Dadeau, Alain Giorgetti:
  Instantiation of Parameterized Data Structures for Model-Based Testing. 94-108
  
• Julien Groslambert:
  Verification of LTL on B Event Systems. 109-124
  
• Edward Chan, Ken Robinson, Brett Welch:
  Patterns for B: Bridging Formal and Informal Development. 125-139
  
• Dominique Cansell, Dominique Méry, Joris Rehm:
  Time Constraint Patterns for Event B Development. 140-154
  
• Bill Stoddart, Dominique Cansell, Frank Zeyda:
  Modelling and Proof Analysis of Interrupt Driven Scheduling. 155-170
  
• Colin F. Snook, Marina A. Waldén:
  Refinement of Statemachines Using Event B Semantics. 171-185
  
• Pontus Boström, Mats Neovius, Ian Oliver, Marina A. Waldén:
  Formal Transformation of Platform Independent Models into Platform Specific Models. 186-200
  
• Frédéric Gervais, Marc Frappier, Régine Laleau:
  Refinement of eb³ Process Patterns into B Specifications. 201-215
  
• Nicolas Stouls, Marie-Laure Potet:
  Security Policy Enforcement Through Refinement Process. 216-231
  
• Nazim Benaïssa, Dominique Cansell, Dominique Méry:
  Integration of Security Policy into System Modeling. 232-247
  

Industrial Papers

• Ian Oliver:
  Experiences in Using B and UML in Industrial Development. 248-251
  
• Didier Essamé, Daniel Dollé:
  B in Large-Scale Projects: The Canarsie Line CBTC Experience. 252-254
  
• Mathieu Clabaut:
  A Tool for Firewall Administration. 255-256
  
• Sarah Hoffmann, Germain Haugou, Sophie Gabriele, Lilian Burdy:
  The B-Method for the Construction of Microkernel-Based Systems. 257-259
  
• Neil Evans, Wilson Ifill:
  Hardware Verification and Beyond: Using B at AWE. 260-261
  

Tool Papers

• Julien Groslambert:
  A. 262-265
  
• Jens Bendisposto, Michael Leuschel:
  A Generic Flash-Based Animation Engine for ProB. 266-269
  
• Jens Bendisposto, Michael Leuschel:
  BE⁴: The B Extensible Eclipse Editing Environment. 270-273
  
• Thierry Servat:
  BRAMA: A New Graphic Animation Tool for B Models. 274-276
  
• Eddie Jaffuel, Bruno Legeard:
  LEIRIOS Test Generator: Automated Test Generation from B Models. 277-280
  
• Amal Haddad:
  Meca: A Tool for Access Control Models. 281-284
  
• Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert:
  JML2B: Checking JML Specifications with B Machines. 285-288
  

Invited Talk

• Joseph M. Morris:
  Plug-and-Play Nondeterminacy. 289-292