Incorporating Formal Methods and Measures Obtained through Analysis, Simulation Testing for Dependable Self-Adaptive Software in Avionics Systems

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 certification poses a unique set of problems, since these systems are required to be dependable. Also inherent is the subject of eliciting measures of adaptability which help evaluate the system in the context of non-functional requirements qualified by self-properties. We illustrate our approach for such a verification and evaluation exercise by proposing a combination of formal methods verification techniques and simulation based testing. The test bed is a representative self-adaptive software of a small UAS (Unmanned Aircraft System) avionics modeled as a multiagent BDI (Belief Desire Intention) system with evolutionary and reactive behaviours, illustrating important aspects of verification.