Modeling and formal specification of automated train control system using Z notation

被引：0
|
作者：
Zafar, Nazir Ahmad [1 ]
机构：
[1] Pakistan Inst Engn & Appl Sci, Dept Informat & Comp Sci, Islamabad, Pakistan
来源：
10TH IEEE INTERNATIONAL MULTITOPIC CONFERENCE 2006, PROCEEDINGS | 2006年
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
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.
引用
收藏
页码：438 / +
页数：2
相关论文
共 50 条
  • [41] Formal verification of safety protocol in train control system
    Yan Zhang
    Tao Tang
    KePing Li
    Jose Manuel Mera
    Li Zhu
    Lin Zhao
    TianHua Xu
    Science China Technological Sciences, 2011, 54 : 3078 - 3090
  • [42] Automated Software Specification and Design Using the SOFL Formal Engineering Method
    Liu, Shaoying
    Xue, Xiang
    2009 WRI WORLD CONGRESS ON SOFTWARE ENGINEERING, VOL 4, PROCEEDINGS, 2009, : 283 - +
  • [43] Automated hardware synthesis from formal specification using SAT solvers
    Greaves, D
    15TH IEEE INTERNATIONAL WORKSHOP ON RAPID SYSTEM PROTOTYPING, PROCEEDINGS: SHORTENING THE PATH FROM SPECIFICATION TO PROTOTYPE, 2004, : 15 - 20
  • [44] Using Reo for formal specification and verification of system designs
    Razavi, Niloofar
    Sirjani, Marjan
    FOURTH ACM & IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2006, : 113 - +
  • [45] Formal specification of ADACOR holonic control system: Coordination models
    Leitao, Paulo
    Colombo, Armando W.
    Restivo, Francisco
    2005 44th IEEE Conference on Decision and Control & European Control Conference, Vols 1-8, 2005, : 2137 - 2142
  • [46] Formal specification and analysis of a control system based on computer networks
    Blum, I
    Juanole, G
    WFCS '97 - 1997 IEEE INTERNATIONAL WORKSHOP ON FACTORY COMMUNICATION SYSTEMS, PROCEEDINGS, 1997, : 297 - 305
  • [47] A Formal Framework for Stochastic Discrete Event System Specification Modeling and Simulation
    Castro, Rodrigo
    Kofman, Ernesto
    Wainer, Gabriel
    SIMULATION-TRANSACTIONS OF THE SOCIETY FOR MODELING AND SIMULATION INTERNATIONAL, 2010, 86 (10): : 587 - 611
  • [48] FORMAL SPECIFICATION METHODS AND NUMERICAL SOFTWARE - A CASE-STUDY USING Z
    LUCENA, CJP
    QIAN, YM
    UTILITAS MATHEMATICA, 1993, 44 : 85 - 114
  • [49] Formal Design and Validation of an Automatic Train Operation Control System
    Amendola, Arturo
    Barruffo, Lorenzo
    Bozzano, Marco
    Cimatti, Alessandro
    De Simone, Salvatore
    Fedeli, Eugenio
    Gabbasov, Artem
    Garrubba, Domenico Ernesto
    Girardi, Massimiliano
    Serra, Diana
    Tiella, Roberto
    Zampedri, Gianni
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2022, 2022, 13294 : 169 - 178
  • [50] European Train Control System: A Case Study in Formal Verification
    Platzer, Andre
    Quesel, Jan-David
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 246 - +
12345