Skip to main content
SpringerLink
Log in

Symbolic Bounded Conformance Checking of Model Programs

  • Conference paper
Perspectives of Systems Informatics (PSI 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5947))

Abstract

Model programs are high-level behavioral specifications typically representing Abstract State Machines or ASMs. Conformance checking of model programs is the problem of deciding if the set of traces allowed by one model program forms a subset of the set of traces allowed by another model program. This is a foundational problem in the context of model-based testing, where one model program corresponds to an implementation and the other one to its specification. Here model programs are described using the ASM language AsmL. We assume a background \({\mathcal{T}}\) containing linear arithmetic, sets, and tuples. We introduce the Bounded Conformance Checking problem or BCC as a special case of the conformance checking problem when the length of traces is bounded and provide a mapping of BCC to a theorem proving problem in \({\mathcal{T}}\). BCC is shown to be highly undecidable in the general case but decidable for a class of model programs that are common in practice.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Henzinger, T.A.: A really temporal logic. In: Proc. 30th Symp. on Foundations of Computer Science, pp. 164–169 (1989)

    Google Scholar 

  2. Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. AsmL, http://research.microsoft.com/fse/AsmL/

  5. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Bjørner, D., Henson, M. (eds.): Logics of Specification Languages. Springer, Heidelberg (2008)

    Google Scholar 

  7. Bjørner, N., Gurevich, Y., Schulte, W., Veanes, M.: Symbolic bounded model checking of abstract state machines. Technical Report MSR-TR-2009-14, Microsoft Research (February 2009) (Submitted to IJSI)

    Google Scholar 

  8. Börger, E., Stärk, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)

    MATH  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Bryant, R.E., German, S.M., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 470–482. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)

    Google Scholar 

  12. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  14. de Moura, L., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 438–455. Springer, Heidelberg (2002)

    Google Scholar 

  15. Fisher, M.J., Rabin, M.O.: Super-exponential complexity of presburger arithmetic. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 122–135. Springer, Heidelberg (1998); Reprint from SIAM-AMS Proceedings, vol. VII, pp. 27-41 (1974)

    Google Scholar 

  16. Grieskamp, W., MacDonald, D., Kicillof, N., Nandan, A., Stobie, K., Wurden, F.: Model-based quality assurance of Windows protocol documentation. In: ICST 2008, Lillehammer, Norway (April 2008)

    Google Scholar 

  17. Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)

    Google Scholar 

  18. Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL. Theor. Comput. Sci. 343(3), 370–412 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  19. Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\Pi^1_1\) complete. Journal of Symbolic Logic 56, 637–642 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  20. Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)

    Google Scholar 

  21. Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2008)

    Google Scholar 

  22. Kang, E., Jackson, D.: Formal modeling and analysis of a flash filesystem in Alloy. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 294–308. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. NModel, http://www.codeplex.com/NModel (public version released, May 2008)

  24. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  25. Rybina, T., Voronkov, A.: A logical reconstruction of reachability. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 222–237. Springer, Heidelberg (2004)

    Google Scholar 

  26. Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II, pp. 115–125 (1968)

    Google Scholar 

  28. Veanes, M., Bjørner, N.: Input-output model programs. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 322–335. Springer, Heidelberg (2009)

    Google Scholar 

  29. Veanes, M., Bjørner, N., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 53–68. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  30. 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.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 39–76. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Veanes, M., Saabas, A.: On bounded reachability of programs with set comprehensions. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 305–317. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  32. Veanes, M., Saabas, A., Bjørner, N.: Bounded reachability of model programs. Technical Report MSR-TR-2008-81, Microsoft Research (May 2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Margus Veanes & Nikolaj Bjørner

Authors
  1. Margus Veanes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nikolaj Bjørner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. (1941-2009), The Weizmann Institute of Science, Rehovot, Israel New York University, NY, USA

    Amir Pnueli

  2. Siberian Division of the Russian Academy of Sciences, A.P. Ershov Institute of Informatics Systems, 6, Acad. Lavrentiev pr., 630090, Novosibirsk, Russia

    Irina Virbitskaite

  3. Department of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Veanes, M., Bjørner, N. (2010). Symbolic Bounded Conformance Checking of Model Programs. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2009. Lecture Notes in Computer Science, vol 5947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11486-1_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11486-1_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11485-4

  • Online ISBN: 978-3-642-11486-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation