Speaker: Pei Zhang, ECpE Graduate Student
Advisor: Phillip H. Jones and Kristin Y. Rozier
Title: A Hardware/Software Co-design Framework for Deploying Runtime Verification Technique
Abstract: Runtime verification (RV) of formal specifications has become essential for the operation of safety-critical real-time systems. Though many RV tools assume unlimited resource-support, e.g., for verification over software systems, in many flight-certified, embedded, or hardware systems (e.g., FPGAs), resources available for monitoring formal specifications are constrained. As a result, it is crucial to design an efficient memory model for verification over hardware platforms as well as to estimate the size of the specifications that can be handled based on resources with a fixed capacity. In this seminar, I will talk about the software compiler for interpreting temporal formulas for hardware, and how we embedded the runtime software-configurable hardware temporal logic computation core into a resource-constrained FPGA inside NASA’s Robonaut2.