FM Program: Partitioning Project

(Note: most of the following text comes directly from the June 2000 edition of NASA Langley's Research and Technology-Transfer Program in Formal Methods, which is available in PDF and PostScript formats.)

The RTCA Special Committee 182 (SC-182) has been established to develop a Minimum Operational Performance Standard (MOPS) for an Avionics Computer Resource (ACR). The ACR will have the capability of performing multiple aircraft functions through use of partitioning. Funda- mental to the success of the ACR strategy is a guarantee that the ACR platform will prevent any application from corrupting another. In particular, the ACR must provide:

• space partitioning (no matter what an application does it cannot corrupt the memory of another application), and
• time partitioning (no matter what an application does it cannot prevent another application from obtaining its scheduled allocation of CPU time)

while supporting:

• inter-partition communications, and
• common modular/configurable I/O (the ACR must allow the partitions access to external devices through a suite of bus protocols such as ARINC 429, ARINC 629, etc.)

Our first efforts have been directed towards developing an abstract formal model of space partitioning that can serve as the basis for evaluating the design of an ACR. The PVS formal model is based on mathematical modeling techniques developed by the computer security community. The model has been used on three candidate designs, each an abstraction of features found in real systems.

SRI International was funded by the FAA and NASA to identify the requirements for partitioning in integrated modular avionics (IMA) and to explore how to achieve those requirements with very high assurance. The final report on this work was published in June 1999.

See also Ben DiVito's paper (A Formal Model of Partitioning for Integrated Modular Avionics. NASA Contractor Report CR-1998-208703, NASA Langley Research Center, Hampton, Virginia, August 1998), and his slides from Lfm97.