Mining requirements from closed-loop control models

A significant challenge to the formal validation of software-based industrial control systems is that system requirements are often imprecise, non-modular, evolving, or even simply unknown. We propose a framework for mining 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. Our algorithm is an instance of counterexample-guided inductive synthesis: an intermediate candidate requirement is synthesized from simulation traces of the system, which is refined using counterexamples to the candidate obtained with the help of a falsification tool. The algorithm terminates when no counterexample is found. Mining has many usage scenarios: mined requirements can be used to validate future modifications of the model, they can be used to enhance understanding of legacy models, and can also guide the process of bug-finding through simulations. We present two case studies for requirement mining: a simple automobile transmission controller and an industrial airpath control model for an engine.