Keeping the trains and tracks in a safe state is important for railway systems, which include automated control. ATO-2000 is an automated railway system that plans, operates, monitors and controls a small railway network of driver-less trains within a mine. The formal specifications, design and implementation of Checker Function (CF), a software sub-system responsible for maintaining safety in ATO-2000 are described. CF is an important component in a safety-critical, real-time, distributed, mobile computing system. The formal specifications (in Z) of the core safety requirements in ATO-2000 are presented which include a new representation of the track topology. Some fault tolerance of the data received from the field is achieved through data validation constraints. Command safety constraints conservatively validate outgoing commands so that no possible future system state is unsafe. A simple approach used to integrate formal methods in the industrial software development process is discussed. The paper concludes with a review of the lessons learnt.
Safety checking in an automatic train operation system
Information and Software Technology ; 43 , 5 ; 325-338
2001
14 Seiten, 17 Quellen
Aufsatz (Zeitschrift)
Englisch
Europäisches Patentamt | 2023
|Europäisches Patentamt | 2024
|