Formal Verification of Interactions of the RTOS, Memory System, and Application Programs at the PowerPC 750 Binary Code Level

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$125,000.00
Award Year:
2013
Program:
SBIR
Phase:
Phase I
Contract:
NNX13CL54P
Award Id:
n/a
Agency Tracking Number:
124851
Solicitation Year:
2012
Solicitation Topic Code:
A1.06
Solicitation Number:
n/a
Small Business Information
IL, Chicago, IL, 60618-3745
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
361627933
Principal Investigator:
Miroslav Velev
Principal Investigator
(773) 856-6633
miroslav.velev@aries-da.com
Business Contact:
Miroslav Velev
Business Official
(773) 856-6633
miroslav.velev@aries-da.com
Research Institute:
Stub




Abstract
In the proposed project, we will formally verify the correctness of the interaction between a Real-Time Operating System (RTOS) and user processes under various operating scenarios, such as multitasking, interrupt handling, user and kernel mode switching. The formal verification will be done assuming execution on the PowerPC 750 architecture that is implemented in the radiation-hardened RAD750 flight-control computers utilized in many NASA space missions, and are planned to be used in future spacecraft, including the Orion Multi-Purpose Crew Vehicle. A unique advantage of our project will be that the formal verification will precisely account for the bit-level semantics of all instructions, as well as the memory system, the bus, and devices on the bus, including multiple CPUs, and thus will allow us to precisely analyze all possible behaviors of the entire system, which is critical for aerospace applications.During Phase I we will lay the foundation for Phase II by: developing initial models of the memory system and the bus; formally defining the bit-level semantics of additional instructions from the PowerPC 750 architecture that we have not specified yet; identifying properties that we will prove to guarantee correct interaction of user processes with the target RTOS, the memory system, and the bus, including scenarios such as multitasking, interrupt handling, user and kernel mode switching; proving some of these properties; and identifying the most promising directions for Phase II work.

* information listed above is at the time of submission.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government