Software Model Checking of ARINC-653 Flight Code with MCPThe ARINC-653 standard defines a common interface for Integrated Modular Avionics (IMA) code. In particular, ARINC-653 Part 1 specifies a process- and partition-management API that is analogous to POSIX threads, but with certain extensions and restrictions intended to support the implementation of high reliability flight code. MCP is a software model checker, developed at NASA Ames, that provides capabilities for model checking C and C++ source code. In this paper, we present recent work aimed at implementing extensions to MCP that support ARINC-653, and we discuss the challenges and opportunities that consequentially arise. Providing support for ARINC-653 s time and space partitioning is nontrivial, though there are implicit benefits for partial order reduction possible as a consequence of the API s strict interprocess communication policy.
Document ID
20100018550
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Thompson, Sarah J. (NASA Ames Research Center Moffett Field, CA, United States)
Brat, Guillaume (NASA Ames Research Center Moffett Field, CA, United States)
Venet, Arnaud (NASA Ames Research Center Moffett Field, CA, United States)
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium