More Web Proxy on the site http://driver.im/

research-article

Formal verification of avionics self adaptive software: A case study

Authors:

Rajanikanth N. Kashi,

Meenakshi D'Souza,

S. Kumar Baghel,

Nitin KulkarniAuthors Info & Claims

ISEC '16: Proceedings of the 9th India Software Engineering Conference

Pages 163 - 169

https://doi.org/10.1145/2856636.2856658

Published: 18 February 2016 Publication History

Abstract

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.

References

[1]

DO-178B: Software Considerations in Airborne Systems and Equipment Certification, 1982.

[2]

RNAV-I (GNSS or DME/DME/IRU) SIDs and STARs, Chennai International, India, 2009.

[3]

DO-178C: Software Considerations in Airborne Systems and Equipment Certification, 2011.

[4]

Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. Boolean and cartesian abstraction for model checking C programs. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, pages 268--283, 2001.

Digital Library

[5]

Guillaume Brat, Doron Drusinsky, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser, and Rich Washington. Experimental evaluation of verification and validation tools on martian rover software. Formal Methods in System Design, 25(2-3):167--198, 2004.

Digital Library

[6]

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of LNCS, Copenhagen, Denmark, July 2002. Springer.

Digital Library

[7]

Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752--794, September 2003.

Digital Library

[8]

Mark d'Inverno, Michael Luck, Michael P. Georgeff, David Kinny, and Michael Wooldridge. The dMARS architecture: A specification of the distributed multi-agent reasoning system. Autonomous Agents and Multi-Agent Systems, 9(1-2):5--53, 2004.

Digital Library

[9]

Michael P. Georgeff, Barney Pell, Martha E. Pollack, Milind Tambe, and Michael Wooldridge. The belief-desire-intention model of agency. In Proceedings of the 5th International Workshop on Intelligent Agents V, Agent Theories, Architectures, and Languages, ATAL '98, pages 1--10, London, UK, UK, 1999. Springer-Verlag.

Digital Library

[10]

M. Usman Iftikhar and Danny Weyns. A case study on formal verification of self-adaptive behaviors in a decentralized system. In Proc. 11th Intl Workshop on Foundations for Co-ordination Languages and Self-Adaptation, volume 91 of EPTCS, 2012.

[11]

S. Jacklin, M. Lowry, J. Schumann, P. Gupta, J. Bosworth, E. Zavala, J. Kelly, K. Hayhurst, and C. Belcastro. Verification, validation, and certification challenges for adaptive flight control systems software. In Proceedings of the AIAA Guidance Navigation and Control Conference and Exhibit, 2004.

[12]

Jan Broersen John-Jules Ch. Meyer and Andreas Herzig. Handbook of Epistemic Logic. College Publications, 35 Ballards Lane, London N3 1XW, 2015.

[13]

Rajanikanth Kashi and Meenakshi D'Souza. Modeling avionics self-adaptive software as a BDI system, 2015.

[14]

Anand S. Rao and Michael P. Georgeff. BDI agents: From theory to practice. In Proceedings of the First International Conference on Multiagent Systems, June 12-14, 1995, San Francisco, California, USA, pages 312--319, 1995.

[15]

Mazeiar Salehie and Ladan Tahvildari. Self-adaptive software: Landscape and research challenges. ACM Trans. Auton. Adapt. Syst., 4(2):14:1--14:42, May 2009.

Digital Library

[16]

Uri Wilensky and William Rand. An Introduction to agent-based modeling: Modeling natural, social and engineered complex systems with Netlogo. MIT Press, 2015.

Digital Library

[17]

Michael Wooldridge. An Introduction to MultiAgent Systems. Wiley Publishing, 2nd edition, 2009.

Digital Library

[18]

Michael Wooldridge and PaulE. Dunne. The complexity of agent design problems: Determinism and history dependence. Annals of Mathematics and Artificial Intelligence, 45(3-4):343--371, 2005.

Digital Library

[19]

Karl Johan Åström and Richard M. Murray. Feedback systems: an introduction for scientists and engineers. Princeton university press, Princeton, Oxford, 2008.

Digital Library

Cited By

Deng PZhou QAn DWang SLi K(2022)A Modeling Method of Agents and SOA in Advanced Avionics System Based on AADLApplied Sciences10.3390/app1216815712:16(8157)Online publication date: 15-Aug-2022
https://doi.org/10.3390/app12168157
Kashi Nagaraj RD’Souza M(2021)A verifiable multi-agent framework for dependable and adaptable avionicsSādhanā10.1007/s12046-020-01538-446:1Online publication date: 4-Feb-2021
https://doi.org/10.1007/s12046-020-01538-4
Kashi RD'Souza M(2019)Mitigating Byzantine Failures in Multi-agent based Dependable and Adaptable Avionics Software2019 IEEE International Conference on Electrical, Computer and Communication Technologies (ICECCT)10.1109/ICECCT.2019.8869104(1-9)Online publication date: Feb-2019
https://doi.org/10.1109/ICECCT.2019.8869104
Show More Cited By

Formal verification of avionics self adaptive software: A case study
1. Computing methodologies
  1. Artificial intelligence
    1. Distributed artificial intelligence
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Incorporating Formal Methods and Measures Obtained through Analysis, Simulation Testing for Dependable Self-Adaptive Software in Avionics Systems
Compute '17: Proceedings of the 10th Annual ACM India Compute Conference

An Area 1rich with challenges is that of self-adaptive avionics software, with considerable thrust in both the American and European airspace modernization programs. Verifying functional requirements for such a system, ultimately leading to ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Coverage metrics for formal verification

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

ISEC '16: Proceedings of the 9th India Software Engineering Conference

February 2016

204 pages

ISBN:9781450340182

DOI:10.1145/2856636

General Chairs:
Santonu Sarkar
BITS Pilani, K.K. Birla Goa Campus
,
Ashish Sureka
ABB Corporate Research Center, India
,
Program Chairs:
Domenico Cotroneo
University of Naples
,
Nishant Sinha
IBM Research, India
,
Vibha S. Sinha
IBM Watson, Almaden Research Center, USA
,
Radhika Venkatasubramanyam
Siemens, Bangalore India
,
Padmaja Joshi
C-DAC, Mumbai
,
R. D. Naik
TCS
,
Pushpendra Singh
IIIT Delhi
,
Publications Chair:
Jayprakash Lalchandani
IIIT Bangalore

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

iSOFT: iSOFT
ACM India: ACM India

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 February 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

ISEC '16

ISEC '16: 9th India Software Engineering Conference

February 18 - 20, 2016

Goa, India

Acceptance Rates

ISEC '16 Paper Acceptance Rate 25 of 127 submissions, 20%;

Overall Acceptance Rate 76 of 315 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
200
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Deng PZhou QAn DWang SLi K(2022)A Modeling Method of Agents and SOA in Advanced Avionics System Based on AADLApplied Sciences10.3390/app1216815712:16(8157)Online publication date: 15-Aug-2022
https://doi.org/10.3390/app12168157
Kashi Nagaraj RD’Souza M(2021)A verifiable multi-agent framework for dependable and adaptable avionicsSādhanā10.1007/s12046-020-01538-446:1Online publication date: 4-Feb-2021
https://doi.org/10.1007/s12046-020-01538-4
Kashi RD'Souza M(2019)Mitigating Byzantine Failures in Multi-agent based Dependable and Adaptable Avionics Software2019 IEEE International Conference on Electrical, Computer and Communication Technologies (ICECCT)10.1109/ICECCT.2019.8869104(1-9)Online publication date: Feb-2019
https://doi.org/10.1109/ICECCT.2019.8869104
Mohalik SRamamurthy BJayaraman MD'Souza M(2018)Workshop on Developmental aspects of Intelligent Adaptive Systems (DIAS)ACM SIGSOFT Software Engineering Notes10.1145/3149485.314952142:4(25-27)Online publication date: 11-Jan-2018
https://dl.acm.org/doi/10.1145/3149485.3149521
D’Souza MKashi R(2018)Avionics Self-adaptive Software: Towards Formal Verification and ValidationDistributed Computing and Internet Technology10.1007/978-3-030-05366-6_1(3-23)Online publication date: 11-Dec-2018
https://doi.org/10.1007/978-3-030-05366-6_1
Kashi RD'Souza MKishore KChakraborty PGupta MDey LRoy S(2017)Incorporating Formal Methods and Measures Obtained through Analysis, Simulation Testing for Dependable Self-Adaptive Software in Avionics SystemsProceedings of the 10th Annual ACM India Compute Conference10.1145/3140107.3140128(137-142)Online publication date: 16-Nov-2017
https://dl.acm.org/doi/10.1145/3140107.3140128
Mohalik SD'Souza MJayaraman MGorthi RSarkar SMedvidovic NKulkarni VKumar AJoshi PInverardi PSureka ASharma R(2017)Developmental aspects of Intelligent Adaptive Systems (DIAS)Proceedings of the 10th Innovations in Software Engineering Conference10.1145/3021460.3021495(221-222)Online publication date: 5-Feb-2017
https://dl.acm.org/doi/10.1145/3021460.3021495
Kashi RD'Souza MBaghel SKulkarni N(2016)Incorporating adaptivity using learning in avionics self adaptive software: A case study2016 International Conference on Advances in Computing, Communications and Informatics (ICACCI)10.1109/ICACCI.2016.7732051(220-229)Online publication date: Sep-2016
https://doi.org/10.1109/ICACCI.2016.7732051

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents