Abstract
This chapter presents the modelling of a software controller in charge of managing the movements of trains on a track network. Some methodological aspects of this development are emphasized: the preliminary informal presentation of the requirements, the careful definition of a refinement strategy, the attention payed to the precise mathematical definition of the train network, and the modelling of a complete system including the external environment. A special attention is given to the prevention of errors and also (but to a less extend) to their tolerance. The modelling notation which is used in this presentation is Event-B.
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
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. In: Fundamentae Informatica ( to appear, 2006)
Abrial, J.-R., Cansell, D.: Click’n Prove: Interactive Proofs within Set Theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003)
Butler, M.: A System-based Approach to the Formal Development of Embedded Controllers for a Railway. In: Design Automation for Embedded Systems (2002)
Butler, M., Sekerinski, E., Sere, K.: An Action System Approach to the Steam Boiler Problem. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165. Springer, Heidelberg (1996)
Haxthausen, A.E., Peleska, J.: Formal Development and Verification of a Distributed Railway Control System. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, p. 1546. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Abrial, JR. (2006). Train Systems. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds) Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, vol 4157. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916246_1
Download citation
DOI: https://doi.org/10.1007/11916246_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48265-9
Online ISBN: 978-3-540-48267-3
eBook Packages: Computer ScienceComputer Science (R0)