Analysis of Logic Controllers by Transformation of SFC into Timed Automata

This paper proposes an approach to connect Sequential Function Charts (SFC), an industrially recognized and used description of logic controllers, to algorithmic verification. Based on a rigorous syntactical and semantical definition of SFC, the paper describes a formal scheme to generate a corresponding model represented by synchronized Timed Automata (TA). The latter model can be composed with a plant model specified as timed or hybrid automata. In order to verify safety properties for the controlled system, existing algorithms for model checking can eventually be applied to the composition.