Dracos

Dracos

Formal Verification of a Distributed Railway Control System


This project is done for ELPRO LET Gmbh (a German company with approx. 1000 employees), which is responsible for the implementation of a distributed railway control system. The system is currently being tested in real operation on a local train route near Berlin. Our original goal was to verify the safety of a prototype made by ELPRO. However, we found that there were some problems with the design, and therefore we decided to extend our goal to also propose a better design. We are doing this using the RAISE formal method, which at the same time is being evaluated for its applicability. Our approach has been to start, prior to the requirement capture, with the construction of a domain model for railway systems. Right now we are doing a stepwise development and verification towards a design. We plan also to investigate how model checking can be combined with the RAISE method.

Participants:
JP Software-Consult (Jan Peleska)
Technical University of Denmark (Anne Haxthausen)

Maintained by Anne Haxthausen, ah@it.dtu.dk
Last update: March 25, 1997