A Unifying Semantics for Sequential Function Charts

Programmable Logic Controllers (PLC) are widely used as device controllers for assembly lines, chemical processes, or power plants. Sequential Function Charts (SFC) form one of the main programming languages for PLCs and, therefore, the correctness of the PLC software implemented as SFCs is crucial for a safe operation of the controlled process. A prerequisite for reasoning about program correctness is a clear understanding of the program semantics. As we show in this work, this is currently not the case for SFCs. Although syntactically specified in the IEC 61131-3 standard, SFCs lack an unambiguous, complete semantic description. We point out a number of problems and explain how these lead to different interpretations in commercial programming environments. To remedy this situation we introduce a parameterized formal semantics for SFCs including many high-level programming features such as parallelism, hierarchy, actions and activity manipulation. Moreover, we show how to extend the...

• Type: Conference
• Year: 2004
• Where: DFG
• Authors: Nanette Bauer, Ralf Huuck, Ben Lukoschus, Sebastian Engell
• Keywords: DFG 2004, Parameterized Formal Semantics, Programmable Logic Controllers, Semantics