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.
Verification and Control of Hybrid Systems: A Symbolic Approach
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.
DOI:10.1016/j.automatica.2008.02.021
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.
DOI:10.1016/j.sysconle.2007.11.005
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.