Formal modeling, verification and implementation of a train control system

For complex system design, it can be very useful to use abstracted models to verify functionality, thereby reducing the number of potential bugs in the implementation phase. In this respect, model checking is a powerful technique for automatically determining whether a design (model) satisfies desired properties. Upon positive results, the design can then be implemented with limited risks of malfunction. In this paper, we show this by modeling a train control system for safe speed and acceleration limits and verifying the correctness of the model properties using the NuSMV model checker. Then, we implement the algorithm of the verified model on an ARM CortexM platform.