Automotive systems requirement mining using breach
Alexandre Donzé, Xiaoqing Jin, Jyotirmoy V. Deshmukh, Sanjit A. Seshia · 2015
Automative control systems are more and more developed in the model-based design paradigm. This typically involves capturing a plant model that describes the dynamical characteristics of the physical processes within the system, and a controller model, which is a block-diagram-based representation of the software used to regulate the plant behavior. In practice, plant models and controller models are highly complex as they can contain nonlinear hybrid dynamics, look-up tables storing pre-computed values, several levels of design-hierarchy, design-blocks that operate at different frequencies, and so on. Moreover, system requirements are often imprecise, non-modular, evolving, or even simply unknown. In this talk, we describe a simulation-guided formal technique that can help characterize temporal properties of a system described with the Simulink modeling language, which is widely used as a high-fidelity simulation tool and is routinely used by control designers to experimentally validate their controller designs. Specifically, we present a way to algorithmically mine temporal assertions implemeted in the tool Breach. The input to our algorithm is a requirement template expressed in Parametric Signal Temporal Logic - a formalism to express temporal formulas in which concrete signal or time values are replaced by parameters. Our algorithm is an instance of counterexample-guided inductive synthesis: an intermediate candidate requirement is synthesized from simulation traces of the system, which is refined using counterexamples to the candidate obtained with the help of a falsification tool. The algorithm terminates when no counterexample is found. Mining has many usage scenarios: mined requirements can be used to validate future modifications of the model, they can be used to enhance understanding of legacy models, and can also guide the process of bug-finding through simulations.