Abstract
Model programs represent transition systems that are used to specify expected behavior of systems at a high level of abstraction. The main application area is application-level network protocols or protocol-like aspects of software systems. Model programs typically use abstract data types such as sets and maps, and comprehensions to express complex state updates. Such models are mainly used in model-based testing as inputs for test case generation and as oracles during conformance testing. Correctness assumptions about the model itself are usually expressed through state invariants. An important problem is to validate the model prior to its use in the above-mentioned contexts. We introduce a technique of using Satisfiability Modulo Theories or SMT to perform bounded reachability analysis of a fragment of model programs. We use the Z3 solver for our implementation and benchmarks, and we use AsmL as the modeling language. The translation from a model program into a verification condition of Z3 is incremental and involves selective quantifier instantiation of quantifiers that result from the comprehension expressions.
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
Spec Explorer, http://research.microsoft.com/specexplorer
Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 146–162. Springer, Heidelberg (2006)
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Blass, A., Gurevich, Y.: Background, reserve, and Gandy machines. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 1–17. Springer, Heidelberg (2000)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)
Brown, G.M., Pike, L.: Easy parameterized verification of biphase mark and 8N1 protocols. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 58–72. Springer, Heidelberg (2006)
de Moura, L., Bjørner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007)
de Moura, L., Bjørner, N.: Model-based theory combination. In: 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), Berlin, Germany, July 2007, pp. 46–57 (2007)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). LNCS, vol. 4963, Springer, Heidelberg (2008)
de Moura, L.M., Owre, S., Rueß, H., Rushby, J.M., Shankar, N., Sorea, M., Tiwari, A.: Sal 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)
Grieskamp, W., Kicillof, N.: A schema language for coordinating construction and composition of partial behavior descriptions. In: 5th International Workshop on Scenarios and State Machines: Models, Algorithms and Tools (SCESM) (2006)
Grieskamp, W., MacDonald, D., Kicillof, N., Nandan, A., Stobie, K., Wurden, F.: Model-based quality assurance of windows protocol documentation. In: First International Conference on Software Testing, Verification and Validation, ICST, Lillehammer, Norway (April 2008)
Gurevich, Y.: Specification and Validation Methods. In: Evolving Algebras 1993: Lipari Guide, pp. 9–36. Oxford University Press, Oxford (1995)
Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL. Theor. Comput. Sci. 343(3), 370–412 (2005)
Gurevich, Y., Veanes, M., Wallace, C.: Can abstract state machines be useful in language theory? Theor. Comput. Sci. 376(1), 17–29 (2007)
Habermehl, P., Iosif, R., Vojnar, T.: What Else Is Decidable about Integer Arrays? In: Amadio, R. (ed.) Proc. of the 11th Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS 2008). LNCS, vol. 4962, Springer, Heidelberg (2008)
Helander, J., Serg, R., Veanes, M., Roy, P.: Adapting futures: Scalability for real-world computing. In: Proceedings Real-Time Systems Symposium (RTSS 2007), pp. 105–116. IEEE, Los Alamitos (2007)
Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2008)
Jacobs, S., Sofronie-Stokkermans, V.: Applications of hierarchical reasoning in the verification of complex systems. Electr. Notes Theor. Comput. Sci. 174(8), 39–54 (2007)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
NModel (released, May 2007), http://www.codeplex.com/NModel
Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS 2001, pp. 29–37. IEEE, Los Alamitos (2001)
Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. In: Hierons, R., Bowen, J., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 39–76. Springer, Heidelberg (2008)
Veanes, M., Campbell, C., Schulte, W.: Composition of model programs. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 128–142. Springer, Heidelberg (2007)
Veanes, M., Schulte, W.: Protocol modeling with model program composition. In: FORTE 2008. LNCS, Springer, Heidelberg (2008); In this volume
Z3 (released September 2007), http://research.microsoft.com/projects/z3
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Veanes, M., Bjørner, N., Raschke, A. (2008). An SMT Approach to Bounded Reachability Analysis of Model Programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2008. FORTE 2008. Lecture Notes in Computer Science, vol 5048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68855-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-68855-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68854-9
Online ISBN: 978-3-540-68855-6
eBook Packages: Computer ScienceComputer Science (R0)