Mining Requirements from Closed-Loop Control Models

Xiaoqing Jin, Alexandre Donzé, Jyotirmoy Deshmukh, and Sanjit A. Seshia. Mining Requirements from Closed-Loop Control Models. In Proceedings of the International Conference on Hybrid Systems: Computation and Control (HSCC), April 2013.

Download

[pdf] 

Abstract

A significant challenge to the formal validation of software-based control systems in an industrial setting is that the system requirements are often imprecise, non-modular, evolving, or even simply unknown. We propose a framework to mine requirements from the closed-loop model of an industrial-scale control system, such as one specified in the Simulink modeling language. 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. 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 enhance the process of bug-finding through simulations. We demonstrate our technique on two case studies: a simple automobile transmission controller and an industrial model of airpath control for an engine.

BibTeX

@inproceedings{jin-hscc13,
  author    = {Xiaoqing Jin and Alexandre Donz{\'{e}} and Jyotirmoy Deshmukh and Sanjit A. Seshia},
  title     = {Mining Requirements from Closed-Loop Control Models},
 booktitle = {Proceedings of the International Conference on Hybrid Systems: Computation and Control (HSCC)},
 month = "April",
 year = {2013},
 abstract = {A significant challenge to the formal validation of software-based 
control systems in an industrial setting is that the system 
requirements are often imprecise, non-modular, evolving, 
or even simply unknown. We propose a framework to 
mine requirements from the closed-loop model of an industrial-scale 
control system, such as one specified in the Simulink 
modeling language. 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. 
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 enhance  
the process of bug-finding through simulations. We 
demonstrate our technique on two case studies: a simple automobile 
transmission controller and an industrial model of 
airpath control for an engine.},
}