Avionics Self-adaptive Software: Towards Formal Verification and Validation

  • Meenakshi D’SouzaEmail author
  • Rajanikanth N. Kashi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11319)


One of the future trends in the aerospace industry for ground and air operations is to make aircrafts self-adaptive, enabling them to take decisions without relying on any control authority. We propose a Belief, Desire, Intention (BDI) based multi-agent system for modelling avionics Self-Adaptive Software (SAS). Our BDI models are formally specified using Z notation and include a library of learning algorithms to cater to adaptability. Apart from satisfying various self-* properties that define adaptability features, avionics SAS, being safety critical systems, also have to satisfy safety and provide deterministic response meeting real-time constraints. We propose a validation framework to check for self-* properties. We also present a formal verification framework based on abstractions and model checking for verifying safety properties. The framework is illustrated through an avionics case study involving an adaptive flight planning system.


  1. 1.
    Helle, P., Strobel, C., Schamai, W.: Testing of autonomous systems - challenges and current state-of-the-art. In: Proceedings of 26th Annual INCOSE International Symposium (IS 2016), Winter Simulation Conference, pp. 150–158 (2016)Google Scholar
  2. 2.
    Goodloe, A.: Challenges in the verification of flight-critical systems. In: CPS V&V I & F Workshop 2014-Talks. National Science Foundation (2014)Google Scholar
  3. 3.
    Adam, C., Gaudou, B.: BDI agents in social simulations: a survey. Knowl. Eng. Rev. 31(3), 207–238 (2016)CrossRefGoogle Scholar
  4. 4.
    Müller, J.P., Fischer, K.: Application impact of multi-agent systems and technologies: a survey. In: Shehory, O., Sturm, A. (eds.) Agent-Oriented Software Engineering, pp. 27–53. Springer, Heidelberg (2014). Scholar
  5. 5.
    Salehie, M., Tahvildari, L.: Self-adaptive software: landscape and research challenges. ACM Trans. Auton. Adapt. Syst. 4(2), 14:1–14:42 (2009)CrossRefGoogle Scholar
  6. 6.
    Roadmap for intelligent systems in aerospace. American Institute of Aeronautics and Astronautics (AIAA), pp. 1–111 (2016)Google Scholar
  7. 7.
    RTCA DO-178B: Software Considerations in Airborne Systems and Equipment Certification (1992)Google Scholar
  8. 8.
    RTCA DO-178C: Software Considerations in Airborne Systems and Equipment Certification (2011)Google Scholar
  9. 9.
    RTCA DO-333: Formal Methods Supplement to DO-178C and DO-278A (2011)Google Scholar
  10. 10.
    Cofer, D., Miller, S.: DO-333 certification case studies. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 1–15. Springer, Cham (2014). Scholar
  11. 11.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  12. 12.
    Kashi, R.N., D’Souza, M.: VERMILLION: Verifiable MultIagent Framework for DependabLe and AdaptabLe AvIONics (2018, submitted)Google Scholar
  13. 13.
    NetLogo: A multi-agent programmable modelling environment.
  14. 14.
    Rao, A.S., George, A.P.: BDI agents: from theory to practice. Technical Note 56, Australian Artificial Intelligence Institute (1995)Google Scholar
  15. 15.
    D’Inverno, M., Luck, M., George, M., Kinny, D., Wooldridge, M.: The dMARS architecture: a specification of the distributed multiagent reasoning system. Auton. Agents Multi-Agent Syst. 9(1–2), 5–53 (2004)CrossRefGoogle Scholar
  16. 16.
    Wooldridge, M.: An Introduction to MultiAgent Systems, 2nd edn. Wiley, Hoboken (2009)Google Scholar
  17. 17.
    Davies, J., Woodcock, J.: Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall, Upper Saddle River (1996)zbMATHGoogle Scholar
  18. 18.
    Siewiorek, D.P., Narasimhan, P.: Fault-tolerant architectures for space and avionics.
  19. 19.
    Sutton, R.S., Barto, A.G.: Temporal difference learning. In: Reinforcement Learning: An Introduction, chap. 6. MIT Press (2005)Google Scholar
  20. 20.
    Kashi, R.N., D’Souza, M., Baghel, S.K., Kulkarni, N.: Formal verification of avionics self-adaptive software: a case study. In: Proceedings of ACM ISEC, pp. 163–169 (2016)Google Scholar
  21. 21.
    Kashi, R.N., D’Souza, M., Baghel, S.K., Kulkarni, N.: Incorporating adaptivity using learning in avionics self adaptive software: a case study. In: Proceedings of IEEE ICACCI 2016, pp. 220–229 (2016)Google Scholar
  22. 22.
    Kashi, R.N., D’Souza, M., Kishore, K.R.: Incorporating formal methods and measures obtained through analysis, simulation testing for dependable self-adaptive software in avionics systems. In: Proceedings of 10th ACM Compute (2017)Google Scholar
  23. 23.
    NuSMV: A symbolic model checker.
  24. 24.
    Webster, M., Cameron, N., Fisher, M., Jump, M.: Generating certification evidence for autonomous unmanned aircraft using model checking and simulation. J. Aerosp. Inf. Syst. 11(5), 258–279 (2014)Google Scholar
  25. 25.
    Georgeff, M., Ingrand, F.: Monitoring and control of spacecraft systems using procedural reasoning (1989)Google Scholar
  26. 26.
    Ljungberg, M., Lucas, A.: The OASIS air traffic management system (1992)Google Scholar
  27. 27.
    Dennis, L.A., Farwer, B.: Gwendolen: a BDI language for verifiable agents. In: Löwe, B. (ed.) Logic and the Simulation of Interaction and Reasoning, AISB 2008 Workshop (2008)Google Scholar
  28. 28.
    Raimondi, F.: Case study description: avionic scenario. Dagstuhl Reports, vol. 3, pp. 180–184 (2013)Google Scholar
  29. 29.
    Whalen, M., et al.: ADGS-2100 adaptive display & guidance system window manager analysis. Technical report, NASA.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.International Institute of Information Technology, BangaloreBangaloreIndia
  2. 2.Dayananda Sagar UniversityBangaloreIndia

Personalised recommendations