DocumentCode :
1150304
Title :
Formal specification and validation of railway network components using Z notation
Author :
Zafar, Nazir Ahmad
Author_Institution :
Dept. of Comput. & Inf. Sci., Pakistan Inst. of Eng. & Appl. Sci., Islamabad, Pakistan
Volume :
3
Issue :
4
fYear :
2009
fDate :
8/1/2009 12:00:00 AM
Firstpage :
312
Lastpage :
320
Abstract :
The railway interlocking system, being a safety-critical system, has achieved importance in the railway industry. Advanced technologies are being applied for its modelling, preventing collision and derailing of trains and at the same time allowing efficient movement of trains. In this study, we have applied Z notation by constructing a specification of the critical components of moving block interlocking. Graphs are used for modelling static components and are then integrated with Z to describe its entire state space. At first a real topology is transferred to a model topology in graph theory and then the critical components of the railway network, for example, tracks, switches, crossings and level crossing, are formalised. These components are integrated to define the static part of the system and then dynamic components, the state space of the static part, trains and controls, are integrated to describe the complete system. Formal specification of the system is given using Z and the model is analysed and validated using Z/EVES tool.
Keywords :
formal specification; graph theory; railway industry; railways; state-space methods; Z-notation; formal specification; formal validation; graph theory; model topology; railway industry; railway network component; safety-critical system; state space;
fLanguage :
English
Journal_Title :
Software, IET
Publisher :
iet
ISSN :
1751-8806
Type :
jour
DOI :
10.1049/iet-sen.2008.0082
Filename :
5174544
Link To Document :
بازگشت