Formal verification of avionics self adaptive software: A case study

被引：3
|
作者：
Kashi, Rajanikanth N. [1 ]
D'Souza, Meenakshi [2 ]
Baghel, S. Kumar [2 ]
Kulkarni, Nitin [2 ]
机构：
[1] Honeywell Technol Solut Labs, Bangalore, Karnataka, India
[2] IIIT Bangalore, Bangalore, Karnataka, India
来源：
PROCEEDINGS OF THE 9TH INDIA SOFTWARE ENGINEERING CONFERENCE | 2016年
关键词：
Avionics; self-adaptive software; BDI model; adaptive flight planning; model checking;
D O I：
10.1145/2856636.2856658
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We model avionics self-adaptive software as a multi-agent system using the BDI (Belief Desire Intention) model of agency. Such a model sufficiently represents several properties of avionics self-adaptive software. We illustrate formal verification of functional requirements related to safety of such software using Boolean predicate abstractions and model checking. Our proposed approach is illustrated using a case study involving BDI model of a flight management system with a proto-type involving appropriate tools.
引用
收藏
页码：163 / 169
页数：7
相关论文
共 50 条
  • [31] A Formal Verification Method for the SOPC Software
    Zhou, Shan
    Wang, Jinbo
    Jia, Jiao
    Zhang, Chi
    Wang, Ruixue
    IEEE TRANSACTIONS ON RELIABILITY, 2022, 71 (02) : 818 - 829
  • [32] Formal verification of automotive embedded software
    Todorov, Vassil
    Boulanger, Frederic
    Taha, Safouan
    2018 ACM/IEEE CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE 2018), 2018, : 84 - 87
  • [33] Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs
    Barnat, Jiri
    Beran, Jan
    Brim, Lubos
    Kratochvila, Tomas
    Rockai, Petr
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2012), 2012, 7437 : 78 - 92
  • [34] UML-Based modeling and formal verification for software self-adaptation
    Han, De-Shuai
    Yang, Qi-Liang
    Xing, Jian-Chun
    Ruan Jian Xue Bao/Journal of Software, 2015, 26 (04): : 730 - 746
  • [35] Formal Analysis of Architectural Policies of Self-Adaptive Software by Bigraph
    Chang, Zhiming
    Mao, Xinjun
    Qi, Zhichang
    PROCEEDINGS OF THE 9TH INTERNATIONAL CONFERENCE FOR YOUNG COMPUTER SCIENTISTS, VOLS 1-5, 2008, : 118 - 123
  • [36] A Case Study of Self-adaptive Software in the Dynamic Reconfiguration of IT Ecosystem
    Lee, Seungmin
    Park, Young B.
    Park, Soojin
    2016 INTERNATIONAL CONFERENCE ON BIG DATA AND SMART COMPUTING (BIGCOMP), 2016, : 513 - 516
  • [37] A Requirements Modelling Language to Facilitate Avionics Software Verification and Certification
    Paz, Andres
    El-Boussaidi, Ghizlane
    2019 IEEE/ACM 6TH INTERNATIONAL WORKSHOP ON REQUIREMENTS ENGINEERING AND TESTING (RET 2019), 2019, : 1 - 8
  • [38] Scaling Up Automated Verification: A Case Study and Formal-IDE for the Construction of High Integrity Software
    Welch, Daniel
    PROCEEDINGS OF THE 2017 ACM SIGCSE TECHNICAL SYMPOSIUM ON COMPUTER SCIENCE EDUCATION (SIGCSE'17), 2017, : 785 - 786
  • [39] End-to-End Formal Specification, Validation, and Verification Process: A Case Study of Space Flight Software
    Bergue Alves, Miriam C.
    Drusinsky, Doron
    Michael, James Bret
    Shing, Man-Tak
    IEEE SYSTEMS JOURNAL, 2013, 7 (04): : 632 - 641
  • [40] Verification support for ARINC-653-based avionics software
    de la Camara, Pedro
    Raul Castro, J.
    del Mar Gallardo, Maria
    Merino, Pedro
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2011, 21 (04): : 267 - 298
12345