Data-Centric Design for Formal Verification of Vehicle Monitoring

The testing and validation of vehicles include several challenges regarding the calibration of its components to enable the safety and efficiency of a vehicle. This step comprises extensive testing sessions where data is collected for offline analysis. Nevertheless, having a real-time or near-real-time analysis of the data being collected can benefit testing and validation by promoting early detection of faulty configurations that may impair the test results or even damage the vehicle. This paper presents a solution for online formal verification of data acquisition without the need to externalize the internal process of the vehicle. The proposed solution is enabled by combining a Data-Centric Design and Signal Temporal Logic. We describe the process of deriving Signal Temporal Logic property monitors from the Data-Centric Design and embedding them to promote formal verification of Event-Driven, Periodic, and more complex data sampling policies. We evaluate the proposed solution on a case study over the project Intelligent Acquisition and Analysis System for Electronic Control Units (IASE), a joint effort of LISHA and Renault do Brasil. The results demonstrated that the proposed solution could suffice the throughput of the original system. Considering plausibility verification based on valid data ranges, the proposed solution was able to provide, on average, 10000 verification every 3.2 ms in the same platform used in IASE, an ARM Cortex-A53 processor.