Abstract
Modeling software features with model programs in C# is a way of formalizing software requirements that lends itself to automated analysis such as model-based testing. Unordered structures like sets and maps provide a useful abstract view of system state within a model program and greatly reduce the number of states that must be considered during analysis. Similarly, a technique called linearization reduces the number of states that must be considered by identifying isomorphic states, or states that are identical except for reserve element choice (such as the choice of object IDs for instances of classes). Unfortunately, linearization does not work on unordered structures such as sets. The problem turns into graph isomorphism, for which no polynomial time solution is known. In this paper we discuss the issue of state isomorphism in the presence of unordered structures and give a practical approach that overcomes some of the algorithmic limitations.
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
Blass, A., Gurevich, Y.: Background, reserve, and gandy machines. In: Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, London, UK, pp. 1–17. Springer-Verlag, Heidelberg (2000)
Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN Model Checking and Software Verification. LNCS, vol. 1885, pp. 1–19. Springer, Heidelberg (2000)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. SIGSOFT Softw. Eng. Notes 27(4), 123–133 (2002)
Campbell, C., Veanes, M.: State exploration with multiple state groupings. In: Beauquier, D., Börger, E., Slissenko, A. (eds.) 12th International Workshop on Abstract State Machines, ASM’05, pp. 119–130. Laboratory of Algorithms, Complexity and Logic, Créteil, France (March 2005)
Darga, P.T., Boyapati, C.: Efficient software model checking of data structure properties. In: OOPSLA ’06. Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pp. 363–382. ACM Press, New York, NY, USA (2006)
Demartini, C., Iosif, R., Sisto, R.: dSPIN: A dynamic extension of SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) Theoretical and Practical Aspects of SPIN Model Checking. LNCS, vol. 1680, pp. 261–276. Springer, Heidelberg (1999)
Dill, D.L.: The Murphi verification system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)
Fortin, S.: The graph isomorphism problem (1996)
Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: ISSTA’02. Software Engineering Notes, vol. 27, pp. 112–122. ACM Press, New York (2002)
Grieskamp, W., Tillmann, N., Schulte, W.: XRT — exploring runtime for.Net architecture and applications. Electr. Notes Theor. Comput. Sci. 144(3), 3–26 (2006)
Gurevich, Y.: Specification and Validation Methods. In: Evolving Algebras 1993: Lipari Guide (chapter), pp. 9–36. Oxford University Press, Oxford (1995)
Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. STTT 6(4), 302–319 (2004)
Ip, C.N., Dil, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1-2), 41–75 (1996)
Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-based Software Testing and Analysis with C#. Cambridge University Press (Forthcoming 2007)
Luks, E.M.: Isomorphism of graphs of bounded valence can be tested in polynomial time. J. Comput. Syst. Sci. 25(1), 42–65 (1982)
McKay, B.D.: Practical graph isomorphism. Congressus Numerantium 30, 45–87 (1981)
Messmer, B.T.: Efficient graph matching algorithms (1995)
Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3), 8 (2006)
Musuvathi, M., Dill, D.L.: An incremental heap canonicalization algorithm. In: Godefroid, P. (ed.) Model Checking Software. LNCS, vol. 3639, Springer, Heidelberg (2005)
Robby, M., Dwyer, B., Hatcliff, J.: Domain-specific model checking using the bogor framework. In: ASE ’06. Proceedings of the 21st IEEE International Conference on Automated Software Engineering (ASE’06), pp. 369–370. IEEE Computer Society, Washington, DC, USA (2006)
SpecExplorer (2006), http://research.microsoft.com/SpecExplorer
Ullmann, J.R.: An algorithm for subgraph isomorphism. J. ACM 23(1), 31–42 (1976)
Utting, M., Legeard, B.: Practical Model-Based Testing - A tools approach. Elsevier, Amsterdam (2006)
Veanes, M., Campbell, C., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N.: Model-based testing of object-oriented reactive systems with Spec Explorer, Tech. Rep. MSR-TR-2005-59, Microsoft Research. Preliminary version of a book chapter in the forthcoming text book Formal Methods and Testing (2005)
Veanes, M., Campbell, C., Schulte, W.: Composition of model programs. In: The current proceedings (2007)
Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC/FSE-13. Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 273–282. ACM Press, New York, NY, USA (2005)
Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: A framework for generating object-oriented unit tests using symbolic execution. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 365–381. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Veanes, M., Ernits, J., Campbell, C. (2007). State Isomorphism in Model Programs with Abstract Data Structures. In: Derrick, J., Vain, J. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2007. FORTE 2007. Lecture Notes in Computer Science, vol 4574. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73196-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-73196-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73195-5
Online ISBN: 978-3-540-73196-2
eBook Packages: Computer ScienceComputer Science (R0)