Correct Real-Time Software for Programmable Logic Controllers

  • Ernst-Rüdiger Olderog
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)


We present an approach to the design of correct real-time software for Programmable Logic Controllers (PLCs), a widespread hardware platform in the area of traffic and automation control [19,26]. Requirements are formulated in a graphical formalism called Constraint Diagrams (CDs) [12]. A CD consists of waveforms that describe the timewise behaviour of observables and of arrows that describe the timed interdependencies between these waveforms. Design specifications are formulated as so-called PLC-Automata [7]. These can be understood as a special class of timed automata that model in an abstract way the cyclic behaviour of PLCs. Programs are formulated in ST (Structured Text), a dedicated programming language for PLCs. PLC-Automata can be easily compiled into ST code.

The semantic link between CDs and PLC-Automata is stated in terms of the Duration Calculus [37], a logic and calculus for specifying realtime behaviour. This enables us to formally establish the correctness of designs with respect to the requirements. The approach is illustrated by a case study defined by an industrial partner engaged in designing railway signalling systems [23]. It is supported by a tool called Moby/plc [11].


Programmable Logic Controller State Assertion Message Sequence Chart Duration Term Duration Calculus 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Alur, D. Dill. A theory of timed automata. Theoret. Comput. Sci., 126, 1994, 283–235.CrossRefMathSciNetGoogle Scholar
  2. 2.
    R. Alur, G.J. Holzmann, D. Peled. An analyzer for message sequence charts. In: T. Margaria and B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems. LNCS 1055 (Springer-Verlag, (1996) 35–48.Google Scholar
  3. 3.
    R.J.R. Back. Refinement calculus, part II: parallel and reactive Programs. In J.W. de Bakker, W.P. de Roever and G. Rozenberg (Eds.), Stepwise Refinement of Distributed Systems-Models, Formalisms, Correctness. LNCS 430 (Springer-Verlag, 1990) 67–93.Google Scholar
  4. 4.
    J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi. Uppaal a tool suite for automatic verification of real-time systems. In: Proc. 4th DIMACS Workshop on Verification and Control of Hybrid Systems. New Brunswick, New Jersey, Oct. 1995.Google Scholar
  5. 5.
    T. Bienmüller, J. Bohn, H. Brinkmann, U. Brockmeyer, W. Damm, H. Hungar, P. Jansen. Verification of Automotive Control Units. This volume.Google Scholar
  6. 6.
    C. Dawsa, A. Olivero, S. Tripakis, S. Yovine. The tool Kronos. In: R. Alur, T.A. Henzinger, E.D. Sontag (Eds.), Hybrids Systems III-Verification and Control. LNCS 1066 (Springer-Verlag, 1996).Google Scholar
  7. 7.
    H. Dierks. PLC-automata: a new class of implementable real-time automata. In: M. Bertran and T. Rus (Eds.), Transformation-Based Reactive Systems Development. LNCS 1231 (Springer-Verlag, 1997) 111–125. (Revised version to appear in TCS)Google Scholar
  8. 8.
    H. Dierks. Synthesising controllers from real-time specifications. In: Tenth In-ternational Symposium on System Synthesis (IEEE CS Press, September 1997) 126–133.Google Scholar
  9. 9.
    H. Dierks, C. Dietz. Graphical specification and reasoning: case study “Generalized Railroad Crossing”. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Formal Methods: Their Industrial Application and Strengthened Foundations (FME‘97), LNCS 1313 (Springer-Verlag, 1997) 20–39.Google Scholar
  10. 10.
    H. Dierks, A. Fehnker, A. Mader, F.W. Vaandrager. Operational and logical semantics for polling real-time systems. In A.P. Ravn, H. Rischel, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT‘98), Lecture Notes in Computer Science volume 1486, pages 29–40, Springer-Verlag, 1998.CrossRefGoogle Scholar
  11. 11.
    H. Dierks, J. Tapken. Tool-supported hierarchical design of distributed real-time systems. In: Proc. IEEE EuroMicro‘98, Berlin, 1998.Google Scholar
  12. 12.
    C. Dietz, Graphical formalization of real-time requirements. In B. Jonsson and J. Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1135 (Springer-Verlag, 1996) 366–385.Google Scholar
  13. 13.
    S. Fowler, A. Wellings. Formal analysis of a real-time kernel specification. In: [21] 440–458.Google Scholar
  14. 14.
    R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel (Eds.). Hybrid Systems. LNCS 736 (Springer-Verlag, 1993)Google Scholar
  15. 15.
    M.R. Hansen, Zhou Chaochen, Duration Calculus: Logical Foundations. Formal Aspects of Computing, 9 (1997) 283–330.zbMATHGoogle Scholar
  16. 16.
    D. Harel. Statecharts: a visual formalism for complex systems. Science of Comp. Progr. (1997) 231–274.Google Scholar
  17. 17.
    Jifeng He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.-R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn, and H. Rischel. Provably correct systems. In: [24] 288–335.Google Scholar
  18. 18.
    C. Heitmeyer and D. Mandrioli (Eds.), Formal Methods for Real-Time Computing. Trends in Software, Vol.5, (Wiley, 1996).Google Scholar
  19. 19.
    IEC International Standard 1131-3, Programmable Controllers, Part 3, Programming Languages, 1993Google Scholar
  20. 20.
    ITU-T, ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU General Secretariat, Geneva, 1994.Google Scholar
  21. 21.
    B. Jonsson, J. Parrow (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 1135 (Springer-Verlag, 1996).Google Scholar
  22. 22.
    M. Joseph (Ed.). Real-time Systems-Specification, Verification and Analysis Prentice Hall, 1996.Google Scholar
  23. 23.
    B. Krieg-Brückner, J. Peleska, E.-R. Olderog, D. Balzer, A. Baer. UniForM-Universal Formal Methods Workbench. In: U. Grote and G. Wolf (Eds.), Statusseminar des BMBF Softwaretechnologie (BMBF, Berlin, 1996) 357–377.Google Scholar
  24. 24.
    H. Langmaack, W.-P. de Roever, J. Vytopil (Eds.). Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 863 (Springer-Verlag, 1994).zbMATHGoogle Scholar
  25. 25.
    K.G. Larsen, B. Steffen, C. Weise. Countinuous modeling of real time and hybrid systems: from concepts to tools. Software Tools for Technology Transfer (STTT) 1, 1997, 64–85.zbMATHCrossRefGoogle Scholar
  26. 26.
    R.W. Lewis. Programming industrial control systems using IEC 1131-3. The Institution of Electrical Engineers, 1995.Google Scholar
  27. 27.
    S. Mauw, M.A. Reniers. An Algebraic Semantics of Basic Message Sequence Charts. The Computer Journal 37, No. 4 (1994) 269–277.CrossRefGoogle Scholar
  28. 28.
    E.-R. Olderog, H. Dierks, Decomposing real-time specifications. In H. Langmaack, A. Pnueli, W.-P. de Roever, editors, Compositionality: The Significant Difference, LNCS (Springer-Verlag, 1998) 465–489.CrossRefGoogle Scholar
  29. 29.
    E.-R. Olderog, A.P. Ravn, J.U. Skakkebæk. Refining system requirements to program specifications. In: [18] 107–134.Google Scholar
  30. 30.
    A.P. Ravn, H. Rischel, K.M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, vol. 19,1 (1993) 41–55.CrossRefGoogle Scholar
  31. 31.
    A.P. Ravn. Design of Embedded Real-Time Computing Systems. Thesis for the Doctor of Technics. Technical Report ID-TR: 1995-170, Technical University of Denmark, 1995.Google Scholar
  32. 32.
    W. Reisig. Petri Nets-An Introduction. Springer-Verlag, 1985.Google Scholar
  33. 33.
    W.-P. de Roever, K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison (Cambridge, 1998).Google Scholar
  34. 34.
    M. Schenke, E.-R. Olderog, Transformational design of real-time systems-part I: from requirements to program specifications. Acta Informatica 36, 1999, 1–65.zbMATHCrossRefMathSciNetGoogle Scholar
  35. 35.
    M. Schenke, Transformational design of real-time systems-part II: from program specifications to programs. Acta Informatica 36, 1999, 67–96.CrossRefMathSciNetGoogle Scholar
  36. 36.
    R. Schlör, W. Damm. Specification and verification of system level hardware designs using timing diagrams. In Proc. European Conf. on Design Automation, Paris, 1993.Google Scholar
  37. 37.
    Zhou Chaochen, C.A.R. Hoare, A.P. Ravn. A calculus of durations. Information Processing Letters, 40/5, 1991, 269–276.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Ernst-Rüdiger Olderog
    • 1
  1. 1.Fachbereich InformatikUniversität OldenburgGermany

Personalised recommendations