Skip to main content
SpringerLink
Log in

Correct Real-Time Software for Programmable Logic Controllers

  • Chapter
  • First Online:
Correct System Design

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1710))

Abstract

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].

This work was partially funded by the German Ministry for Education and Research (BMBF), project UniForM, grant FKZ 01 IS 521 B3, and the Leibniz Programme of the German Research Council (DFG) under grant Ol 98/1-1.

Acknowledgements

The work described in this paper is motivated by my participation in the projects ProCoS (Provably Correct Systems [17]) and UniForM (Universal Workbench for Formal Methods [23]). I am indepted to H. Dierks, C. Dietz, H. Fleischhack and J. Tapken for their work on various aspects of the approach to real-time design described in this paper.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, D. Dill. A theory of timed automata. Theoret. Comput. Sci., 126, 1994, 283–235.

    Article  MathSciNet  Google Scholar 

  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. 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. 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. 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. 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. 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. 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. 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. 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.

    Chapter  Google Scholar 

  11. H. Dierks, J. Tapken. Tool-supported hierarchical design of distributed real-time systems. In: Proc. IEEE EuroMicro‘98, Berlin, 1998.

    Google Scholar 

  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. S. Fowler, A. Wellings. Formal analysis of a real-time kernel specification. In: [21] 440–458.

    Google Scholar 

  14. R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel (Eds.). Hybrid Systems. LNCS 736 (Springer-Verlag, 1993)

    Google Scholar 

  15. M.R. Hansen, Zhou Chaochen, Duration Calculus: Logical Foundations. Formal Aspects of Computing, 9 (1997) 283–330.

    MATH  Google Scholar 

  16. D. Harel. Statecharts: a visual formalism for complex systems. Science of Comp. Progr. (1997) 231–274.

    Google Scholar 

  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. C. Heitmeyer and D. Mandrioli (Eds.), Formal Methods for Real-Time Computing. Trends in Software, Vol.5, (Wiley, 1996).

    Google Scholar 

  19. IEC International Standard 1131-3, Programmable Controllers, Part 3, Programming Languages, 1993

    Google Scholar 

  20. ITU-T, ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU General Secretariat, Geneva, 1994.

    Google Scholar 

  21. B. Jonsson, J. Parrow (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 1135 (Springer-Verlag, 1996).

    Google Scholar 

  22. M. Joseph (Ed.). Real-time Systems-Specification, Verification and Analysis Prentice Hall, 1996.

    Google Scholar 

  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. H. Langmaack, W.-P. de Roever, J. Vytopil (Eds.). Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 863 (Springer-Verlag, 1994).

    MATH  Google Scholar 

  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.

    Article  MATH  Google Scholar 

  26. R.W. Lewis. Programming industrial control systems using IEC 1131-3. The Institution of Electrical Engineers, 1995.

    Google Scholar 

  27. S. Mauw, M.A. Reniers. An Algebraic Semantics of Basic Message Sequence Charts. The Computer Journal 37, No. 4 (1994) 269–277.

    Article  Google Scholar 

  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.

    Chapter  Google Scholar 

  29. E.-R. Olderog, A.P. Ravn, J.U. Skakkebæk. Refining system requirements to program specifications. In: [18] 107–134.

    Google Scholar 

  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.

    Article  Google Scholar 

  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. W. Reisig. Petri Nets-An Introduction. Springer-Verlag, 1985.

    Google Scholar 

  33. W.-P. de Roever, K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison (Cambridge, 1998).

    Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

  35. M. Schenke, Transformational design of real-time systems-part II: from program specifications to programs. Acta Informatica 36, 1999, 67–96.

    Article  MathSciNet  Google Scholar 

  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. Zhou Chaochen, C.A.R. Hoare, A.P. Ravn. A calculus of durations. Information Processing Letters, 40/5, 1991, 269–276.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Oldenburg, Postfach 2503, D-26111, Oldenburg, Germany

    Ernst-Rüdiger Olderog

Authors
  1. Ernst-Rüdiger Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fachbereich Informatik, Universität Oldenburg, Postfach 2503, D-26111, Oldenburg, Germany

    Ernst-Rüdiger Olderog

  2. Fachbereich Informatik, Universität Dortmund, Baroper Str. 301, D-44221, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Olderog, ER. (1999). Correct Real-Time Software for Programmable Logic Controllers. In: Olderog, ER., Steffen, B. (eds) Correct System Design. Lecture Notes in Computer Science, vol 1710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48092-7_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-48092-7_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66624-0

  • Online ISBN: 978-3-540-48092-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation