NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
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
Subject Category
Computer Programming And Software
Meeting Information
Meeting: NASA Formal Methods Symposium
Location: Washington D.C.
Country: United States
Start Date: April 13, 2010
End Date: April 15, 2010
Sponsors: NASA Headquarters
Distribution Limits
Public
Copyright
Public Use Permitted.

Related Records

IDRelationTitle20100018529Collected WorksProceedings of the Second NASA Formal Methods Symposium
No Preview Available