Advertisement

Using B as a High Level Programming Language in an Industrial Project: Roissy VAL

  • Frédéric Badeau
  • Arnaud Amelot
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)

Abstract

In this article we would like to go back on B used to design software, by presenting the industrial process established through years by Siemens Transportation Systems on a real project: the VAL shuttle for Roissy Charles de Gaulle airport. In this project, the logical core of an equipment located along the tracks and driving the shuttles is designed with B.

By confronting this B software development, with the historical context, we show that B can be used as a high-level programming language offering the feature of proving properties. We show how this process is used to build, by construction, a large size software with very few design errors ever since its first release, and for a predefined cost.

Keywords

Abstract Model Concrete Model Read Operation Block Logic Abstract Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Abr96]
    Abrial, J.-R., Extending, B.: Without Changing it (for Developing Distributed Systems) (1996)Google Scholar
  2. [BBook96]
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings (1996)Google Scholar
  3. [Behm99]
    Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: A Successful Application of B in a Large Project (1999)Google Scholar
  4. [Burd99]
    Burdy, L., Meynadier, J.-M.: Automatic Refinement. In: BUGM at FM 1999 (1999)Google Scholar
  5. [Dol03]
    Dollé, D., Essamé, D., Falampin, J.: B dans le transport ferroviaire, l’expérience de Siemens. Technique et science informatiques 22 (2003)Google Scholar
  6. [MRefB02]
    Badeau, F.: B Language Reference Manual v1.8.5 (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Frédéric Badeau
    • 1
  • Arnaud Amelot
    • 2
  1. 1.ClearSy, Europarc de Pichaury bat. C1Aix-en-ProvenceFrance
  2. 2.Siemens Transportation SystemsMontrougeFrance

Personalised recommendations