To search, Click below search items. |
| All Published Papers Search Service |
|
|
|
Title |
Formal Dynamic Operational Model of RIS Components |
|
Author |
Nazir Ahmad Zafar |
| Citation |
Vol. 11 No. 9 pp. 91-97 |
|
Abstract |
Primary objective of railway interlocking system is preventing trains from collision and derailing while at the same time allowing efficient and normal movement of trains. Railway interlocking system is a safety critical system and it needs a high practice of its modeling and development. Previous work of the author was on modeling of railway network components and safety analysis of the system. In this paper, we have applied Z notation to describe the operational model controlling the network's components based on their formal definitions. At first the critical components are described then state space is defined. Then components are refined and integrated to define the simplified system. The state space is enhanced by adding trains and controls to describe the entire system. Finally, formal dynamic model is proposed by defining critical local and global operations to guarantee safe and efficient operation of the system. The model is analyzed and validated using Z/Eves tool. |
|
Keywords |
Formal methods, Operational model, Railway interlocking, Z notation |
|
URL |
