Mining Requirements from Closed-Loop Control Models

Xiaoqing Jin, Alexandre Donzé, Jyotirmoy Deshmukh, and Sanjit A. Seshia. Mining Requirements from Closed-Loop Control Models. IEEE Transactions on Computer-Aided Design of Circuits and Systems, 34(11):1704–1717, 2015.
Donald O. Pederson Best Paper Award for IEEE TCAD (awarded in 2017).

Download

[pdf] 

Abstract

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.

BibTeX

@ARTICLE{jin-tcad15, 
  author    = {Xiaoqing Jin and Alexandre Donz{\'{e}} and Jyotirmoy Deshmukh and Sanjit A. Seshia},
  title     = {Mining Requirements from Closed-Loop Control Models},
  journal={IEEE Transactions on Computer-Aided Design of Circuits and Systems}, 
  year={2015}, 
  volume    = {34},
  number    = {11},
  pages     = {1704--1717},
  wwwnote = {<b>Donald O. Pederson Best Paper Award</b> for IEEE TCAD (awarded in 2017).},
  abstract = {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.},
}