You are here

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
Contract: NNX13CL54P
Agency Tracking Number: 124851
Amount: $125,000.00
Phase: Phase I
Program: SBIR
Solicitation Topic Code: A1.06
Solicitation Number: N/A
Solicitation Year: 2012
Award Year: 2013
Award Start Date (Proposal Award Date): 2013-05-23
Award End Date (Contract End Date): 2013-11-23
Small Business Information
IL, Chicago, IL, 60618-3745
DUNS: 361627933
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Miroslav Velev
 Principal Investigator
 (773) 856-6633
Business Contact
 Miroslav Velev
Title: Business Official
Phone: (773) 856-6633
Research Institution
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. *

US Flag An Official Website of the United States Government