TY  - CONF
AU  - Tronci, Enrico
PY  - 1999
DA  - 1999//
TI  - Formally Modeling a Metal Processing Plant and its Closed Loop Specifications
BT  - 4th IEEE International Symposium on High-Assurance Systems Engineering (HASE)
SP  - 151
PB  - IEEE Computer Society
CY  - Washington, D.C, USA
AB  - 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.
SN  - 0-7695-0418-3
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Tronci1999a.pdf
UR  - https://doi.org/10.1109/HASE.1999.809490
DO  - 10.1109/HASE.1999.809490
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=50), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - Tronci1999
ER  -