Runtime verification of electronic stability control system in automated vehicles with STL₃ formalism

Recently, extensive research has been done on automated vehicles (AV) to increase vehicle and road safety. Because of the uncertainty involved in the environmental interactions of vehicles, classical methods such as testing and model checking turned out to be insufficient in realizing full safety guarantees. As a result, runtime verification (RV) which is the verification in combination with runtime monitoring, seems to be a more appropriate method to ensure vehicle safety. One of the AV components that has attracted much attention from researchers is the electronic stability control (ESC) system. In this paper, an RV model is proposed to verify the safe operation of an ESC system using an automata-based monitoring method. The proposed model provides a specification language, called three-valued signal temporal logic (STL₃) formalism, for expressing the safety properties of AV components and a two-phase methodology for producing and deploying a monitor for an ESC system. The proposed model is evaluated using CarSim and MATLAB/Simulink simulation environments. The experiments show that the model can automatically generate the monitor and detect all violations of safety properties related to vehicle stability.