Title: Formal validation of intelligent-automated production systems: towards industrial applications

Authors: Hans-Michael Hanisch, Andrei Lobov, Jose L. Martinez Lastra, Reijo Tuokko, Valeriy Vyatkin

Addresses: Department of Engineering Science, Martin Luther University Halle-Wittenberg, Halle 06099, Germany. ' Institute of Production Engineering, Tampere University of Technology, P.O. Box 589, Tampere, Finland. ' Institute of Production Engineering, Tampere University of Technology, P.O. Box 589, Tampere, Finland. ' Institute of Production Engineering, Tampere University of Technology, P.O. Box 589, Tampere, Finland. ' Department of Electrical and Computer Engineering, The University of Auckland, Auckland, New Zealand

Abstract: This paper introduces a framework for formal modelling and validation of automation systems destined to be used directly by control engineers. The framework is based on a modelling formalism of Net Condition/Event Systems (NCES), which is graphical, modular and typed. This allows for the modelling of realistic hierarchically organised automation systems in a closed plant-controller loop. The framework consists of methodologies and tools, which enable formal analysis of automation systems. The framework is to be used for the improvement of safety characteristics, reliability and robustness of such systems by means of prediction of potential faults and deadlocks.

Keywords: formal verification; intelligent industrial automation; flexible manufacturing; programmable logic controllers; PLCs; net condition/event systems; NCES; ladder logic; flow charts; modeling; validation; plant control; closed-loop control; safety; reliability; robustness; fault prediction; deadlock; distributed control.

DOI: 10.1504/IJMTM.2006.008802

International Journal of Manufacturing Technology and Management, 2006 Vol.8 No.1/2/3, pp.75 - 106

Published online: 25 Jan 2006 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article