Automated Synthesis of Embedded Control Software (NSF CAREER 0717188) This project attempts to answer the following question: Can we synthesize correctbydesign 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 correctbydesign methodology based on symbolic or discrete abstractions of control systems. For discretetime control systems we use bisimulation as the notion of abstraction while for continuoustime control systems we use the recently introduced notion of approximate bisimulation. Based on symbolic abstractions, correctbydesign synthesis can be performed as a sequence of three steps: Step I: Abstraction In this step a finitestate abstraction of the continuous system being controlled is constructed. This abstraction results in a finitestate 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 finitestate model of existing software resources and with a finitestate 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 discreteevent systems or from algorithmic game theory can now be used to synthesize a finitestate 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 finitestate controller into a hybrid controller that determines which continuoustime 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 correctbydesign methodology developed within this project.
Symbolic models for nonlinear timedelay systems using approximate bisimulations Giordano Pola, Pierdomenico Pepe, Maria D. Di Benedetto, and Paulo Tabuada Systems and Control Letters, 59, 365373, 2010. DOI:10.1016/j.sysconle2010.04.001 arXiv:0903.0361
