Analysis of Logic Controllers by Transformation of SFC into Timed Automata
Olaf Stursberg, Sven Lohmann · 2006
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.