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] Formal Modeling and Verification of the Functionality of Electronic Urban Railway Control Systems Through a Case Study [J].

Lukacs, Gabor ;

Bartha, Tamas .

URBAN RAIL TRANSIT, 2022, 8 (3-4) :217-245

[42] Formal Modeling and Verification of the Functionality of Electronic Urban Railway Control Systems Through a Case Study [J].

Gábor Lukács ;

Tamás Bartha .

Urban Rail Transit, 2022, 8 :217-245

[43] Study on formal modeling and verification of safety computer platform [J].

Wang, Xi ;

Ma, Lianchuan ;

Tang, Tao .

ADVANCES IN MECHANICAL ENGINEERING, 2016, 8 (05) :1-13

[44] Introduction to Self-Adaptive Software: Applications [J].

Laddaga, R ;

Robertson, P ;

Shrobe, H .

SELF-ADAPTIVE SOFTWARE: APPLICATIONS, 2001, 2614 :1-5

[45] A formal approach to adaptive software: continuous assurance of non-functional requirements [J].

Filieri, Antonio ;

Ghezzi, Carlo ;

Tamburrelli, Giordano .

FORMAL ASPECTS OF COMPUTING, 2012, 24 (02) :163-186

[46] Bridging the gap between formal verification and schedulability analysis: The case of robotics [J].

Foughali, Mohammed ;

Hladik, Pierre-Emmanuel .

JOURNAL OF SYSTEMS ARCHITECTURE, 2020, 111

[47] Towards Formal Verification of Smart Grid Distributed Intelligence: FREEDM case [J].

Patil, Sandeep ;

Zhabelova, Gulnara ;

Vyatkin, Valeriy ;

McMillin, Bruce .

IECON 2015 - 41ST ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2015, :3974-3979

[48] Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499 [J].

Lilli, Giordano ;

Xavier, Midhun ;

Le Priol, Etienne ;

Perret, Vincent ;

Liakh, Tatiana ;

Oboe, Roberto ;

Vyatkin, Valeriy .

IEEE OPEN JOURNAL OF THE INDUSTRIAL ELECTRONICS SOCIETY, 2023, 4 :417-431

[49] A Domain Model for Self-Adaptive Software Systems [J].

Moghaddam, Fahimeh Alizadeh ;

Deckers, Robert ;

Procaccianti, Giuseppe ;

Grosso, Paola ;

Lago, Patricia .

11TH EUROPEAN CONFERENCE ON SOFTWARE ARCHITECTURE (ECSA 2017) - COMPANION VOLUME, 2017, :23-29

[50] Self-Adaptive Software: Landscape and Research Challenges [J].

Salehie, Mazeiar ;

Tahvildari, Ladan .

ACM TRANSACTIONS ON AUTONOMOUS AND ADAPTIVE SYSTEMS, 2009, 4 (02)

← 1 2 3 4 5 →