Abstract
Recently, an active research topic in software verification is applying model checkers to programs, such as multi-threaded Java code. However, a program typically consists of more behaviors, such as operations on complicated data structures or implementation details which are typically made for some criteria like performance. A brute-force model extraction may produce a poor model for analysis engine. In this paper, we give examples to show how subtle changes in implementation may result in considerable differences in analysis, particularly to compositional analysis. Unfortunately, these implementation choices are made by programmers – people who typically do not possess the knowledge of verification. To mitigate such sensitivity, we advocate that verification tools should recognize and support abstract data types and, in the meantime, prohibit or suppress the use of array. Programming process behaviors with abstract data types can hide and converge the implementation choices. More importantly, abstract data types are informative. They provide essential information for tool automation to select a best implementation for analysis. In this paper, we describe the design and implementation of such a prototype tool which can parse systems written in Promela syntax.
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.
References
Avrunin, G.S., Corbett, J.C., Dwyer, M.B., Pasareanu, C.S., Siegel, S.F.: Comparing finite-state verification techniques for concurrent software. Technical Report UM-CS-1999-069, Dept. of CS, University of Massachusetts (November 1999) (in preparation)
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex lines. Communications of ACM 12(5), 260–261 (1969)
Bryant, R.E.: Graph-based algorithms for boolean function manipulations. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Cheng, Y.: Refactoring design models for inductive verification. In: Proceedings of International Symposium on Software Testing and Analysis (ISSTA 2002), Rome, Italy, July 2002, pp. 164–168 (2002)
Cheng, Y.-P., Young, M., Huang, C.-L., Pan, C.-Y.: Towards scalable compositional analysis by refactoring design models. In: Proceedings of the ACM SIGSOFT 2003 Symposium on the Foundations of Software Engineering, pp. 247–256 (2003)
Cheung, S.C., Giannakopoulou, D., Kramer, J.: Verification of liveness properties using compositional reachability analysis. In: 5th ACM SIGSOFT Symposium on Foundations of Software Engineering, Zurich, Switzerland, September 1997, pp. 227–243 (1997)
Cheung, S.C., Kramer, J.: Context constraints for compositional reachability analysis. ACM Transactions on Software Engineering and Methodology 5(4), 334–377 (1996)
Cheung, S.C., Kramer, J.: Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology 8, 49–78 (1999)
Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Proceedings of 4th IEEE Symposium on Logic in Computer Sciences, pp. 353–362. IEEE Computer Society Press, Los Alamitos (1989)
Corbett, J.C.: Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering 2(3), 161–180 (1996)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from java source code. In: International Conference on Software Engineering, pp. 439–448 (2000)
Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186–204. Springer, Heidelberg (1991)
Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA pathfinder. International Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997)
Holzmann, G.J.: Designing executable abstractions. In: Proceedings of the second workshop on formal methods in software practice, Clearwater Beach, Florida USA, March 1998, pp. 103–108 (1998)
Keller, R.K., Cameron, M., Taylor, R.N., Troup, D.B.: User interface development and software environments: The Chiron-1 system. In: Proceedings of the Thirteenth International Conference on Software Engineering, Austin, TX, May 1991, pp. 208–218 (1991)
Madelaine, E., de Simone, R.: The FC2 Reference Manual. Available by ftp from http://cma.cma.fr:pub/verif as file http://fc2refman.ps INRIA
McMillan, K.L.: Symbolic model checking. Kluwer Academic Publishers, Massachusetts (1993)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, New York (1980)
Richardson, D.J., Aha, S.L., O’Malley, T.O.: Specification-based test oracles for reactive systems. In: Proceedings of the Fourteenth International Conference on Software Engineering, Melbourne, Australia, May 1992, pp. 105–118 (1992)
Yeh, W.J., Young, M.: Re-designing tasking structure of Ada programs for analysis: A case study. Software Testing, Verification, and Reliability 4, 223–253 (1994)
Young, M., Taylor, R., Levine, D., Nies, K.A., Brodbeck, D.: A concurrency analysis tool suite for Ada programs: Rationale, design, and preliminary experience. ACM Transactions on Software Engineering and Methodology 4(1), 65–106 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cheng, YP. (2005). Crafting a Promela Front-End with Abstract Data Types to Mitigate the Sensitivity of (Compositional) Analysis to Implementation Choices. In: Godefroid, P. (eds) Model Checking Software. SPIN 2005. Lecture Notes in Computer Science, vol 3639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11537328_13
Download citation
DOI: https://doi.org/10.1007/11537328_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28195-5
Online ISBN: 978-3-540-31899-6
eBook Packages: Computer ScienceComputer Science (R0)