Model Checking: Cleared for Take Off

The increasing popularity of model-based development tools and the growing power of model checkers are making it practical to use formal methods for verification of avionics software. This paper describes a translator framework that enables model checking tools to be easily integrated into a model-based development environment to increase assurance, reduce cost, and satisfy certification objectives. In particular, we describe how formal methods can be used to satisfy certification objectives of DO-178C/ED-12C, the new guidance document for software aspects of certification for commercial aircraft.