Abstract
Model checking techniques have been successfully applied to the verification of correctness properties of complex hardware systems and communication protocols. This success has fueled the application of these techniques to software systems. To date, those efforts have been targeted at concurrent software whose complexity lies, primarily, in the large number of possible execution orderings of asynchronously executing program actions. In this paper, we apply existing model checking techniques to parameterizable implementations of container data structures. In contrast to most of the concurrent systems that have been studied in the model checking literature, the complexity of these implementations lies in their data structures and algorithms. We report our experiences model checking specifications of correctness properties of queue, stack and priority queue data structures implemented in Ada.
Supported in part by NSF under grants CCR-9703094 and CCR-9708184, by NSF and DARPA under grant CCR-9633388, and by NASA under grant NAG-02-1209.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J.-R. Abrial, E. Börger, and H. Langmaack. Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. Lecture Notes in Computer Science, 1165. Springer-Verlag, Oct. 1996.
G. Avrunin, U. Buy, J. Corbett, L. Dillon, and J. Wileden. Automated analysis of concurrent systems with the constrained expression toolset. IEEE Transactions on Software Engineering, 17(11):1204–1222, Nov. 1991.
J. Beidler. The Scranton generic data structure suite. ∣http://academic.uofs.edu/faculty/beidler/ADA/default.html—, 1996.
E. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. Long, K. McMillan, and L. Ness. Verification of the future-bus+ cache coherence protocol. Formal Methods in System Design, 6(2), 1995.
J. Corbett. Evaluating deadlockdetection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3), Mar. 1996.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.
D. Craigen, S. Gerhart, and T. Ralston. An international survey of industrial applications of formal methods. Technical report, National Institute of Standards and Technology, Mar. 1993.
J. Davies and J. Woodcock. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996.
D. Dill, A. Drexler, A. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522–525, July 1992.
M. Dwyer, G. Avrunin, and J. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999. to appear.
M. Dwyer and D. Schmidt. Limiting state explosion with filter-based refinement. In Proceedings of the 1st International Workshop on Verification, Abstract Interpretation and Model Checking, Oct. 1997.
M. B. Dwyer and C. S. Păsăreanu. Filter-based model checking of partial systems. In Proceedings of the Sixth ACM SIGSOFT Symposium on Foundations of Software Engineering, Nov. 1998.
M. B. Dwyer, C. S. Păsăreanu, and J. C. Corbett. Translating Ada programs for model checking: A tutorial. Technical Report 98-12, Kansas State University, Department of Computing and Information Sciences, 1998.
J. Hatcliff, M. B. Dwyer, and S. Laubach. Staging static analysis using abstractionbased program specialization. In LNCS 1490. Principles of Declarative Programming 10th International Symposium, PLILP’98, Sept. 1998.
D. Hoffman and R. Snodgrass. Trace specifications: Methodology and models. IEEE Transactions on Software Engineering, 14(9):1243–1252, Sept. 1988.
G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–294, May 1997.
C. Lewerentz and T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. Lecture Notes in Computer Science, 891. Springer-Verlag, Jan. 1995.
B. Liskov and J. V. Guttag. Abstraction and Specification in Program Development. The MIT Electrical Engineering and Computer Science Series. MIT Press, Cambridge, MA, 1986.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.
K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
G. Naumovich, L. Clarke, and L. Osterweil. Verification of communication protocols using data flow analysis. In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, Oct. 1996.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, pages 123–144. Springer-Verlag, 1985.
P. Wolper. Specifying interesting properties of programs in propositional temporal logics. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages, pages 184–193, St. Petersburg, Fla., Jan. 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dwyer, M.B., PĂsĂreanu, C.S. (2000). Model Checking Generic Container Implementations. In: Jazayeri, M., Loos, R.G.K., Musser, D.R. (eds) Generic Programming. Lecture Notes in Computer Science, vol 1766. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-39953-4_13
Download citation
DOI: https://doi.org/10.1007/3-540-39953-4_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41090-4
Online ISBN: 978-3-540-39953-7
eBook Packages: Springer Book Archive