Advertisement

A Unifying Semantics for Sequential Function Charts

  • Nanette Bauer
  • Ralf Huuck
  • Ben Lukoschus
  • Sebastian Engell
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)

Abstract

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.

Keywords

Transition System Operational Semantic Action Block State Transformation Discrete Event System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. 2.
    Anderson, S., Tourlas, K.: Design for proof: An approach to the design of domainspecific languages. Formal Aspects of Computing 10, 452–468 (1998)zbMATHCrossRefGoogle Scholar
  3. 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. 4.
    International Electrotechnical Commission, Technical Committee No. 65: Programmable Controllers – Programming Languages, IEC 61131-3. 2nd edn. (1998), Committee draft Google Scholar
  5. 5.
    International Electrotechnical Commission, Technical Committee No. 848: IEC 60848, Preparation of function charts for control systems (1992) Google Scholar
  6. 6.
    David, R., Alla, H.: Petri Nets & Grafcet. Prentice-Hall, Englewood Cliffs (1992)Google Scholar
  7. 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. 8.
    Bauer, N.: Formale Analyse von Sequential Function Charts. PhD thesis, Lehrstuhl für Anlagensteuerungstechnik, Universität Dortmund, Shaker Verlag, Aachen (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Nanette Bauer
    • 1
  • Ralf Huuck
    • 2
  • Ben Lukoschus
    • 3
  • Sebastian Engell
    • 4
  1. 1.BASF AktiengesellschaftLudwigshafenGermany
  2. 2.National ICT Australia Ltd (NICTA)The University of New South WalesSydneyAustralia
  3. 3.Institute of Computer Science and Applied MathematicsUniversity of KielKielGermany
  4. 4.Process Control Laboratory (BCI-AST)University of DortmundDortmundGermany

Personalised recommendations