Citation
Alexandre Donze. "Specification Mining of Industrial-scale Control Systems". Talk or presentation, 14, May, 2013.

Abstract
Industrial-scale control systems are more and more developed in the model-based design paradigm. This typically involves capturing a plant model that describes the dynamical characteristics of the physical processes within the system, and a controller model, which is a block-diagram-based representation of the software used to regulate the plant behavior. In practice, plant models and controller models are highly complex as they can contain nonlinear hybrid dynamics, look-up tables storing pre-computed values, several levels of design-hierarchy, design-blocks that operate at different frequencies, and so on. Moreover, the biggest challenge is that system requirements are often imprecise, non-modular, evolving, or even simply unknown. As a result, formal techniques have been unable to digest the scale and format of industrial-scale control systems. On the other hand, the Simulink modeling language -- a popular language for describing such models -- is widely used as a high-fidelity simulation tool in the industry, and is routinely used by control designers to experimentally validate their controller designs. This raises the question: "What can we accomplish if all we have is a very complex Simulink model of a control system?" In this talk, we give an example of a simulation-guided formal technique that can help characterize temporal properties of the system, or guide the search for design behaviors that do not conform to "good behavior". Specifically, we present a way to algorithmically mine temporal assertions from a Simulink model. 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. (Joint work with X. Jin, J. Deshmuck and S. Seshia).

Electronic downloads

• dreams-donze-may-2013.pdf · application/pdf · 1082 kbytes

• HTML

  Alexandre Donze. <a
  href="http://chess.eecs.berkeley.edu/pubs/989.html"
  ><i>Specification Mining of Industrial-scale
  Control Systems</i></a>, Talk or presentation, 
  14, May, 2013.

• Plain text

  Alexandre Donze. "Specification Mining of
  Industrial-scale Control Systems". Talk or
  presentation,  14, May, 2013.

• BibTeX

  @presentation{Donze13_SpecificationMiningOfIndustrialscaleControlSystems,
      author = {Alexandre Donze},
      title = {Specification Mining of Industrial-scale Control
                Systems},
      day = {14},
      month = {May},
      year = {2013},
      abstract = {Industrial-scale control systems are more and more
                developed in the model-based design paradigm. This
                typically involves capturing a plant model that
                describes the dynamical characteristics of the
                physical processes within the system, and a
                controller model, which is a block-diagram-based
                representation of the software used to regulate
                the plant behavior. In practice, plant models and
                controller models are highly complex as they can
                contain nonlinear hybrid dynamics, look-up tables
                storing pre-computed values, several levels of
                design-hierarchy, design-blocks that operate at
                different frequencies, and so on. Moreover, the
                biggest challenge is that system requirements are
                often imprecise, non-modular, evolving, or even
                simply unknown. As a result, formal techniques
                have been unable to digest the scale and format of
                industrial-scale control systems. On the other
                hand, the Simulink modeling language -- a popular
                language for describing such models -- is widely
                used as a high-fidelity simulation tool in the
                industry, and is routinely used by control
                designers to experimentally validate their
                controller designs. This raises the question:
                "What can we accomplish if all we have is a very
                complex Simulink model of a control system?" In
                this talk, we give an example of a
                simulation-guided formal technique that can help
                characterize temporal properties of the system, or
                guide the search for design behaviors that do not
                conform to "good behavior". Specifically, we
                present a way to algorithmically mine temporal
                assertions from a Simulink model. 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. (Joint work
                with X. Jin, J. Deshmuck and S. Seshia). },
      URL = {http://chess.eecs.berkeley.edu/pubs/989.html}
  }
  

Posted by David Broman on 15 May 2013.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.