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.










Software tools


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

Symbolic models for nonlinear time-delay systems using approximate bisimulations
Giordano Pola, Pierdomenico Pepe, Maria D. Di Benedetto, and Paulo Tabuada
Systems and Control Letters, 59, 365-373, 2010.
DOI:10.1016/j.sysconle2010.04.001
arXiv:0903.0361

Approximately bisimilar symbolic models for incrementally stable switched systems
Antoine Girard, Giordano Pola and Paulo Tabuada
IEEE Transactions on Automatic Control, 55(1), 116-126, 2010.
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.

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.

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
    
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.