Skip to main content
SpringerLink
Log in

B 2007: Formal Specification and Development in B

7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings

  • Conference proceedings
  • © 2006

Overview

Editors:
  1. Jacques Julliand

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Olga Kouchnarenko

    1. LIFC – TFC Team, Besançon

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 4355)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Included in the following conference series:

Conference proceedings info: B 2007.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (32 papers)

  1. Front Matter

    Download chapter PDF

  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 3 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
Back to top

Keywords

About this book

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.

Editors and Affiliations

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

    Jacques Julliand

  • LIFC – TFC Team, Besançon

    Olga Kouchnarenko

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation