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 semantics to include time, clocks, and timed actions. The presented semantics is general enough to comprise different existing interpretations while at the same time being adjustable to precisely represent each of them.
KeywordsTransition System Operational Semantic Action Block State Transformation Discrete Event System
Unable to display preview. Download preview PDF.
- 1.Jiang, J., Holding, D.: The formalisation and analysis of sequential function charts using a petri net approach. In: Proceedings of 13th World Congress of IFAC, pp. 513–518 (1996)Google Scholar
- 3.Bornot, S., Huuck, R., Lakhnech, Y., Lukoschus, B.: An abstract model for sequential function charts. In: Discrete Event Systems: Analysis and Control, Proceedings of WODES 2000: 5th Workshop on Discrete Event Systems, Ghent, Belgium, August 21-23. The Kluwer International Series in Engineering and Computer Science, pp. 255–264 (2000)Google Scholar
- 4.International Electrotechnical Commission, Technical Committee No. 65: Programmable Controllers – Programming Languages, IEC 61131-3. 2nd edn. (1998), Committee draft Google Scholar
- 5.International Electrotechnical Commission, Technical Committee No. 848: IEC 60848, Preparation of function charts for control systems (1992) Google Scholar
- 6.David, R., Alla, H.: Petri Nets & Grafcet. Prentice-Hall, Englewood Cliffs (1992)Google Scholar
- 7.Bauer, N., Treseler, H.: Vergleich der Semantik der Ablaufsprache nach IEC 61131-3 in unterschiedlichen Programmierwerkzeugen. GMA Kongress, 2001, Baden-Baden, Germany (2001)Google Scholar
- 8.Bauer, N.: Formale Analyse von Sequential Function Charts. PhD thesis, Lehrstuhl für Anlagensteuerungstechnik, Universität Dortmund, Shaker Verlag, Aachen (2004)Google Scholar