Description: 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.

Benefits: The tool flow and formal verification methods that we will develop will allow NASA to easily retarget the formal verification to any RTOS and user processes, represented as binary code, and to any new processor architecture, given formal definitions of its instruction semantics, memory system, bus, and devices on the bus. By reusing the formal definitions of all functional units for integer, logical, and floating-point instructions in the PowerPC 750 architecture that we have already defined in our NASA SBIR Phase II project titled Efficient Techniques for Formal Verification of PowerPC 750 Executables, it will be possible to formally specify the bit-level semantics of a new processor architecture in several months. Also, we will be able to use the formal definition of the bit-level instruction semantics of the architecture as a non-pipelined specification when formally verifying a new pipelined/superscalar/VLIW implementation processor for that architecture by applying our industrial tool flow for formal verification of pipelined processors. Thus, we will prove that the designs of new processors will implement the exact bit-level specification of the instruction semantics that is used to formally verify the correctness of the software and its interaction with the RTOS, the memory system, bus, and devices on the bus, including under scenarios such as multitasking, interrupt handling, user and kernel mode switching. These capabilities are critical for aerospace applications.

The NASA applications will also benefit other government agencies, such as DoD, DoE, NIST, and NIH. Furthermore, all companies that either manufacture microprocessors or develop IP of microprocessors, as well as all their clients that develop safety-critical software, will be potential users of the resulting technology. As embedded microprocessors are increasingly used in safety-critical applications, many of them controlled by an RTOS, it will become the norm to formally verify the executables for such applications, as the correctness of a microprocessor alone will not be sufficient to guarantee correct execution of the software, and the absence of errors in the binary code will become a requirement. Additional applications will include the formal verification of executables for absence of security vulnerabilities.