Skip to main content
SpringerLink
Log in
Book cover

Ausgezeichnete Informatikdissertationen 1999 pp 32–41Cite as

Specification and Verification of Polling Real-Time Systems

  • Chapter

Part of the book series: GI-Dissertationspreis ((GIDISS))

Abstract

Formal methods for real-time systems are an important topic of contemporary research. The aim is to cope with the additional complexity of “time” in specification and verification. In [Die99a] we present an approach to the correct design of real-time programs implemented on “Programmable Logic Controllers” (PLCs). This hardware executes repeatedly an application program whereas each cycle has an upper time bound. The central device in our approach is the notion of “PLC-Automaton” which provides an abstract view on PLC programs. For PLC-Automata the following results are presented in [Die99a]:

  1. 1.

    It is possible to generate PLC source code from a PLC-Automaton. Also constraints on both the speed of the PLC and on the accuracy of time measurement are derived.

  2. 2.

    A logical semantics in terms of Duration Calculus is developed. Since this semantics considers the cyclic behaviour, computation speed, and timer tolerances a realistic model of the real-world behaviour is given.

  3. 3.

    Several ways to compose PLC-Automata are defined and described semantically.

  4. 4.

    An alternative operational semantics in terms of Timed Automata is given. It is provably consistent with the Duration Calculus semantics. Hence, model-checking PLC-Automata is possible due to this semantics. Moreover, we examine techniques for building abstractions of these Timed Automata models.

  5. 5.

    A formal synthesis procedure for “Implementables”, a sublanguage of Duration Calculus, is derived that produces a PLC-Automaton implementing the Implementables-specification if and only if there exists an implementing PLC-Automaton.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   49.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   39.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In Fifth Annual IEEE Symp. on Logic in Computer Science, pages 414–425. IEEE Press, 1990.

    Google Scholar 

  2. R. Alur and D.L. Dill. A theory of timed automata. TCS, 126:183–235, 1994.

    Article  MathSciNet  MATH  Google Scholar 

  3. A. Benveniste and G. Berry. The Synchronous Approach to Reactive and Real-Time Systems. Proceedings of the IEEE, 79(9): 1270–1282, September 1991.

    Article  Google Scholar 

  4. J. Bowen, C.A.R. Hoare, H. Langmaack, E.-R. Olderog, and A.R Ravn. ProCoS II: A ProCos II Project Final Report, chapter 7, pages 76–99. Number 59 in Bulletin of the EATCS. European Association for Theoretical Computer Science, June 1996.

    Google Scholar 

  5. H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. In A.P. Ravn and H. Rischel, editors, FTRTFT’98, volume 1486 of LNCS, pages 29–40, Lyngby, Denmark, September 1998. Springer.

    Google Scholar 

  6. H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. In M. Bertran and T. Rus, editors, ARTS’97, volume 1231 of LNCS, pages 111–125, Mallorca, Spain, May 1997. Springer.

    Google Scholar 

  7. H. Dierks. Synthesising Controllers from Real-Time Specifications. In Tenth International Symposium on System Synthesis, pages 126–133. IEEE Computer Society, September 1997. short version of [Die99b].

    Google Scholar 

  8. H. Dierks. Specification and Verification of Polling Real-Time Systems. PhD thesis, University of Oldenburg, July 1999.

    Google Scholar 

  9. H. Dierks. Synthesizing Controllers from Real-Time Specifications. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(1):33–43, 1999.

    Article  Google Scholar 

  10. H. Dierks. A Process Algebra for Real-Time Programs. In FASE 2000: Fundamental Approaches to Software Engineering, LNCS. Springer, 2000. to appear.

    Google Scholar 

  11. H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. TCS, 2000. full version of [Die97a], to appear.

    Google Scholar 

  12. H. Dierks and J. Tapken. Tool-Supported Hierarchical Design of Distributed Real-Time Systems. In Proceedings of the 10th EuroMicro Workshop on Real Time Systems, pages 222–229. IEEE Computer Society, June 1998.

    Google Scholar 

  13. He Jifeng, 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 H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of LNCS, pages 288–335. Springer, 1994.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  15. B. Krieg-Brückner, J. Peleska, E.-R. Olderog, D. Balzer, and A. Baer. UniForM — Universal Formal Methods Workbench. In U. Grote and G. Wolf, editors, Statusseminar des BMBF Softwaretechnologie, pages 357–378. BMBF, Berlin, March 1996.

    Google Scholar 

  16. J. Tapken. Moby/PLC — A Design Tool for Hierarchical Real-Time Automata. In E. Astesiano, editor, Fundamental Approaches to Software Engineering, volume 1382 of LNCS, pages 326–329. Springer, 1998.

    Google Scholar 

  17. Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. IPL, 40/5:269–276, 1991.

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oldenburg, Germany

    Henning Dierks

Authors
  1. Henning Dierks
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. U Bonn, Deutschland

    Herbert Fiedler

  2. HU Berlin, Deutschland

    Oliver Günther

  3. U Passau, Deutschland

    Werner Grass

  4. TU Dresden, Deutschland

    Steffen Hölldobler

  5. U Saarbrücken, Deutschland

    Günter Hotz (Vorsitzender) (Vorsitzender)

  6. MedU Lübeck, Deutschland

    Rüdiger Reischuk

  7. U Marburg, Deutschland

    Bernhard Seeger

  8. U Konstanz, Deutschland

    Dorothea Wagner

Rights and permissions

Reprints and permissions

Copyright information

© 2000 B. G. Teubner GmbH, Stuttgart/Leipzig/Wiesbaden

About this chapter

Cite this chapter

Dierks, H. (2000). Specification and Verification of Polling Real-Time Systems. In: Fiedler, H., et al. Ausgezeichnete Informatikdissertationen 1999. GI-Dissertationspreis. Vieweg+Teubner Verlag. https://doi.org/10.1007/978-3-322-84823-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-322-84823-9_3

  • Publisher Name: Vieweg+Teubner Verlag

  • Print ISBN: 978-3-519-02650-1

  • Online ISBN: 978-3-322-84823-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation