Abstract
The applicability of model-checking is often restricted by the size of the considered system. To overcome this limitation, a number of techniques have been investigated. Prominent among these are data independence, abstraction, and compositionality. This paper presents a methodology based on deductive reasoning and model-checking which combines these techniques. As we show, the combination of abstraction and compositionality gives a significant added value to each of them in isolation. We substantiate the approach proving safety of a sliding window protocol of window size 16 using Spin and PVS.
This work has been partially supported by the Esprit-LTR project Vires.
Contact author.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Bouajjani, S. Bensalem, C. Loiseaux, and J. Sifakis. Property preserving simulations. In G. v. Bochmann and D. K. Probst, editors, CAV’92, volume663 of LNCS. Springer, 1992
R. Cardell-Oliver. The specification and verification of sliding window protocols. Technical Report 183, University of Cambridge, 1989.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, Los Angeles, CA. ACM, 1977.
E. M. Clarke and E. A. Emerson. Synthesis of synchronisation skeletons for branching time temporal logic. In D. Kozen, editor, Workshop on Logic of Programs1981, volume 131 ofLNCS. Springer, 1981.
E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. TOPLAS, 16(5):1512–1542, 1994.
D. Dams. Abstract interpretation and partition refinement for model che cking. PhD thesis, Technical University of Eindhoven, 1996.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL-, ECTL- and CTL-. In E.-R. Olderog, editor, Proceedings of PROCOMET’ 94. North-Holland, 1994.
I. Dravapoulos, N. Pronios, A. Andritsou, I. Piveropoulos, N. Passas, D. Skyrianoglou, G. Awater, J. Kruys, N. Nikaein, A. Enout, S. Decrauzat, T. Kaltenschnee, T. Schumann, J. Meierhofer, S. Thomel, and J. Mikkonen. The Magic WAND, Deliverable 3D5, Wireless ATM MAC, Final Report, 1998.
W.-P. de Roever, H. Langmaack, and A. Pnueli, editors. Compos’ 97, volume 1536of LNCS. Springer, 1998.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, University of Uppsala, 1987. Technical Report DoCS 87/09.
R. Kaivola. Using compositional preorders in the verification of sliding window protocol. In O. Grumberg, editor, Proceedings of CAV’ 97, volume 1256 of LNCS, pages 48–59. Springer, 1997.
P. Kelb. Abstraktionstechniken fur Automatische Verifikationsmethoden. PhD thesis, University of Oldenburg, 1995.
D. E. Knuth. Verification of link-level protocols. BIT, 21:31–36, 1981.
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes, the automata theoretic approach. Princeton Series in Computer Science. Princeton University Press, 1994.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995.
D. E. Long. Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon, 1993.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal veri-cation for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, 1995.
J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium on Programming, 1981.
J. L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in Xesar of the sliding window protocol. In PSTV VII. North-Holland, 1987.
A. U. Shankar and S. S. Lam. A stepwise refinement heuristics for protocol construction. TOPLAS, 14(3):417–461, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stahl, K., Baukus, K., Lakhnech, Y., Stefen, M. (1999). Divide, Abstract, and Model-Check. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds) Theoretical and Practical Aspects of SPIN Model Checking. SPIN 1999. Lecture Notes in Computer Science, vol 1680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48234-2_5
Download citation
DOI: https://doi.org/10.1007/3-540-48234-2_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66499-4
Online ISBN: 978-3-540-48234-5
eBook Packages: Springer Book Archive