Modeling of Train Control Systems Using Formal Techniques

摘要

Train control systems must guarantee a very high level of safety because their incorrect functioning may have very serious consequences such as loss of human life, large-scale environmental damages, or considerable economical penalties. The software reliability is related to several factors, such as completeness, consistency, and lack of ambiguity. Formal methods are widely recognized as fault avoidance techniques that can increase dependability by removing errors during the specification of requirements and during the design stages of development. In this chapter, a brief overview of existing results on formal specification of train control systems is first presented. Then we propose an integrated formal approach to specify train control systems; this integrated approach combines CSP and Object-Z with Clock theory to specify the Railway Control System concerning both the linear track and crossing area, especially the time delay between any two aspects of the railway system.