Abstract
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.
Research supported by DFG, Leibniz Programm.
Research supported by ESPRIT BRA 6453, Types.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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.
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.
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.
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.
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.
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.
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.
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.
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.
P. Herrmann and H. Krumm. Report on analysis and verification techniques. Technical Report 485, Fachbereich Informatik, Universität Dortmund, 1993.
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.
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.
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.
N. Lynch and M. Tuttle. An introduction to Input/Output automata. CWI Quarterly, 2(3):219–246, 1989.
T. Nipkow and K. Slind. I/O automata in Isabelle/HOL. In Proc. TYPES Workshop 1994, Lect. Notes in Comp. Sci. Springer-Verlag, 1995.
K. Sabnani. An algorithmic technique for protocol verification. IEEE Transactions on Communications, 36(8):924–930, 1988.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, O., Nipkow, T. (1995). Combining model checking and deduction for I/O- automata. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1995. Lecture Notes in Computer Science, vol 1019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60630-0_1
Download citation
DOI: https://doi.org/10.1007/3-540-60630-0_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60630-7
Online ISBN: 978-3-540-48509-4
eBook Packages: Springer Book Archive