Advertisement

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

  • Olaf Müller
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

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

Keywords

Model Checker Temporal Logic System Verification Proof Obligation High Order Logic 
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. 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. 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. 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. 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. 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. 6.
    F. Kröger. Temporal Logic of Programs. Springer-Verlag, 1987.Google Scholar
  7. 7.
    L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.CrossRefGoogle Scholar
  8. 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. 9.
    N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.Google Scholar
  10. 10.
    Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, NY, 1995.Google Scholar
  11. 11.
    S. Merz. Mechanizing TLA in Isabelle. In Workshop Verification in New Orientations, 1995. Technical Report, University Maribor.Google Scholar
  12. 12.
    O. Müller. Abstraction rules for I/O automata using temporal logic. 1998. in preparation.Google Scholar
  13. 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. 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. 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. 16.
    O. Müller, T. Nipkow, D. Oheimb, and O. Slotosch. HOLCF = HOL + LCF. J. Functional Programming, 1998. submitted.Google Scholar
  17. 17.
    L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  18. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Olaf Müller
    • 1
  1. 1.Institut für InformatikTechnische UniversitÄt MünchenMünchenGermany

Personalised recommendations