University of Minnesota
Software Engineering Center

You are here

Darren Cofer

Recent Publications

Software Model Checking for Avionics SSoftware MSoftware Model Checking for Avionics SSoftware Model Checking for Avionics Systemsystemsodel Checking for Avionics Systemsystems

The adoption of model-based development tools is changing the cost-benefit equation for the industrial use of formal methods. The integration of formal methods such as model checking into software development environments makes it possible to fight increasing cost and complexity with automation and rigor. This paper describes how formal analysis tools can be inserted into a model-based development process to decrease costs and increase quality of safety-critical avionics software.

Integration of Formal Analysis into a Model-Based Software Development Process

The next generation of military aerospace systems will include advanced control systems whose size and complexity will challenge current verification and validation approaches. The recent adoption by the aerospace industry of model-based development tools such as Simulink® and SCADE Suite™ is removing barriers to the use of formal methods for the verification of critical avionics software. Formal methods use mathematics to prove that software design models meet their requirements, and so can greatly increase confidence in the safety and correctness of software.