Formal Verification of Double Two out of Two Computer Systems

摘要

The double two out of two safety computer system is widely used in China's rail transit. To enhance the safety integrity level of such a system, safety related logic is described and modelled by FSP (finite state process) language in a simple and explicit manner. A new method based on LTS (labelled transition system) model checking is proposed for verifying the system safety properties. The LTS method is adapted to model system behaviors by means of LTSA (labelled transition system analyzer) software. It visualizes overall activity traces and is easy for analysis and safety verification by developers. Simulation and verification results indicate that the LTS method provides great assistance for designers to develop more efficient and reliable complex systems.