Paper Title:
Formally Modeling a Metal Processing Plant and its
Closed Loop Specifications


Author: Enrico Tronci

Affiliation:
Dip. di MAtematica Pura ed Applicata
Universita` di L'Aquila
Coppito 67100 L'Aquila
Italy

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


We present a case study on automatic synthesis
of control software
from formal specifications for
an industrial automation control system.
Our aim is to compare
the effectiveness (i.e. design effort and controller quality)
of automatic controller synthesis
from closed loop formal specifications
with that 
of manual controller design followed by automatic verification.

The system to be controlled (plant) models a metal processing
facility near Karlsruhe. 

We succeeded in automatically generating  C code implementing a
(correct by construction)
embedded controller for such a plant from closed loop formal specifications.
Our experimental results show that for 
industrial automation control systems
automatic synthesis is a viable and profitable
(especially as far as design effort is concerned) 
alternative to
manual design followed by automatic verification.


Keywords

Formal Methods, Model Checking, Control Systems,
Finite State Systems, Reactive Systems,
Hybrid Systems, Discrete Event Systems, 
Supervisory Control, Manufacturing Systems.