Skip to main content
SpringerLink
Log in

Verification of safety critical systems using TTM/RTTL

  • Conference paper
  • First Online:
Book cover Real-Time: Theory in Practice (REX 1991)

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

Abstract

This paper shows how real-time temporal logic can be used for the verification of safety-critical systems. Heuristics are provided that help the designer to construct a proof diagram that either facilitates the presentation of a proof of correctness, or provides a counterexample to indicate the invalidity of the specification that is being checked. The heuristics can be semi-automated using constraint logic programming languages because most of the reasoning does not involve the actual use of temporal logic. The type of reasoning employed in this paper is not limited to finite state systems, but can be used on infinite state systems as well. The heuristics are illustrated using a process control example.

This work is supported by the Natural Sciences and Engineering Research Council of Canada

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.M. Chandy and J. Misra. Parallel program design. Addison-Wesley, 1988.

    Google Scholar 

  2. D. Gries. The Science of Programming. Springer-Verlag, 1985.

    Google Scholar 

  3. F. Kroger. Temporal Logics of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1987.

    Google Scholar 

  4. Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proceedings of the Symposium on Principles of Programming Languages, pages 141–154, Austin, Texas, January 1983.

    Google Scholar 

  5. Z. Manna and A. Pnueli. Verification of concurrent programs: a temporal proof system. Technical report, Dept. of Computer Science, Stanford University, June 1983. See also Foundations of Computer Science IV, Amsterdam, Mathematical Center Tracts, pages 163–225, 1983.

    Google Scholar 

  6. J.S. Ostroff. Real-time computer control of discrete event systems modelled by extended state machines: a temporal logic approach. Technical Report 8618, Systems Control Group, Dept. of Electrical Engineering, University of Toronto, September 1986. revised January 1987.

    Google Scholar 

  7. J.S. Ostroff. Mechanizing the verification of real-time discrete systems. In Proceedings of the 15th Symposium on Microprocessing and Microprogramming. North-Holland, September 1989.

    Google Scholar 

  8. J.S. Ostroff. Temporal Logic for Real-Time Systems. Advanced Software Development Series. Research Studies Press Limited (distributed by John Wiley and Sons), England, 1989.

    Google Scholar 

  9. J.S. Ostroff. Deciding properties of timed transition models. IEEE Transactions on Parallel and Distributed Systems, 1(2):170–183, April 1990.

    Article  Google Scholar 

  10. J.S. Ostroff. A logic for real-time discrete event processes. IEEE Control Systems Magzine, June 1990.

    Google Scholar 

  11. J.S. Ostroff. Constraint logic programming for reasoning about discrete event processes. The Journal of Logic Programming, 1991. (In Press).

    Google Scholar 

  12. J.S. Ostroff. Systematic development of real-time discrete event systems. In Proceedings of the ECC91 European Control Conference, pages 522–533, Paris, France, July 1991. Hermes Press.

    Google Scholar 

  13. J.S. Ostroff. A verifier for real-time properties. Real-Time Journal, 1992. (In press).

    Google Scholar 

  14. J.S. Ostroff and W.M. Wonham. A temporal logic approach to real time control. In Proceedings of the 24th IEEE Conference on Decision and Control, pages 656–657, Florida, December 1985.

    Google Scholar 

  15. J.S. Ostroff and W.M. Wonham. A framework for real-time discrete event control. IEEE Transactions on Automatic Control, April 1990.

    Google Scholar 

  16. Amir Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In J. de Bakker, W.P de Roever, and G. Rozenburg, editors, Current trends in concurrency, LNCS 244. Springer-Verlag, 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, York University, 4700 Keele Street, M3J 1P3, North York, Ontario, Canada

    J. S. Ostroff

Authors
  1. J. S. Ostroff
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker C. Huizing W. P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ostroff, J.S. (1992). Verification of safety critical systems using TTM/RTTL. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds) Real-Time: Theory in Practice. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032008

Download citation

  • DOI: https://doi.org/10.1007/BFb0032008

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55564-3

  • Online ISBN: 978-3-540-47218-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation