B 2007: Formal Specification and Development in B

1. Front Matter

   PDF

2. Invited Talks

   1. E-Voting and the Need for Rigourous Software Engineering – The Past, Present and Future

      • J. Paul Gibson

      Pages 1-1

   2. Using B Machines for Model-Based Testing of Smartcard Software

      • Eddie Jaffuel

      Pages 2-2

   3. The Design of Spacecraft On-Board Software

      • David Chemouil

      Pages 3-3

3. Regular Papers

   1. Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions

      • Sylvain Boulmé, Marie-Laure Potet

      Pages 4-18

   2. Chorus Angelorum

      • Steve Dunne

      Pages 19-33

   3. Augmenting B with Control Annotations

      • Wilson Ifill, Steve Schneider, Helen Treharne

      Pages 34-48

   4. Justifications for the Event-B Modelling Notation

      • Stefan Hallerstede

      Pages 49-63

   5. Automatic Translation from Combined B and CSP Specification to Java Programs

      • Letu Yang, Michael R. Poppleton

      Pages 64-78

   6. Symmetry Reduction for B by Permutation Flooding

      • Michael Leuschel, Michael Butler, Corinna Spermann, Edd Turner

      Pages 79-93

   7. Instantiation of Parameterized Data Structures for Model-Based Testing

      • Fabrice Bouquet, Jean-François Couchot, Frédéric Dadeau, Alain Giorgetti

      Pages 94-108

   8. Verification of LTL on B Event Systems

      • Julien Groslambert

      Pages 109-124

   9. Patterns for B: Bridging Formal and Informal Development

      • Edward Chan, Ken Robinson, Brett Welch

      Pages 125-139

   10. Time Constraint Patterns for Event B Development

       • Dominique Cansell, Dominique Méry, Joris Rehm

       Pages 140-154

   11. Modelling and Proof Analysis of Interrupt Driven Scheduling

       • Bill Stoddart, Dominique Cansell, Frank Zeyda

       Pages 155-170

   12. Refinement of Statemachines Using Event B Semantics

       • Colin Snook, Marina Waldén

       Pages 171-185

   13. Formal Transformation of Platform Independent Models into Platform Specific Models

       • Pontus Boström, Mats Neovius, Ian Oliver, Marina Waldén

       Pages 186-200

   14. Refinement of eb ³ Process Patterns into B Specifications

       • Frédéric Gervais, Marc Frappier, Régine Laleau

       Pages 201-215

   15. Security Policy Enforcement Through Refinement Process

       • Nicolas Stouls, Marie-Laure Potet

       Pages 216-231

   16. Integration of Security Policy into System Modeling

       • Nazim Benaïssa, Dominique Cansell, Dominique Méry

       Pages 232-247

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.

• Animation
• B method
• C#
• Eclipse
• Java
• Unified Modeling Language (UML)
• data structure
• formal software development
• formal specification
• formal verification
• model checkimg
• program analysis
• program development
• system modeling
• systems

• LIFC, Université de Franche-Comté, Besançon Cedex, France

  Jacques Julliand

• LIFC – TFC Team, Besançon

  Olga Kouchnarenko

Policies and ethics