Automotive control design bug-finding with the S-TaLiRo tool

One of the important challenges in the Model Based Development (MBD) of automotive systems is the problem of verifying functional system properties. In its general form, the verification problem is undecidable due to the interplay between continuous and discrete system dynamics [1]. In this tutorial, we present the bounded-time temporal logic testing and verification problem for Cyber-Physical Systems (CPS) [2]. Temporal logics [3] can formally capture both state-space and real-time system requirements. For example, temporal logics can mathematically state requirements like “whenever the system switches to first gear, then it should not switch to second gear within 2.5 sec”. Our approach in tackling this challenging problem is to convert the verification problem into an optimization problem through a notion of robustness for temporal logics [4]. The robust interpretation of a temporal logic specification over a system trajectory quantifies “how much” the system trajectory satisfies or does not satisfy the specification. In general, the resulting optimization problem is non-convex and non-linear, the utility function is not known in closed-form and the search space is uncountable. Thus, stochastic search techniques are employed in order to solve the resulting optimization problem. We have implemented our testing and verification framework into a MATLAB (TM) toolbox called S-TaLiRo (System´s TemporAl LogIc Robustness) [5], [6]. In this tutorial, we will demonstrate how S-TaLiRo can provide answers to challenge problems from the automotive industry [7]-[10].