Modeling and Verification of an Automatic Train Protection System

Advances in automatic control technologies have made society extremely dependent on control software used in train operation and many other applications. Consequently, the trust ability of control software is crucial. This has led to an increased emphasis on setting up a mechanism that can be used to guarantee the correctness of the models. In this paper, we proposed a process to integrate the modeling and verification techniques in Model Driven Architecture (MDA) and reported a successful application of the method to Automatic Train Protection (ATP) system. The ATP models are constructed and refined based on Refinement Calculus of Object Systems (rCOS). A modeling and verification trustable MDA tool is developed to facilitate the process.