USA flag logo/image

An Official Website of the United States Government

Formal Verification of Interactions of the RTOS, Memory System, and Application…

Award Information

Agency:
National Aeronautics and Space Administration
Branch:
N/A
Award ID:
Program Year/Program:
2013 / SBIR
Agency Tracking Number:
124851
Solicitation Year:
2012
Solicitation Topic Code:
A1.06
Solicitation Number:
Small Business Information
Aries Design Automation, LLC
2705 West Byron Street Chicago, IL 60618-3745
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 1
Fiscal Year: 2013
Title: Formal Verification of Interactions of the RTOS, Memory System, and Application Programs at the PowerPC 750 Binary Code Level
Agency: NASA
Contract: NNX13CL54P
Award Amount: $125,000.00
 

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.

Principal Investigator:

Miroslav N. Velev
Principal Investigator
7738566633
miroslav.velev@aries-da.com

Business Contact:

Miroslav Velev
Business Official
7738566633
miroslav.velev@aries-da.com
Small Business Information at Submission:

Aries Design Automation, LLC
2705 West Byron Street Chicago, IL 60618-3745

EIN/Tax ID: 202887585
DUNS: N/A
Number of Employees:
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No