Large-scale complex safety-critical systems are inherently difficult to both verify in real-time and transparently validate. The iterative specification development process is challenging when the performance and reliability demands of target systems (eg, flight software) require strict behavior of verification tools which often trade off usability for performance and conformance. Providing both strict behavioral guarantees and efficiency of this iterative process allows specification authors and engineers to more quickly deploy their systems and have more confidence in their verification efforts.

Our on-going work addresses this challenge by providing validation transparency for specification authors during system development while maintaining necessary performance during deployment by extending R2U2, a real-time verification tool specifically designed for resource-constrained systems. We also strengthen the trust in R2U2 by providing a robust suite of tests to show adherence to the strict requirements of safety-critical flight software. These tasks are efforts toward transitioning R2U2 from a research-grade tool to a flightsoftware-grade tool suitable for use by real-time safetycritical systems and thereby answer the calls for expanded developmental-to-operational verification by, eg, the Vehicle System Management (VSM) team of the NASA Lunar Gateway.