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 条
  • [41] Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification
    Matichuk, Daniel
    Murray, Toby
    Andronick, June
    Jeffery, Ross
    Klein, Gerwin
    Staples, Mark
    2015 IEEE/ACM 37TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, VOL 1, 2015, : 722 - 732
  • [42] Formal Modelling and Verification of Real-Time Self-Adaptive Systems
    Cicirelli, Franco
    Nigro, Libero
    Pupo, Francesco
    2019 IEEE/ACM 23RD INTERNATIONAL SYMPOSIUM ON DISTRIBUTED SIMULATION AND REAL TIME APPLICATIONS (DS-RT), 2019, : 154 - 161
  • [43] From practical CASE to formal verification: Software engineering using Java']Java
    Clayton, PG
    Stiles, GS
    INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, PROCEEDINGS, 1999, : 81 - 87
  • [44] Timing Analysis of an Avionics Case Study on Complex Hardware/Software Platforms
    Wartel, Franck
    Kosmidis, Leonidas
    Gogonel, Adriana
    Baldovin, Andrea
    Stephenson, Zoe
    Triquet, Benoit
    Quinones, Eduardo
    Lo, Code
    Mezzetti, Enrico
    Broster, Ian
    Abella, Jaume
    Cucu-Grosjean, Liliana
    Vardanega, Tullio
    Cazorla, Francisco J.
    2015 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2015, : 397 - 402
  • [45] Lightweight Formal Verification in Real World, A Case Study
    Atzeni, Andrea
    Su, Tao
    Montanaro, Teodoro
    ADVANCED INFORMATION SYSTEMS ENGINEERING WORKSHOPS, 2014, 178 : 335 - 342
  • [46] Formal Verification of Health Assessment Tools: a Case Study
    Bezerra, Jonas Santos
    Costa, Andrei
    Ribeiro, Leila
    Cota, Erika
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2016, 324 : 31 - 47
  • [47] A case study: Formal verification of processor critical properties
    Zarpas, E
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 406 - 409
  • [48] Similarities and reuse of proofs in formal software verification
    Melis, E
    Schairer, A
    ADVANCES IN CASE-BASED REASONING, 1998, 1488 : 76 - 87
  • [49] Maintenance of formal software developments by stratified verification
    Autexier, S
    Hutter, D
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2002, 2514 : 36 - 52
  • [50] Formal Verification of Arithmetic Masking in Hardware and Software
    Gigerl, Barbara
    Primas, Robert
    Mangard, Stefan
    APPLIED CRYPTOGRAPHY AND NETWORK SECURITY, PT I, ACNS 2023, 2023, 13905 : 3 - 32
12345