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 条
  • [1] Avionics Self-adaptive Software: Towards Formal Verification and Validation
    D'Souza, Meenakshi
    Kashi, Rajanikanth N.
    DISTRIBUTED COMPUTING AND INTERNET TECHNOLOGY, ICDCIT 2019, 2019, 11319 : 3 - 23
  • [2] Formal Verification of Avionics Software Products
    Souyris, Jean
    Wiels, Virginie
    Delmas, David
    Delseny, Herve
    FM 2009: FORMAL METHODS, PROCEEDINGS, 2009, 5850 : 532 - +
  • [3] Incorporating Adaptivity using Learning in Avionics Self Adaptive Software: A Case Study
    Kashi, Rajanikanth N.
    D'Souza, Meenakshi
    Baghel, S. Kumar
    Kulkami, Nitin
    2016 INTERNATIONAL CONFERENCE ON ADVANCES IN COMPUTING, COMMUNICATIONS AND INFORMATICS (ICACCI), 2016, : 220 - 229
  • [4] Formal verification of control software: A case study
    Griesmayer, A
    Bloem, R
    Hautzendorfer, M
    Wotawa, F
    INNOVATIONS IN APPLIED ARTIFICIAL INTELLIGENCE, 2005, 3533 : 783 - 788
  • [5] A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System
    Iftikhar, M. Usman
    Weyns, Danny
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (91): : 45 - 62
  • [6] Formal verification of overhead accounting in an avionics RTOS
    Cofer, D
    Rangarajan, M
    23RD IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2002, : 181 - 190
  • [7] Orientations in verification engineering of avionics software
    Randimbivololona, F
    INFORMATICS - 10 YEARS BACK, 10 YEARS AHEAD, 2001, 2000 : 131 - 137
  • [8] Towards Formal Verification for Cyber-physically Agnostic Software: a Case Study
    Drozdov, Dmitrii
    Patil, Sandeep
    Dubinin, Victor
    Vyatkin, Valeriy
    IECON 2017 - 43RD ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2017, : 5509 - 5514
  • [9] Formal Verification With Frama-C: A Case Study in the Space Software Domain
    Busquim e Silva, Rovedy Aparecida
    Arai, Nanci Naomi
    Burgareli, Luciana Akemi
    Parente de Oliveira, Jose Maria
    Pinto, Jorge Sousa
    IEEE TRANSACTIONS ON RELIABILITY, 2016, 65 (03) : 1163 - 1179
  • [10] Incorporating Formal Methods and Measures Obtained through Analysis, Simulation Testing for Dependable Self-Adaptive Software in Avionics Systems
    Kashi, Rajanikanth N.
    D'Souza, Meenakshi
    Kishore, Koyalkar Raman
    COMPUTE'17: PROCEEDINGS OF THE 10TH ANNUAL ACM INDIA COMPUTE CONFERENCE, 2017, : 137 - 142
12345