@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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},
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.},
}