Using Visual Specifications in Verification of Industrial Automation Controllers

This paper deals with further development of a graphical specification language resembling timing-diagrams and allowing specification of partially ordered events in input and output signals. The language specifically aims at application in modular modelling of industrial automation systems and their formal verification via model-checking. The graphical specifications are translated into a model which is connected with the original model under study. Formal verification of industrial automation systems requires three constituent components: a model of the controller, a model of the uncontrolled plant, and a specification of desired or forbidden plant behaviour.