Formal Modeling And Verification Research Of Automatic Train Protection System

Complexity of software development has to be dealt with by dividing the different aspects and different views of the system and separating different concerns in the design. This implies the need of different modelling notations and tools to support more and more phases of the entire development process. To ensure the correctness of the models produced, the tools therefore need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensure high quality of such add-ins is to base them on sound formal foundations. Formal method is the basis to ensure strict specification, refinement and verification of model.Refinement Calculus of Object Systems (rCOS) is an extension of program refinement, which applies program refinement to the object oriented and component based model refinement process. The formal method rCOS can support refinement and verification techniques and tools in the component-based development process. Further,'automata-based formalism is widely used for interface specification and compatibility checking of components.After analyzing and studing rCOS method and the modeling and verification method for real-time system, this paper proposes an approach to model and verify the real-time system based on rCOS method and timed automata theory.At first, we extend rCOS profile with modelling element especially for time properties to Real-time Refinement Calculus of Object Systems (RT-rCOS), which improves the modelling ability of rCOS. Secondly, we introduce the concept of multi-Clock to timed automata and at the same time integrate required/provided interface of component in RT-rCOS development process to the state transitions where actions are expressed by the form of interface invoking, and thus we get Timed Execution Automata Model (TEAM). TEAM supports different type of Clock form, which enhances the ability of time properties specification of timed automata. Further, interface invoking on the state transition makes it pissible to transform RT-rCOS component modle to TEAM directly and thus verification tool can facilitate the analysis and verification of system properties. Finally, we apply above method to model and verify the Automatic Train Protection (ATP) system with the assistance of our modeling and verifcaion tool tMDA (Trustable Model Driven Architecture), which ensures the correctness and quality of ATP system。...