Model checking intelligent avionics systems for test cases generation using multi-agent systems

Warda Elkholy, Mohamed El-Menshawy, Jamal Bentahar, Mounia Elqortobi, Amine Laarej, Rachida Dssouli

Research output: Contribution to journalArticlepeer-review

18 Scopus citations


The paper contributes by introducing a novel, formal and operational approach that addresses the open challenging issues of modeling, verifying, and testing intelligent critical avionics systems. We advance the state-of-the-art by unifying the three challenges and considering the intelligence, autonomy, and accountability of the components as first citizen concepts. The proposed methodology is effectively applied to a real, practical and complex case study of intelligent avionics systems, namely the landing gear system and uses multi-agent systems to model each main component in the system as an intelligent agent. We also introduce the formalism of extended interpreted systems that supports intelligence, autonomy, communication, input and output actions, predicate conditions and post-conditions. The paper adopts the computation tree logic of conditional commitments to model communication among autonomous agents and trace its progress. The symbolic model checker of this logic is used to run the verification of the system model, encoded in an extended input language, against coverage criteria and properties. Furthermore, we introduce a new testing methodology that: 1) Follows a test-driven development approach; 2) performs unit testing, component testing, and system testing in each increment; and 3) uses model checking to generate automatically counterexamples and witness traces interpreted into concrete test suites that achieve new coverage criteria. The experimental results showed the efficiency and scalability of the developed approach against a transformation-based technique. Finally, the computational complexity of the developed approach is analysed.

Original languageBritish English
Article number113458
JournalExpert Systems with Applications
StatePublished - 15 Oct 2020


  • Avionics
  • Commitments
  • Interpreted systems
  • MCMAS+
  • Model checking
  • Multi-agent systems
  • Test cases generation


Dive into the research topics of 'Model checking intelligent avionics systems for test cases generation using multi-agent systems'. Together they form a unique fingerprint.

Cite this