Skip to main content
SpringerLink
Log in

Model Checking a Model Checker: A Code Contract Combined Approach

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6447))

Included in the following conference series:

Abstract

Model checkers, like any complex software, are subject to bugs. Unlike ordinary software, model checkers are often used to verify safety critical systems. Their correctness is thus vital. Verifying model checkers is extremely challenging because they are always complicated in logic and highly optimized. In this work, we propose a code contract combined approach for checking model checkers and apply it to a home-grown model checker PAT. In this approach, we firstly embed programming contracts (i.e., pre/post-conditions and invariants) into its source code, which can capture correctness of model checking algorithms, underlying data structures, consistency between different model checking parameters, etc. Then, interface models of complicated data structures and graphical user interfaces (GUI) are built and model checked. By linking the interface models with actual source codes and exhausting all execution sequences of interface models using PAT, we model check PAT using itself! Our experience shows that the approach is effective in identifying common bugs or subtle flaws that result from extremely improbable events.

This research was partially supported by a grant “SRG ISTD 2010 001” from Singapore University of Technology and Design.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. STTT 5(1), 49–58 (2003)

    Article  MATH  Google Scholar 

  3. Barnett, M., DeLine, R., Fähndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The SPEC# Programming System: Challenges and Directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144–152. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Barnett, M., Fähndrich, M., de Halleux, P., Logozzo, F., Tillmann, N.: Exploiting the Synergy between Automated-test-generation and Programming-by-contract. In: ICSE Companion 2009, pp. 401–402. IEEE, Los Alamitos (2009)

    Google Scholar 

  5. Bierhoff, K., Aldrich, J.: Lightweight Object Specification with Yypestates. In: ESEC/SIGSOFT FSE 2005, pp. 217–226. ACM, New York (2005)

    Google Scholar 

  6. Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdzinski, M., Mang, F.Y.C.: Interface Compatibility Checking for Software Modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 428–441. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  9. Dill, D.L.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  10. Emerson, E.A., Wahl, T.: Dynamic Symmetry Reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Floyd, R.W.: Algorithm 97: Shortest Path. Commun. ACM 5(6), 345 (1962)

    Article  Google Scholar 

  12. Gastin, P., Oddoux, D.: Fast LTL to Büchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Gunter, E.L., Peled, D.: Model checking, Testing and Verification Working Together. Formal Asp. Comput. 17(2), 201–221 (2005)

    Article  MATH  Google Scholar 

  14. Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  15. Hughes, G., Bultan, T.: Interface Grammars for Modular Software Model Checking. In: ISSTA 2007, pp. 39–49. ACM, New York (2007)

    Google Scholar 

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

    MATH  Google Scholar 

  17. Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodová, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 414–429. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Kebrt, M., Sery, O.: UnitCheck: Unit Testing and Model Checking Combined. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 97–103. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Liu, Y., Pang, J., Sun, J., Zhao, J.: Verification of Population Ring Protocols in PAT. In: TASE 2009, pp. 81–89. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  20. Liu, Y., Sun, J., Dong, J.S.: Scalable Multi-core Model Checking Fairness Enhanced Systems. In: ICFEM 2009. LNCS, vol. 5885, pp. 426–445. Springer, Heidelberg (2009)

    Google Scholar 

  21. Mühlberg, J.T., Lüttgen, G.: Blasting Linux Code. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 211–226. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Peled, D.: Combining Partial Order Reductions with On-the-fly Model-Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  23. Peled, D.: Model Checking and Testing Combined. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 47–63. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  24. Sen, K., Marinov, D., Agha, G.: CUTE: a Concolic Unit Testing Engine for C. In: ESEC/SIGSOFT FSE 2005, pp. 263–272. ACM, New York (2005)

    Google Scholar 

  25. Sherman, E., Dwyer, M.B., Elbaum, S.G.: Saturation-based Testing of Concurrent Programs. In: ESEC/SIGSOFT FSE 2009, pp. 53–62. ACM, New York (2009)

    Google Scholar 

  26. Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs. ACM Trans. Softw. Eng. Methodol. 17(2) (2008)

    Google Scholar 

  27. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  28. Sun, J., Liu, Y., Dong, J.S., Zhang, X.: Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction. In: ICFEM 2009. LNCS, vol. 5885, pp. 581–600. Springer, Heidelberg (2009)

    Google Scholar 

  29. Weiser, M.: Program Slicing. In: ICSE, pp. 439–449 (1981)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Singapore University of Technology and Design, UK

    Jun Sun

  2. School of Computing, National University of Singapore, UK

    Yang Liu & Bin Cheng

Authors
  1. Jun Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yang Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bin Cheng
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Computer Science Dept, National University of Singapore, 13 Computing Drive, 117417, Singapore, Singapore

    Jin Song Dong

  2. Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), 200062, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sun, J., Liu, Y., Cheng, B. (2010). Model Checking a Model Checker: A Code Contract Combined Approach. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16901-4_34

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16900-7

  • Online ISBN: 978-3-642-16901-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation