Automatic Co-Synthesis of Hardware and Software Safety Monitors for Embedded Systems

Abstract

Embedded systems have become pervasive and increasingly complex, especially in modern applications such as self-driving vehicles, where safety requires both accurate functionality and real-time guarantees. However, the complexity and the integration of artificial intelligence and machine learning algorithms in autonomous systems challenge conventional test-based verification methods. Given the continuous evolution and deployment of these systems, verification must keep pace to ensure their reliability and safety. Runtime verification is a promising approach for validating system behaviors during execution using monitors derived from formal system specifications. The adoption of runtime monitoring has historically been limited to experts, primarily due to the esoteric formal notations and verification processes. To overcome this barrier, this dissertation presents GROOT, a novel methodology and framework designed to automate synthesis of hardware and/or software monitors from pseudo- English statements. The automatic steps include translating English properties to formalisms, converting the formalisms into monitor automata, and formally verifying the monitors. GROOT addresses the distinction between functional and timing requirements inherent in real-time embedded systems by providing distinct pseudo-English languages and synthesis flows. This dual approach allows customized verification processes for each category. To make the monitor structure simple, monitor inputs and responses are handled in separate external modules, allowing formal analysis methods to be used. The synthesized monitors can assist system development and be retained in fielded systems. Their lightweight nature enables the deployment of multiple monitors, each focusing on specific circumstances independently and concurrently. Monitor implementations can range from sequential software to parallel hardware, allowing for flexibility in meeting various system constraints. By eliminating the need for manual code generation and verification, GROOT allows practitioners to synthesize monitors without requiring a formal methods background.