Search

• We propose a formal approach to model, verify and test avionics systems. • We use intelligent agents to model the components of the landing gear system. • We introduce extended interpreted systems to reason about interactions and actions. • We introduce a testing methodology that follows a test-driven development approach. • We use MCMAS+ to generate traces for test suites achieving new coverage criteria. 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. [ABSTRACT FROM AUTHOR]