Formal verification of a control system can be performed by checking if a model of its dynamical behavior conforms to temporal requirements. Unfortunately, adoption of formal verification in an industrial setting is a formidable challenge as design requirements are often vague, non-modular, evolving, or sometimes simply unknown. We propose a framework to mine requirements from a closed-loop model of an industrial-scale control system, such as one specified in Simulink.
The input to our algorithm is a requirement template expressed in Parametric Signal Temporal Logic: a logical formula in which concrete signal or time values are replaced with parameters. Given a set of simulation traces of the model, our method infers values for the template parameters to obtain the strongest candidate requirement satisfied by the traces.
It then tries to falsify the candidate requirement using a falsification tool. If a counterexample is found, it is added to the existing set of traces and these steps are repeated; otherwise, it terminates with the synthesized requirement. Requirement mining has several usage scenarios: mined requirements can be used to formally validate future modifications of the model, they can be used to gain better understanding of legacy models or code, and can also help enhancing the process of bug-finding through simulations.
We demonstrate the scalability and utility of our technique on three complex case studies in the domain of automotive powertrain systems: a simple automatic transmission controller, an air-fuel controller with a mean-value model of the engine dynamics, and an industrial-size prototype airpath controller for a diesel engine. We include results on a bug found in the prototype controller by our method.
A RUNNING EXAMPLE
We are interested in the following signals: the vehicle speed, transmission gear position, and engine speed measured in RPM (rotations per minute). Suppose we want to use this controller to ensure the requirement that the engine speed never exceeds 4500 rpm, and that the vehicle never drives faster than 120 mph. After simulating the closed-loop system Fig. 2 shows that these requirements are not met.
PRELIMINARIES AND OVERVIEW
Our algorithm (Algorithm 1) for mining STL requirements from the closed- loop model in Simulink is an instance of a counter example guided inductive synthesis procedure, shown in Fig. 3. It consists of two key components.
For such classes the mining technique can be complete, i.e., absence of a counterexample means that we have identified the strongest requirement. Due to its incompleteness for general systems, the falsification tool may not be able to find a counterexample though one exists. We argue that a requirement mined in this fashion is still useful as it is one that FALSIFYALGO is unable to disprove even after extensive simulations, and is thus likely to be close to the actual requirement.
Intuitively, this means that the valuation is closed to the boundary of the validity domain. Under certain regularity conditions, one can show that on such boundary, the satisfaction function ρ is equal to 0. On Fig. 4, we represent the validity domain for a simple property and a signal.
REQUIREMENT TEMPLATES FOR AUTOMOTIVE CONTROL SYSTEMS
We now discuss a set of PSTL formulas that serve as useful template requirements for continuous and hybrid dynamical systems. We start with a general discussion on useful templates for such systems, and then present particular templates specialized to express requirements on closed-loop control systems, with an emphasis on the automotive domain. Most of the requirements discussed herein were obtained by discussions with designers, and correspond to well-known metrics and tests used to judge design quality. In what follows, we use T to represents the simulation time horizon.
The implication here is that the algorithm pushed the falsifier to finding a behavior in the model that exhibits hunting behavior, or oscillations of magnitude exceeding the tolerance. This output signal is shown in Fig. 5. This behavior was unexpected; discussions with the designers revealed that it was a real bug. Investigating further, we traced the root-cause to an incorrect value in a lookup table; such lookup tables are commonly used to speed up the computation time by storing pre-computed values approximating the control law.
Mining requirements from programs and circuits is well-studied in the field of computer science. In computer science, the word “requirement” is often synonymous with “specification”. These techniques vary based on what is mined, e.g., automata, temporal rules, and sequence diagrams. They also differ on the input to the mining tool; e.g., techniques based on static analysis or model checking operate on the source code, dynamic techniques mine from execution traces.
Source: University of California
Authors: Xiaoqing Jin | Alexandre Donze | Jyotirmoy V. Deshmukh | Sanjit A. Seshia