Search this site

CyPhyLab

News

10/22/09: Pessoa, a tool for embedded control software synthesis, is released.

09/28/09: NSF funds Prof. Majumdar and Prof. Tabuada to close the gap in controller synthesis.

06/15/09: Prof. Paulo Tabuada receives the 2009 AACC Donald P. Eckman award.

06/15/09: New book on Hybrid Systems already available online.

05/11/09: Georgia Tech Summer School on Cyber-Physical Systems

01/12/09: New journal IEEE Embedded Systems Letters. Consider submitting your best work!
Home‎ > ‎Projects‎ > ‎

Automated synthesis of embedded control software

Automated Synthesis of Embedded Control Software (NSF CAREER 0717188)

This project attempts to answer the following question: Can we synthesize correct-by-design embedded control software? If the answer is yes, then the need for formal verification can be greatly reduced thereby reducing the design time and design cost of embedded control software.

Within the context of this project we developed a specific correct-by-design methodology based on symbolic or discrete abstractions of control systems. For discrete-time control systems we use bisimulation as the notion of abstraction while for continuous-time control systems we use the recently introduced notion of approximate bisimulation. Based on symbolic abstractions, correct-by-design synthesis can be performed as a sequence of three steps:

Step I: Abstraction

In this step a finite-state abstraction of the continuous system being controlled is constructed. This abstraction results in a finite-state model that is of the same kind of the models used to describe software and hardware. The remaining two steps rely on the existence and construction of these symbolic abstractions.











Step II: Controller Synthesis

Once a symbolic model for the continuous dynamics has been built, we can compose it with a finite-state model of existing software resources and with a finite-state model of existing hardware resources. The model resulting from this composition still has finitely many states and is regarded as the plant to be controlled. Existing results from supervisory control of discrete-event systems or from algorithmic game theory can now be used to synthesize a finite-state controller that, when composed with the plant, enforces the desired specifications. Note that the specifications can refer to the continuous dynamics, to the existing software resources, to the existing hardware resources, or to combinations of all of these.

Step III: Controller Refinement

The final step consists in refining the finite-state controller into a hybrid controller that determines which continuous-time signals should be used to control the continuous system. The refinement step is based on the bisimulation or approximate bisimulation relation between the continuous system to be controlled and its symbolic abstraction. The resulting hybrid controller is a mathematical model of the control software as it describes how to use the existing software and hardware resources to control the physical system. Moreover, the hybrid controller can be directly converted into software given a desired target platform.










Publications

The following publications describe several aspects of the correct-by-design methodology developed within this project.

    Paulo Tabuada
    Springer, 2009.
    Available online through SpringerLink

    Approximately bisimilar symbolic models for incrementally stable switched systems
    Antoine Girard, Giordano Pola and Paulo Tabuada
    Submitted for publication.
    arXiv:0807.5022
    
    Symbolic models for nonlinear control systems: Alternating approximate bisimulations
    Giordano Pola and Paulo Tabuada
    SIAM Journal on Control and Optimization, 48(2), 719-733, 2009.
    arXiv:0707.4205 

    Approximately bisimilar symbolic models for nonlinear control systems
    Giordano Pola, Antoine Girard and Paulo Tabuada
    Automatica, 44(10), 2508-2516, October 2008.
    arXiv:0706.0246
    
    An approximate simulation approach to symbolic control
    Paulo Tabuada
    IEEE Transactions on Automatic Control, 53(6), 1406-1418, July 2008.
    PDF file

    Controller synthesis for bisimulation equivalence
    Paulo Tabuada
    Systems and Control Letters, 57(6), 443-452, June 2008.    
    arXiv:0706.0929

    Symbolic models for control systems
    Paulo Tabuada
    Acta Informatica, 43(7), 477-500, February 2007.
    Special issue on Hybrid Systems.
    PDF file
    
    Linear Time Logic control of discrete-time linear systems
    Paulo Tabuada and George J. Pappas
    IEEE Transactions on Automatic Control, 51(12), 1862-1877, December 2006.
    PDF file

    Symbolic control of linear systems based on symbolic subsystems
    Paulo Tabuada
    IEEE Transactions on Automatic Control, 51(6), 1003-1013, June 2006.
    Special issue on Symbolic Methods for Complex Control Systems.
    PDF file