Advertisement

Abstract

A formal framework for specifying and verifying real-time systems with a continuous environment is presented. Metric Temporal Logic (MTL) is extended with a duration concept similar to the one in the Duration Calculus (DC). The resulting logic, called MTL-∫, is compared with DC and is shown to be more expressive. Axioms for MTL-∫ and a sound rule to prove that a timed transition system satisfies a limited-duration property are given.

Keywords

Hybrid System Temporal Logic Safety Property Liveness Property Proof Rule 
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.
    M. Abadi and L. Lamport, An old-fashioned recipe for real-time, in: J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, ed., Proc. of the REX Workshop “Real-Time: Theory in Practice”, LNCS 600 (Springer-Verlag 1992) 1–27.Google Scholar
  2. 2.
    B. Alpern and F.B. Schneider, Defining liveness, Inf. Proc. Letters 21 (1985) 181–185.Google Scholar
  3. 3.
    R. Alur and T.A. Henzinger, Real-time logics: Complexity and expressiveness, in: Proc. of the 5th IEEE Symp. Logic in Comp. Sci. (IEEE Computer Society Press, 1990) 390–401.Google Scholar
  4. 4.
    R. Alur and T.A. Henzinger, Logics and models of real-time: A survey. in: J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, ed., Proc. of the REX Workshop ”Real-Time: Theory in Practice”, LNCS 600 (Springer-Verlag 1992) 74–106.Google Scholar
  5. 5.
    H. Barringer, R. Kuiper, and A. Pnueli, Now you may compose temporal logic specifications, in: Proc. of the 16th Annual ACM Symp. on Theory of Comp. (1984) 51–63.Google Scholar
  6. 6.
    H. Barringer, R. Kuiper, and A. Pnueli, A really abstract concurrent model and its temporal logic, in: Proc. of the 13th ACM Symp. on Princ. of progr. Lang. (1986) 173–183.Google Scholar
  7. 7.
    H.S. Carslaw, An introduction to the Theory of Fourier's Series and Integrals (Dover Publications, Inc., New York, 1950.)Google Scholar
  8. 8.
    Zhou Chaochen, M.R. Hansen, A.P. Ravn, and H. Rischel, Duration specifications for shared processors, in: J. Vytopil, ed., Second International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, The Netherlands, LNCS 571 (Springer-Verlag 1992) 21–32.Google Scholar
  9. 9.
    Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn, A calculus of durations, Inf. Proc. Letters 40(5) (1991) 269–276.Google Scholar
  10. 10.
    Zhou Chaochen, A.P. Ravn, and M.R. Hansen, An extended duration calculus for hybrid real-time systems, in: R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, ed., Workshop on hybrid systems, LNCS 736 (Springer-Verlag 1993) 36–59.Google Scholar
  11. 11.
    M.R. Hansen and Zhou Chaochen, Semantics and completeness of duration calculus, in: J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, ed., Proc. of the REX Workshop ”Real-Time: Theory in Practice”, LNCS 600 (Springer-Verlag 1992) 209–225.Google Scholar
  12. 12.
    T.A. Henzinger, Z. Manna, and A. Pnueli, Temporal proof methodologies for real-time, in: Proc. of the 18th ACM Symp. on Princ. of Progr. Lang. (1991) 353–366.Google Scholar
  13. 13.
    T.A. Henzinger, Z. Manna, and A. Pnueli, Timed transition systems, in: J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, ed., Proc. of the REX Workshop ”Real-Time: Theory in Practice”, LNCS 600 (Springer-Verlag 1992) 226–251.Google Scholar
  14. 14.
    J. Hooman, Specification and Compositional Verification of Real-Time Systems, LNCS 558 (Springer-Verlag 1991).Google Scholar
  15. 15.
    R. Koymans, Specifying message passing and time-critical systems with temporal logic, LNGS 651 (Springer-Verlag 1992).Google Scholar
  16. 16.
    Y. Lakhneche and J. Hooman, Metric Temporal Logic with Durations, in: A. Pnueli and J. Sifakis, ed., Theoretical Computer Science, special issue on hybrid systems (1994). To appear.Google Scholar
  17. 17.
    L. Lamport, The Temporal Logic of Actions, Technical report, Digital Equipment Corporation, Systems Research Center, 1991.Google Scholar
  18. 18.
    L. Lamport, Hybrid systems in TLA+, in: R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, ed., Workshop on hybrid systems, LNCS 736 (Springer-Verlag 1993) 77–102.Google Scholar
  19. 19.
    O. Maler, Z. Manna, and A Pnueli, From timed to hybrid systems, in: J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, ed., Proc. of the REX Workshop ”Real-Time: Theory in Practice”, LNCS 600 (Springer-Verlag 1992) 447–484.Google Scholar
  20. 20.
    Z. Manna and A. Pnueli, Completing the temporal picture, in: 16th EATCS ICALP (1989).Google Scholar
  21. 21.
    K. Marzullo, F.B. Schneider, and N. Budhiraja, Derivation of sequential, real-time process-control programs, in: A.M. van Tilborg and G.M. Koob, ed., Foundations of Real-Time Computing: Formal Specifications and Methods, (Kluver Academic Publishers 1991) chapter2, 39–54.Google Scholar
  22. 22.
    X. Nicollin, J Sifakis, and S. Yovine, From ATP to timed graphs and hybrid systems, in: Acta Informatica 30(2) (1993) 181–202.Google Scholar
  23. 23.
    B. Moszkowski, A temporal logic for multilevel reasoning about hardware, in: IEEE Computer 18(2) (1985) 10–19.Google Scholar
  24. 24.
    A. Pnueli, System Specification and Refinement in Temporal Logic, in: Foundations of Software Technology and Theoretical Computer Science, LNCS Vol. 652 (Springer-Verlag 1993) 1–38.Google Scholar
  25. 25.
    J.S. Ostrolf. Temporal logic for real-time systems, (Research Studies Press, 1989).Google Scholar
  26. 26.
    A. Pnueli, The temporal logic of programs, in: Proc. 18th IEEE Symp. on Found. of Comp. Sci., (1977) 46–57.Google Scholar
  27. 27.
    P. Prior, Past, Present, and Future (Oxford University Press 1967).Google Scholar
  28. 28.
    A.P. Ravn, H. Rischel, and K.M. Hansen, Specifying and verifying requirements of real-time systems, in: IEEE Transaction on Software Engeneering (January 1993).Google Scholar
  29. 29.
    J. U. SkakkebÆk, Liveness and fairness in a Duration Calculus, Proc. CONCUR '94, LNCS, (Springer-Verlag 1994). To appear.Google Scholar
  30. 30.
    Y. Venema, A modal logic for chopping intervals, in: Journal of Logic Computation, 1(4) (1991) 453–476.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Yassine Lakhneche
    • 1
  • Jozef Hooman
    • 2
  1. 1.Institut für Informatik und Praktische MathematikChristian-Albrechts-UniversitÄt zu KielKielGermany
  2. 2.Dept. of Mathematics and Computing ScienceEindhoven University of TechnologyMB EindhovenThe Netherlands

Personalised recommendations