Article

Using b as a high level programming language in an industrial project: roissy VAL

Authors:

Frédéric Badeau,

Arnaud AmelotAuthors Info & Claims

ZB'05: Proceedings of the 4th international conference on Formal Specification and Development in Z and B

Pages 334 - 354

https://doi.org/10.1007/11415787_20

Published: 13 April 2005 Publication History

Publisher Site

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.

References

[1]

Abrial, J.-R., Extending B Without Changing it (for Developing Distributed Systems), 1996.

Google Scholar

[2]

Abrial, J.-R., The B-Book: Assigning Programs to Meanings, 1996.

Digital Library

Google Scholar

[3]

Behm P., Benoit P., Faivre A. and Meynadier J.-M., Météor: A Successful Application of B in a Large Project, 1999.

Google Scholar

[4]

Burdy L., Meynadier J.-M., Automatic Refinement; BUGM at FM'99, 1999.

Google Scholar

[5]

Dollé D., Essamé D., Falampin J., B dans le transport ferroviaire, l'expérience de Siemens, Technique et science informatiques - volume 22, 2003.

Google Scholar

[6]

Badeau F., B Language Reference Manual v1.8.5, 2002.

Google Scholar

Cited By

View all

ter Beek M(2024)Formal Methods and Tools Applied in the Railway DomainRigorous State-Based Methods10.1007/978-3-031-63790-2_1(3-21)Online publication date: 25-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-63790-2_1
Aït-Ameur YBogomolov SDupont GIliasov ARomanovsky AStankaitis P(2023)A Refinement-based Formal Development of Cyber-physical Railway Signalling SystemsFormal Aspects of Computing10.1145/352405235:1(1-1)Online publication date: 12-Jan-2023
https://dl.acm.org/doi/10.1145/3524052
Lutz SNeider DRoy R(2023)Specification Sketching for Linear Temporal LogicAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_2(26-48)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_2
Show More Cited By

Recommendations

Bypassing portability pitfalls of high-level low-level programming
VMIL '12: Proceedings of the sixth ACM workshop on Virtual machines and intermediate languages

Program portability is an important software engineering consideration. However, when high-level languages are extended to effectively implement system projects for software engineering gain and safety, portability is compromised--high-level code for ...
A high-level programming and command language

Unifying programming and command languages is a promising idea that has yet to be thoroughly exploited. Most attempts at such unification have used Lisp or traditional languages, such as Pascal. This paper describes the command and programming language ...
A high-level programming and command language
SIGPLAN '83: Proceedings of the 1983 ACM SIGPLAN symposium on Programming language issues in software systems

Unifying programming and command languages is a promising idea that has yet to be thoroughly exploited. Most attempts at such unification have used Lisp or traditional languages, such as Pascal. This paper describes the command and programming language ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ZB'05: Proceedings of the 4th international conference on Formal Specification and Development in Z and B

April 2005

493 pages

ISBN:3540255591

Editors:
Helen Treharne
Department of Computing, University of Surrey
,
Steve King
Department of Computer Science, University of York, Heslington, York, UK
,
Martin Henson
Department of Computer Science, University of Essex, Heslington, York, UK
,
Steve Schneider
Department of Computing, University of Surrey

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 13 April 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

ter Beek M(2024)Formal Methods and Tools Applied in the Railway DomainRigorous State-Based Methods10.1007/978-3-031-63790-2_1(3-21)Online publication date: 25-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-63790-2_1
Aït-Ameur YBogomolov SDupont GIliasov ARomanovsky AStankaitis P(2023)A Refinement-based Formal Development of Cyber-physical Railway Signalling SystemsFormal Aspects of Computing10.1145/352405235:1(1-1)Online publication date: 12-Jan-2023
https://dl.acm.org/doi/10.1145/3524052
Lutz SNeider DRoy R(2023)Specification Sketching for Linear Temporal LogicAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_2(26-48)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_2
Ferrari ABeek M(2022)Formal Methods in Railways: A Systematic Mapping StudyACM Computing Surveys10.1145/352048055:4(1-37)Online publication date: 21-Nov-2022
https://dl.acm.org/doi/10.1145/3520480
Dupont GAit-Ameur YSingh NPantel M(2021)Event-B HybridationACM Transactions on Embedded Computing Systems10.1145/344827020:4(1-37)Online publication date: 13-May-2021
https://dl.acm.org/doi/10.1145/3448270
(2018)Modelling, specifying and verifying self-adaptive systems instantiating MAPE patternsInternational Journal of Computer Applications in Technology10.1504/IJCAT.2018.09002957:1(28-44)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.1504/IJCAT.2018.090029
Mentré D(2016)SysML2BProceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 967510.1007/978-3-319-33600-8_26(308-311)Online publication date: 23-May-2016
https://dl.acm.org/doi/10.1007/978-3-319-33600-8_26
Hansen DSchneider DLeuschel M(2016)Using B and ProB for Data Validation ProjectsProceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 967510.1007/978-3-319-33600-8_10(167-182)Online publication date: 23-May-2016
https://dl.acm.org/doi/10.1007/978-3-319-33600-8_10
Bousse EMentré DCombemale BBaudry BKatsuragi T(2012)Aligning SysML with the B method to provide V&V for systems engineeringProceedings of the Workshop on Model-Driven Engineering, Verification and Validation10.1145/2427376.2427379(11-16)Online publication date: 1-Oct-2012
https://dl.acm.org/doi/10.1145/2427376.2427379
Kaur AGulati SSingh SMeghanathan NWozniak M(2012)A comparative study of two formal specification languagesProceedings of the Second International Conference on Computational Science, Engineering and Information Technology10.1145/2393216.2393304(524-531)Online publication date: 26-Oct-2012
https://dl.acm.org/doi/10.1145/2393216.2393304
Show More Cited By

Abstract

References

Cited By

Recommendations

Bypassing portability pitfalls of high-level low-level programming

A high-level programming and command language

A high-level programming and command language

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations