Object-oriented modular place/transition formalism for systematic modeling and validation of industrial automation systems

We introduce a framework for formal modeling and validation of automation systems destined to use by control engineers. The framework is based on a modeling formalism of net condition/event systems which is graphical, modular, and typed. This allows for modeling of realistic hierarchically organized automation systems in a closed-loop. The framework consists of methodologies and tools, which enable formal analysis of automation systems. The framework is to be used for improvement of safety characteristics, reliability and robustness of such systems by means of prediction of potential faults and deadlocks.