*banner
 

Specification Mining of Industrial-scale Control Systems
Alexandre Donze

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess