Combining model checking and deduction for I/O- automata

  • Olaf Müller
  • Tobias Nipkow
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)


We propose a combination of model checking and interactive theorem proving where the theorem prover is used to represent finite and infinite state systems, reason about them compositionally and reduce them to small finite systems by verified abstractions. As an example we verify a version of the Alternating Bit Protocol with unbounded lossy and duplicating channels: the channels are abstracted by interactive proof and the resulting finite state system is model checked.


Model Check Theorem Prover State Component Interactive Proof Interactive Theorem 
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.


  1. [1]
    P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In Proc. 8th IEEE Symp. Logic in Computer Science, pages 160–170. IEEE Press, 1993.Google Scholar
  2. [2]
    S. Aggarwal, C. Courcoubetis, and P. Wolper. Adding liveness properties to coupled finite-state machines. ACM Transactions on Programming Languages and Systems, 12(2):303–339, 1990.Google Scholar
  3. [3]
    K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmission over half-duplex lines. Communications of the ACM, 12(5):260–261, 1969.Google Scholar
  4. [4]
    E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Proc. 19th ACM Symp. Principles of Programming Languages, pages 343–354. ACM Press, 1992.Google Scholar
  5. [5]
    D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving ∀CTL*, ∃CTL* and CTL*. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi (PROCOMET), pages 573–593. North-Holland, 1994.Google Scholar
  6. [6]
    J.-C. Fernandez and L. Mounier. “On the Fly” verification of behavioural equivalences and preorders. In K. G. Larsen, editor, Proc. 3rd Workshop Computer Aided Verification, volume 575 of Lect. Notes in Comp. Sci., pages 181–191. Springer-Verlag, 1992.Google Scholar
  7. [7]
    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. Extended abstract in Proceedings ICALP'94.Google Scholar
  8. [8]
    S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In C. Courcoubetis, editor, Computer Aided Verification, volume 697 of Lect. Notes in Comp. Sci., pages 71–84. Springer-Verlag, 1993.Google Scholar
  9. [9]
    P. Herrmann, T. Kraatz, H. Krumm, and M. Stange. Automated verification of refinements of concurrent and distributed systems. Technical Report 541, Fachbereich Informatik, Universität Dortmund, 1994.Google Scholar
  10. [10]
    P. Herrmann and H. Krumm. Report on analysis and verification techniques. Technical Report 485, Fachbereich Informatik, Universität Dortmund, 1993.Google Scholar
  11. [11]
    H. Hungar. Combining model checking and theorem proving to verify parallel processes. In C. Courcoubetis, editor, Computer Aided Verification, volume 697 of Lect. Notes in Comp. Sci., pages 154–165. Springer-Verlag, 1993.Google Scholar
  12. [12]
    R. Kurshan. Reducibility in analysis of coordination. In K. Varaiya, editor, Discrete Event Systems: Models and Applications, volume 103 of Lecture Notes in Control and Information Science, pages 19–39. Springer-Verlag, 1987.Google Scholar
  13. [13]
    N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. Technical Report MIT/LCS/TR-387, Laboratory for Computer Science, MIT, Cambridge, MA., 1987.Google Scholar
  14. [14]
    N. Lynch and M. Tuttle. An introduction to Input/Output automata. CWI Quarterly, 2(3):219–246, 1989.Google Scholar
  15. [15]
    T. Nipkow and K. Slind. I/O automata in Isabelle/HOL. In Proc. TYPES Workshop 1994, Lect. Notes in Comp. Sci. Springer-Verlag, 1995.Google Scholar
  16. [16]
    K. Sabnani. An algorithmic technique for protocol verification. IEEE Transactions on Communications, 36(8):924–930, 1988.Google Scholar
  17. [17]
    P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. Principles of Programming Languages, pages 184–193. ACM Press, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Olaf Müller
    • 1
  • Tobias Nipkow
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations