Studying Formal Methods Applications in CBTC

Formal methods are mathematics-based techniques, often supported by reasoning tools, that can offer a rigorous and effective way to model, design and analyse computer systems. Up to now formal methods in railway systems have mostly been used for interlocking applications. We are interested in studying and describing some possible formal methods applications in CBTC (Communications-Based Train Control). The main goal is to meet the safety requirements of railway signalling systems by reasonable safety evidences. At a basic level, formal methods may simply be used for a high-level specification of the system to be designed (e.g., using the Z notation). The process of specification is the act of writing things down precisely. The main benefit in so doing is intangible gaining a deeper understanding of the system being specified. The next level of usage is to apply formal methods to the development process (e.g., VDM, SMV), using a set of rules or a design calculus that allows stepwise refinement of the operations and data structures in the specification to an efficiently executable program. We want to try modelling multi-tasking applications in real-time operating system of MCU (Micro Controlling Unit) in CBTC with Z notation, and the model will be analysed by exhaustive simulation with the SMV model checker. Besides, we select a feasible way to the verification of interlocking system. At the most rigorous level, the whole process of proof may be mechanized (e.g., B-tools). A major conclusion of the study is that formal methods, while still immature in certain important respects, are beginning to be used seriously and successfully by railway to design and develop safety-related systems.