DocumentCode :
2552287
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
fYear :
2006
fDate :
23-24 Dec. 2006
Firstpage :
438
Lastpage :
443
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Multitopic Conference, 2006. INMIC '06. IEEE
Conference_Location :
Islamabad
Print_ISBN :
1-4244-0795-8
Electronic_ISBN :
1-4244-0795-8
Type :
conf
DOI :
10.1109/INMIC.2006.358207
Filename :
4196450
Link To Document :
بازگشت