The ARINC-653 standard specifies the operating system’s software interface for Integrated Modular Avionics flight code. Adding a capability to directly model check code written with this API makes it possible for MCP to be used on Orion and Ares flight code as that is implemented. MCP can directly check C and C++ code without a requirement for translation to another language or for a (potentially inaccurate) manual model extraction process.
A preliminary paper outlining the work has been submitted to the 2010 NASA Formal Methods symposium, and is currently in review.
NASA PROGRAM FUNDING: NASA ETDP (Exploration Technology Development Program) Intelligent Software Design Project
Contact: Sarah Thompson