Title :
Modeling and Formal Specification of Automated Train Control System using Z Notation
Author :
Zafar, Nazir Ahmad
Author_Institution :
Dept. of Comput. & Inf. Sci., Pakistan Inst. of Eng. & Appl. Sci., Islamabad
Abstract :
In this paper, formal methods which are advanced software engineering techniques, in term of Z notation, are applied for the specification of critical components of automated train control system. At first graph theory is used for modeling of static components of the system and then integrated with Z notation to describe its entire state space. At first real topology is transferred to model topology in graph theory and then switches, crossings, and level crossing are formalized. At the end, these components are composed to define the entire interlocking system. Formal specification of the system is described in Z notation and the model is analyzed using Z/EVES tool.
Keywords :
formal specification; graph theory; locomotives; railway engineering; railway safety; railways; Z notation; advanced software engineering technique; automated train control system; formal methods; formal specification; graph theory; Automatic control; Control system synthesis; Formal specifications; Graph theory; Rail transportation; Railway safety; Software engineering; State-space methods; Switches; Topology;
Conference_Titel :
Multitopic Conference, 2006. INMIC '06. IEEE
Conference_Location :
Islamabad
Print_ISBN :
1-4244-0795-8
Electronic_ISBN :
1-4244-0795-8
DOI :
10.1109/INMIC.2006.358207