Skip to main content
SpringerLink
Log in

I/O automata and beyond: Temporal logic and abstraction in Isabelle

  • Refereed Papers
  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 1998)

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

Included in the following conference series:

Abstract

We describe a verification framework for I/O automata in Isabelle. It includes a temporal logic, proof support for showing implementation relations between live I/O automata, and a combination of Isabelle with model checking via a verified abstraction theory. The underlying domain-theoretic sequence model turned out to be especially adequate for these purposes. Furthermore, using a tailored combination of Isabelle's logics HOL and HOLCF we achieve two complementary goals: expressiveness for proving meta theory (HOLCF) and simplicity and efficiency for system verification (HOL).

Research supported by BMBF, KorSys

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. M. Archer and C. Heitmeyer. Human-style theorem proving using PVS. In E. Gunter, editor, Proc. 10th Int. Conf. on Theorem Proving in Higher Order Logics (TPHOL'97), volume 1275 of Lecture Notes in Computer Science, pages 33–48. Springer-Verlag, 1997.

    Google Scholar 

  2. A. Biere. Μcke — Efficient Μ-calculus model checking. In O. Grumberg, editor, Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 468–471. Springer-Verlag, 1997.

    Google Scholar 

  3. N. BjØrner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H. B. Sipma, and T. E. Uribe. STeP: deductive-algorithmic verification of reactive and real-time systems. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification: 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 415–418. Springer-Verlag, 1996.

    Google Scholar 

  4. M. Devillers, D. Griffioen, and O. Müller. Possibly infinite sequences in theorem provers: A comparative study. In E. Gunter, editor, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOL'97), volume 1275 of Lecture Notes in Computer Science, pages 89–104. Springer-Verlag, 1997.

    Google Scholar 

  5. R. Gawlick, R. Segala, J. Sogaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Technical Report MIT/LCS/TR-587, Laboratory for Computer Science, MIT, Cambridge, MA, December 1993.

    Google Scholar 

  6. F. Kröger. Temporal Logic of Programs. Springer-Verlag, 1987.

    Google Scholar 

  7. L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

    Article  Google Scholar 

  8. T. Långbacka. A HOL formalisation of the Temporal Logic of Actions. In T. Melham and J. Camilleri, editors, Proc. 7th Int. Workshop on Higher Order Logic Theorem Provers and Applications, volume 859 of Lecture Notes in Computer Science, pages 332–347. Springer-Verlag, 1994.

    Google Scholar 

  9. N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.

    Google Scholar 

  10. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, NY, 1995.

    Google Scholar 

  11. S. Merz. Mechanizing TLA in Isabelle. In Workshop Verification in New Orientations, 1995. Technical Report, University Maribor.

    Google Scholar 

  12. O. Müller. Abstraction rules for I/O automata using temporal logic. 1998. in preparation.

    Google Scholar 

  13. O. Müller. A Verification Environment for I/O Automata based on formalized Meta-Theory. PhD thesis, Institut für Informatik, Technische UniversitÄt München, 1998.

    Google Scholar 

  14. O. Müller and T. Nipkow. Combining model checking and deduction for I/O-automata. In Proc. 1st Workshop Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 1995.

    Google Scholar 

  15. O. Müller and T. Nipkow. Traces of I/O-automata in Isabelle/HOLCF. In Proc. 7th Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'97), volume 1214 of Lecture Notes in Computer Science, pages 580–595. Springer-Verlag, 1997.

    Google Scholar 

  16. O. Müller, T. Nipkow, D. Oheimb, and O. Slotosch. HOLCF = HOL + LCF. J. Functional Programming, 1998. submitted.

    Google Scholar 

  17. L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

  18. J. F. Soegaard-Andersen, S. J. Garland, J. V. Guttag, N. A. Lynch, and A. Pogosyants. Computer-assisted simulation proofs. In C. Courcoubetis, editor, Proc. 5th Int. Conf. Computer-Aided Verificatio (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 305–319. Springer-Verlag, 1993.

    Google Scholar 

  19. J. Wright. Mechanising the Temporal Logic of Actions in HOL. In M. Archer, J. Joyce, K. Levitt, and P. Windley, editors, Proc. 1991 Int. Workshop on the HOL Theorem Proving System and its Applications, pages 155–159. IEEE Computer Society Press, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische UniversitÄt München, 80290, München, Germany

    Olaf Müller

Authors
  1. Olaf Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jim Grundy Malcolm Newey

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Müller, O. (1998). I/O automata and beyond: Temporal logic and abstraction in Isabelle. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055145

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64987-8

  • Online ISBN: 978-3-540-49801-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation