From modelling control systems using Grafcet to analyzing systems using hybrid automata

Grafcet is a language which is used for the specification of control systems, although it is not very well suited for the verification of the specification. This paper describes the translation of grafcet specifications into hybrid automata. This translation is a part of a framework which enables not only the verification of a grafcet but of a hybrid system consisting of a discrete controller and a continuous process. The approach taken is based on the construction of a situation graph which serves as the underlying structure in the translation of a grafcet in its equivalent hybrid automaton