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 feature-based classification of formal verification techniques for software models
    Sebastian Gabmeyer
    Petra Kaufmann
    Martina Seidl
    Martin Gogolla
    Gerti Kappel
    Software & Systems Modeling, 2019, 18 : 473 - 498
  • [32] A feature-based classification of formal verification techniques for software models
    Gabmeyer, Sebastian
    Kaufmann, Petra
    Seidl, Martina
    Gogolla, Martin
    Kappel, Gerti
    SOFTWARE AND SYSTEMS MODELING, 2019, 18 (01) : 473 - 498
  • [33] Hardware/Software co-design of an avionics communication protocol interface system:: an industrial case study
    Clouté, F
    Contensou, JN
    Esteve, D
    Pampagnin, P
    Pons, P
    Favard, Y
    PROCEEDINGS OF THE SEVENTH INTERNATIONAL WORKSHOP ON HARDWARE/SOFTWARE CODESIGN (CODES'99), 1999, : 48 - 52
  • [34] Formal verification of software-based medical devices considering medical guidelines
    Daw, Zamira
    Cleaveland, Rance
    Vetter, Marcus
    INTERNATIONAL JOURNAL OF COMPUTER ASSISTED RADIOLOGY AND SURGERY, 2014, 9 (01) : 145 - 153
  • [35] An Outline Workflow for Practical Formal Verification from Software Requirements to Object Code
    Sexton, Darren
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2013, 8187 : 32 - 47
  • [36] Formal verification of software-based medical devices considering medical guidelines
    Zamira Daw
    Rance Cleaveland
    Marcus Vetter
    International Journal of Computer Assisted Radiology and Surgery, 2014, 9 : 145 - 153
  • [37] Formal verification of software-only mechanisms for live migration of SGX enclaves
    Demigha, Oualid
    Haddad, Nabil
    INTERNATIONAL JOURNAL OF INFORMATION AND COMPUTER SECURITY, 2023, 22 (02) : 230 - 261
  • [38] Formal Verification With Confidence Intervals to Establish Quality of Service Properties of Software Systems
    Calinescu, Radu
    Ghezzi, Carlo
    Johnson, Kenneth
    Pezze, Mauro
    Rafiq, Yasmin
    Tamburrelli, Giordano
    IEEE TRANSACTIONS ON RELIABILITY, 2016, 65 (01) : 107 - 125
  • [39] Formal Verification of Python']Python Software Transactional Memory Based on Timed Automata
    Kordic, Branislav
    Popovic, Miroslav
    Ghilezan, Silvia
    ACTA POLYTECHNICA HUNGARICA, 2019, 16 (07) : 197 - 216
  • [40] Towards the Formal Development of Software Based Systems: Access Control System as a Case Study
    Boucherit, Ammar
    Castro, Laura M.
    Khababa, Abdallah
    Hasan, Osman
    INFORMATION TECHNOLOGY AND CONTROL, 2018, 47 (03): : 393 - 405
12345