Formal Verification of Integrated Modular Avionics (IMA) Health Monitoring using Timed Automata

被引:0
|
作者
Budiyanto, Ida Bagus [1 ]
Kistijantoro, Achmad Imam [2 ]
Trilaksono, Bambang Riyanto [2 ]
机构
[1] Politekn TEDC Bandung, Dept Informat, Cimahi, Indonesia
[2] Inst Teknol Bandung, Sch Elect Engn & Informat, Bandung, Indonesia
关键词
health monitor; IMA; timed automata; ARINC-653;
D O I
暂无
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Specifications of safety-critical real-time systems which are made with natural language has many disadvantages, such as contradictory, vague, ambiguous, and incomplete. The weakness in this specification will continue to the next stages, and will result the system failure. Formal methods allow the designer to determine the specifications of the system at different abstraction levels and verify the consistency of this formal specification before it is implemented. This study aimed to build and verify the formal specification of integrated modular avionics (IMA) health monitoring which use the ARINC-653 standard using a model checking timed automata. The verified results will help developers to define logic effective of fault-tolerance, so as to guarantee the IMA system can always available.
引用
收藏
页码:291 / 295
页数:5
相关论文
共 50 条
  • [1] Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE
    Wang, Lisong
    Chen, Miaofang
    Hu, Jun
    [J]. INTERNATIONAL JOURNAL OF AEROSPACE ENGINEERING, 2018, 2018
  • [2] CERTIFICATION CONCERNS OF INTEGRATED MODULAR AVIONICS (IMA) SYSTEMS
    Bartley, Gregg
    Lingberg, Barbara
    [J]. DASC: 2008 IEEE/AIAA 27TH DIGITAL AVIONICS SYSTEMS CONFERENCE, VOLS 1 AND 2, 2008, : 181 - +
  • [3] Formal Verification of Vessel Scheduling Using Probabilistic Timed Automata
    Thianpunyathanakul, Ratchanok
    Vatanawood, Wiwat
    [J]. PROCEEDINGS OF THE 20TH INTERNATIONAL CONFERENCE ON COMPUTING AND INFORMATION TECHNOLOGY, IC2IT 2024, 2024, 973 : 65 - 72
  • [4] ARINC 653 ROLE IN INTEGRATED MODULAR AVIONICS (IMA)
    Prisaznuk, Paul J.
    [J]. DASC: 2008 IEEE/AIAA 27TH DIGITAL AVIONICS SYSTEMS CONFERENCE, VOLS 1 AND 2, 2008, : 218 - 227
  • [5] Incremental Assurance of Multicore Integrated Modular Avionics (IMA)
    VanderLeest, Steven H.
    Matthews, David C.
    [J]. 2021 IEEE/AIAA 40TH DIGITAL AVIONICS SYSTEMS CONFERENCE (DASC), 2021,
  • [6] Testing Method of Integrated Modular Avionics Health Monitoring
    Zhang, Huinan
    Wang, Shihai
    Liu, Bin
    Diao, Xiaoxu
    [J]. 2013 PROGNOSTICS AND HEALTH MANAGEMENT CONFERENCE (PHM), 2013, 33 : 649 - 654
  • [7] Formal Verification of Business Processes as Timed Automata
    Mendoza Morales, Luis E.
    Monsalve, Carlos
    Villavicencio, Monica
    [J]. 2017 12TH IBERIAN CONFERENCE ON INFORMATION SYSTEMS AND TECHNOLOGIES (CISTI), 2017,
  • [8] Formal Verification of Sequence Diagram with State Invariants Using Timed Automata
    Thitareedechakul, Supapitch S.
    Vatanawood, Wiwat
    [J]. PROCEEDINGS OF THE 20TH INTERNATIONAL CONFERENCE ON COMPUTING AND INFORMATION TECHNOLOGY, IC2IT 2024, 2024, 973 : 43 - 54
  • [9] Business Process Verification using a Formal Compositional Approach and Timed Automata
    Mendoza Morales, Luis E.
    [J]. PROCEEDINGS OF THE 2013 XXXIX LATIN AMERICAN COMPUTING CONFERENCE (CLEI), 2013,
  • [10] Modular verification: Testing a subset of Integrated Modular Avionics in isolation
    Watkins, Christopher B.
    [J]. 2006 IEEE/AIAA 25TH DIGITAL AVIONICS SYSTEMS CONFERENCE, VOLS 1- 3, 2006, : 1228 - 1239