TY  - CONF
AU  - Tronci, Enrico
PY  - 1998
DA  - 1998//
TI  - Automatic Synthesis of Controllers from Formal Specifications
BT  - Proc of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM)
SP  - 134
EP  - 143
CY  - Brisbane, Queensland, Australia
AB  - Many safety critical reactive systems are indeed embedded control systems. Usually a control system can be partitioned into two main subsystems: a controller and a plant. Roughly speaking: the controller observes the state of the plant and sends commands (stimulus) to the plant to achieve predefined goals. We show that when the plant can be modeled as a deterministic finite state system (FSS) it is possible to effectively use formal methods to automatically synthesize the program implementing the controller from the plant model and the given formal specifications for the closed loop system (plant+controller). This guarantees that the controller program is correct by construction. To the best of our knowledge there is no previously published effective algorithm to extract executable code for the controller from closed loop formal specifications. We show practical usefulness of our techniques by giving experimental results on their use to synthesize C programs implementing optimal controllers (OCs) for plants with more than 109 states.
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Tronci1998.pdf
UR  - https://doi.org/10.1109/ICFEM.1998.730577
DO  - 10.1109/ICFEM.1998.730577
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=52), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - Tronci1998
ER  -