This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Development and Verification of a Distributed Railway Control System
August 2000 (vol. 26 no. 8)
pp. 687-701

Abstract—In this article, we introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.

[1] D. Bjørner, C.W. George, B. Stig Hansen, H. Laustrup, and S. Prehn, “A Railway System, Coordination '97, Case Study Workshop Example,” Technical Report 93, United Nations University's Int'l Inst. for Software Technology, Macau, 1997.
[2] B. Dehbonei and F. Mejia, “Formal Development of Safety-Critical Software Systems in Railway Signalling,” Applications of Formal Methods, M.G. Hinchey and J.P. Bowen, eds., pp. 227–252, Prentice Hall, 1995.
[3] U. Oser, J. Arms, and H. Wegel, “FunkFahrBetrieb (FFB) Zum Wirtschaftlichen Einsatz auf Regionalstrecken,” Eisenbahntechnische Rundschau (ETR) vol. 46 Heft 6, pp. 323-331, 1997.
[4] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns. Addison Wesley, 1995.
[5] K. Mark Hansen, “Linking Safety Analysis to Safety Requirements—Exemplified by Railway Interlocking Systems,” PhD dissertation, Technical Univ. Denmark, Lyngby, Dept. of Information Tech nology, 1996.
[6] K. Mark Hansen, “Formalising Railway Interlocking Systems,” Proc. Second FMERail Workshop, Oct. 1998.
[7] A. Haxthausen and J. Peleska, “A Distributed Railway Control System–Selected Proofs,” Feb. 2000. http://www.it.dtu.dk/~ahDracos.
[8] J. Peleska and B. Buth, “Formal Methods for the International Space Station ISS,” Correct System Design. E.-R. Olderog, and B. Steffen, eds., pp. 363-389, 1999.
[9] J. Peleska, A. Baer, and A. Haxthausen, “Towards Domain-Specific Formal Specification Languages for Railway Control Systems,” Proc. Transportation Systems 2000, June, 2000.
[10] The RAISE Language Group, The RAISE Specification Language. The BCS Practitioners Series, Prentice Hall, 1992.
[11] The RAISE Method Group, The RAISE Development Method. The BCS Practitioners Series, Prentice Hall, 1995.
[12] N. Storey, Safety-Critical Computer Systems, Addison Wesley Longman, Reading, Mass., 1996.

Index Terms:
Safety, railways, distributed control system, formal specification, verification, stepwise refinement, RAISE.
Citation:
Anne E. Haxthausen, Jan Peleska, "Formal Development and Verification of a Distributed Railway Control System," IEEE Transactions on Software Engineering, vol. 26, no. 8, pp. 687-701, Aug. 2000, doi:10.1109/32.879808
Usage of this product signifies your acceptance of the Terms of Use.