*banner
 

On the synthesis of correct-by-design embedded control software
Paulo Tabuada

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

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

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.

You are not logged in 
©2002-2014 Chess