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

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.