Proving sequential function chart programs using automata

Abstract

Applications described by Sequential Function Chart (SFC) often being critical, we have studied the possibilities of program checking. In particular, physical time can be handled by SFC programs using temporisations, that’s why we are interested in the quantitative temporal properties. We have proposed a modeling of SFC in timed automata, a formalism which takes time into account. In this modeling, we use the physical constraints of the environment. Verification of properties can be carried out using the model-checker Kronos. We apply this method to SFC programs of average size like the one of the controlling part of the production cell Korso. The size of the programs remaining however a limit, we are studying the means of solving this problem.