Citation
Paulo Tabuada. "On the synthesis of correct-by-design embedded control software". Talk or presentation, 17, April, 2009.

Abstract
The tight integration of computational systems with the physical world, now known as Cyber-Physical Systems, is believed to hold great promise for the competitiveness of several industries such as automotive, aerospace, chemical production, energy, healthcare, manufacturing, etc. Within Cyber-Physical Systems, embedded control software plays a major role by monitoring and regulating several continuous variables through feedback loops. Nevertheless, the design of embedded control software is still considered an art for which no rigorous and comprehensive design methodologies exist. In order to detect and eliminate design flaws, and the unavoidable software bugs, a large part of the design budget is consumed with validation and verification efforts. In this talk, I will propose a new paradigm for the synthesis of embedded control software. By changing the emphasis from verification to design, I will show that it is possible to synthesize correct-by-design embedded control software while providing formal guarantees of correctness and performance. This proposal is grounded on several technical results describing how differential equation models for control systems can be transformed into equivalent finite-state models for the purpose of software design. The new finite-state models offer a common language within which it is possible to express and solve design problems meeting computational and physical requirements. In particular, I will show how it is possible to automatically synthesize controllers enforcing discrete specifications (languages, finite-state machines, temporal logics, etc) on continuous systems. The synthesized controllers describe both the continuous control laws as well as its correct-by-design software implementation.

Electronic downloads

• CorrectByDesign.pdf · application/pdf · 2031 kbytes

• HTML

  Paulo Tabuada. <a
  href="http://chess.eecs.berkeley.edu/pubs/577.html"
  ><i>On the synthesis of correct-by-design embedded
  control software</i></a>, Talk or presentation, 
  17, April, 2009.

• Plain text

  Paulo Tabuada. "On the synthesis of correct-by-design
  embedded control software". Talk or presentation,  17,
  April, 2009.

• BibTeX

  @presentation{Tabuada09_OnSynthesisOfCorrectbydesignEmbeddedControlSoftware,
      author = {Paulo Tabuada},
      title = {On the synthesis of correct-by-design embedded
                control software},
      day = {17},
      month = {April},
      year = {2009},
      abstract = {The tight integration of computational systems
                with the physical world, now known as
                Cyber-Physical Systems, is believed to hold great
                promise for the competitiveness of several
                industries such as automotive, aerospace, chemical
                production, energy, healthcare, manufacturing,
                etc. Within Cyber-Physical Systems, embedded
                control software plays a major role by monitoring
                and regulating several continuous variables
                through feedback loops. Nevertheless, the design
                of embedded control software is still considered
                an art for which no rigorous and comprehensive
                design methodologies exist. In order to detect and
                eliminate design flaws, and the unavoidable
                software bugs, a large part of the design budget
                is consumed with validation and verification
                efforts. In this talk, I will propose a new
                paradigm for the synthesis of embedded control
                software. By changing the emphasis from
                verification to design, I will show that it is
                possible to synthesize correct-by-design embedded
                control software while providing formal guarantees
                of correctness and performance. This proposal is
                grounded on several technical results describing
                how differential equation models for control
                systems can be transformed into equivalent
                finite-state models for the purpose of software
                design. The new finite-state models offer a common
                language within which it is possible to express
                and solve design problems meeting computational
                and physical requirements. In particular, I will
                show how it is possible to automatically
                synthesize controllers enforcing discrete
                specifications (languages, finite-state machines,
                temporal logics, etc) on continuous systems. The
                synthesized controllers describe both the
                continuous control laws as well as its
                correct-by-design software implementation. },
      URL = {http://chess.eecs.berkeley.edu/pubs/577.html}
  }
  

Posted by Hiren Patel on 20 Apr 2009.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.