Proceedings of 2nd IEEE Conference on:
Formal Engineering Methods,
Dec. 1998, Brisbane, Australia
IEEE CS Press


Title:
Automatic Synthesis of Controllers from Formal Specifications

Author:
Enrico Tronci
Univ. di L'Aquila
Coppito 67100 L'Aquila
Italy

tronci@univaq.it
http://univaq.it/~tronci




Abstract

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 $10^9$ states.