Abstract
Usually, case studies dealing with train systems concentrate on the safety of trains circulating on tracks equipped with points and crossings and protected by means of traffic lights and speed limit sign postings as in [1,2,3]. Train drivers are supposed to follow such indications. The goal of formal approaches used in such case studies is to prove that trains may circulate safely on such tracks provided drivers act correctly. This is done by constructing models of such complex systems and by using formal proof techniques.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, Chap. 17. Cambridge University Press, Cambridge (2010)
Butler, M.: A system-based approach to the formal development of embedded controllers for a railway. Des. Autom. Embed. Syst. 6, 355–366 (2002)
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1546–1563. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48118-4_32
EEIG ERTMS Users Group: Hybrid ERTMS/ETCS Level 3: Principles, July 2017. Ref. 16E042 Version 1A
Hoang, T.S., Butler, M., Reichl, K.: The Hybrid ERTMS/ETCS Level 3 Case Study. ECS University of Southampton
To some (but not all) MAC readers: after loading this file, you may have to compress it (zip) before importation in the Rodin toolset. To all readers: after importing, it might be the case that some proof obligations are not discharged. In this case, click on ‘Proof Replay on Undischarged POs’ under ‘Proof Obligations’. http://users.ecs.soton.ac.uk/asf08r/ABZ_Case_2018
Acknowledgments
I would like to thank Asieh Salehi and Dominique Cansell for their help in preparing this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Abrial, JR. (2018). The ABZ-2018 Case Study with Event-B. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-91271-4_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91270-7
Online ISBN: 978-3-319-91271-4
eBook Packages: Computer ScienceComputer Science (R0)