The automotive industry is increasingly dependent on computing systems with variable levels of critical requirements. The verification and validation methods for these systems are now leveraging complex AI methods, for which the decision algorithms introduce non-determinism, especially in autonomous driving. This paper presents a runtime verification technique agnostic to the target system, which focuses on monitoring spatio-temporal properties that abstract the evolution of objects’ behavior in their spatial and temporal flow. First, a formalization of three known traffic rules (from the Vienna convention on road traffic) is presented, where a spatio-temporal logic fragment is used. Then, these logical expressions are translated to a monitoring model written in the first-order logic, where they will be processed by a non-linear satisfiability solver. Finally, the translation allows the solver to check the validity of the encoded properties according to an instance of a specific traffic scenario (a trace). The results obtained from our tool that automatically generates a monitor from a formula show that our approach is feasible for online monitoring in a real-world environment.
Abstract
Published at: FMICS22 – Formal Methods for Industrial Critical Systems https://doi.org/10.1007/978-3-031-15008-1_11
Acknowledgment
This work was partially supported by the European Regional Development Fund (ERDF) through the Competitiveness and Internationalization Operational Program (COMPETE 2020) of Portugal 2020 [Project STEROID with number 069989 (POCI-01-0247-FEDER-069989)]. This work was also partially supported by FCT/MCTES grant UIDB/04516/2020.
Access Complete Publication
For an in-depth exploration of our findings and methodologies, download here
