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