CVFCS: Compositional Verification of Flight Critical Systems

Advanced capabilities planned for the next generation of aircraft and the Next Generation Air Transportation System (NextGen) will be based on complex new software. Integrated Modular Avionics (IMA) will enable the implementation of more functionality in software and tighter integration of these functions to improve aircraft efficiency. Aircraft will incorporate adaptive control algorithms that will provide enhanced safety and robustness in the presence of failures and adverse flight conditions. NextGen will encompass airborne and ground-based nodes with significant computational elements acting in coordination to maintain a safe and efficient airspace.

However, there are serious barriers to the deployment of these new capabilities. As these systems have grown in complexity, their verification has become the single most costly development activity. The verification costs of even more complex NextGen systems in the future will impact safety not just through an increasing incidence of errors and unforeseen interactions, but by delaying and preventing the deployment of crucial safety functions.

In this NASA-funded project we are addressing these challenges by developing a framework for compositional verification that will permit the verification of systems that exceed the complexity limits of current approaches. Our approach is based on:

  • Modeling the system architecture using the industry standard notations that engineers will be using
  • Developing a sophisticated translation framework that automates the translation of these models for analysis by powerful general purpose verification engines such as model checkers and theorem provers
  • Developing techniques for compositional verification based on the system architecture to divide the verification task into manageable, reusable pieces
This will significantly reduce verification costs by identifying and correcting system design errors early in the life cycle rather than waiting until system integration. We are validating this approach and the tools we develop on a realistic fault-tolerant flight control system model.

Our compositional approach exploits the verification effort and artifacts that are already part of typical software component verification work. We use formal assume-guarantee contracts that correspond to the requirements for each component. Each component in the system model is annotated with a contract that includes the requirements and constraints that were specified and verified as part of its development process. We then reason about the system-level behavior based on the interaction of the component contracts. This approach allows us to leverage existing development processes for software components and provides a scalable way to reason about the system as a whole.

Publications