Paper Title:
Automatic Synthesis of Control Software 
for an Industrial Automation Control System


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



Abstract

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)
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, Embedded Control Systems,
Finite State Systems, Reactive Systems, Hybrid Systems,
Discrete Event Systems, Supervisory Control,
Ordered Binary Decision Diagrams, Manufacturing Systems.