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
关键词
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 条
  • [21] Stepwise Formal Modeling and Verification of Self-Adaptive systems with Event-B. The Automatic Rover Protection case study
    Singh, Neeraj Kumar
    Ait-Ameur, Yamine
    Pantel, Marc
    Dieumegard, Arnaud
    Jenn, Eric
    2016 21ST INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2016), 2016, : 43 - 52
  • [22] Formal methods and finite element analysis of hurricane storm surge: A case study in software verification
    Baugh, John
    Altuntas, Alper
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 158 : 100 - 121
  • [23] A comparative study of formal verification techniques for software architecture specifications
    Tsai, JJP
    Xu, K
    ANNALS OF SOFTWARE ENGINEERING, 2000, 10 : 207 - 223
  • [24] Formal Design and Verification of Self-Adaptive Systems with Decentralized Control
    Arcaini, Paolo
    Riccobene, Elvinia
    Scandurra, Patrizia
    ACM TRANSACTIONS ON AUTONOMOUS AND ADAPTIVE SYSTEMS, 2017, 11 (04)
  • [25] Case study of the space shuttle cockpit avionics upgrade software
    Ferguson, Roscoe C.
    Thompson, Mrain C.
    IEEE AEROSPACE AND ELECTRONIC SYSTEMS MAGAZINE, 2006, 21 (08) : 3 - 8
  • [26] Applying formal proof techniques to avionics software: A pragmatic approach
    Randimbivololona, F
    Souyris, J
    Baudin, P
    Pacalet, A
    Raguideau, J
    Schoen, D
    FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1798 - 1815
  • [27] Self-Adaptive Software Needs Quantitative Verification at Runtime
    Calinescu, Radu
    Ghezzi, Carlo
    Kwiatkowska, Marta
    Mirandola, Raffaela
    COMMUNICATIONS OF THE ACM, 2012, 55 (09) : 69 - 77
  • [28] Formal Software Verification Measures Up
    Greengard, Samuel
    COMMUNICATIONS OF THE ACM, 2021, 64 (07) : 13 - 15
  • [29] Automatic formal verification of DSP software
    Currie, DW
    Hu, AJ
    Rajan, S
    Fujita, M
    37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 130 - 135
  • [30] What's formal software verification?
    Niculaescu, Oana
    XRDS: Crossroads, 2019, 25 (04): : 64 - 65