Author(s)

F. Yan & T. Tang

Abstract

The safety of software is becoming increasingly important as computers pervade control systems on which human life depends. This has become more complex and in rail transportation fields and the methods to ensure its correctness have been slow in development. One feasible approach is to mathematically verify software design in such systems with Formal Methods. ATP (Automatic Train Protection) is a vital part of Train Control Systems. It assures safe train movement by a combination of train detection, separation of trains running on the same track or over interlocked routes, over speed prevention, and route interlocking. Obviously ATP is a safety-critical system and we regard it as a case study for our formal development methods. Firstly, the multi-tasks ATP onboard software model and state transitions will be modelled with UML; secondly, the timing model will be verified to meet the requirement of timing by SMV model checker; finally, the multi-tasking timing model will be realized with VxWorks (a real-time operating system by WindRiver). A major conclusion of the survey is that formal methods, while still immature in some respects, can be used successfully to assist in developing safety-critical systems. Keywords: safety critical system; Formal Methods; ATP; UML; SMV. 1 Introduction Nowadays, rail transportation is improving rapidly in China, and we need to assure that Train Control Systems meet safety requirements because they play an important role in the safety of the public. With the development of modern computer technology, it has become possible to protect against drivers' errors; the generic label for systems to do this is Automatic Train Protection (ATP).

Keywords

safety critical system; Formal Methods; ATP; UML; SMV.