A Model-Checking Approach to Safe SFCs
Ralf Huuck, Ben Lukoschus, Nanette Bauer · 2003
Sequential function charts (SFC) are a high-level graphical programming language for programmable logic controllers. Their main purpose is to provide a structure and organization of the control flow. Therefore, various features such as parallelism, priorities on branching transitions, and activity manipulations are incorporated. The syntactic rules for building SFCs are formally defined in IEC 61131-3. It is, however, still possible to derive SFCs from these rules whose structure do not make sense. In this work we give a characterization for socalled safe SFCs. Moreover, we present a semantic definition for them, as well as an algorithmic approach to automatically detect whether an SFC is safe or not.