On the Specification and Verification of Safety Properties in Data-Driven Critical Systems

Data is at the core of the design of modern Safety-Critical Systems. Data is no longer only sensed and processed in the context of the control loops of such systems. It is also secured, stored, and transmitted for the sake of the decision-making processes required for higher levels of autonomy. The task-centered strategies traditionally used to design critical systems consistently support scheduling analysis and verification of tasks execution times as long as periods, deadlines, and execution time estimates are known, but mostly ignore the flow of data across the various components in the system and often assume that data generation time is constant and can be fully encapsulated in the execution time of tasks. These assumptions, however, are not in phase with the design of modern autonomous systems such as smart factories and autonomous vehicles, examples of systems that address critical constraints, that are quickly advancing towards autonomy. A Data-driven approach to the design of such systems can more promptly accommodate requirements such as data freshness, redundant data sources, and operational safety. In this work, we propose a Framework to support the specification and verification of safety properties of safety-critical systems that are designed using data-driven methods. We extract the properties considering the timing and data dependency, which are verified at run-time via a Safety Enforcement Unit (SEU). The SEU is an isolated component of the system that constantly monitors the data generated by the system and verifies the safety properties, issuing counter-measures as needed to maintain system safety. We demonstrate and evaluate the proposed solution with the modeling of an Autonomous Vehicle, with a proof of concept implementation considering an autonomous vehicle simulator integrated with hardware-in-the-loop. We demonstrate that the system can be formally verified at runtime, where the SEU implementation consumed less than 2% of the computational power of the Electronic Control Unit (ECU) used for evaluation.