@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
@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.},
}