Validation and verification of grafcets using state machine

Abstract

This paper presents a method to verify (the internal consistency) and to validate (with respect to the purpose of the builders) Sequential Function Charts [8] (grafcets in French). The method is based upon the translation of any grafcet into its equivalent finite automaton. The proofs of consistency of the models are then established on this automaton. The main difficulty of this approach is the control of the combinatorial explosion implied by the parallel and the synchronous nature of Grafcet. A specific grammar has been developed in order to express the expected properties to prove. An example is given to illustrate the presented approach.