Formal validation of intelligent-automated production systems: towards industrial applications
Hans Michael Hanisch, Andrei Lobov, Jose Luis Martinez Lastra, Reijo O. Tuokko, Valeriy V. Vyatkin · International Journal of Manufacturing Technology and Management · 2006
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.