Skip to main content
SpringerLink
Log in

State/Event-Based Software Model Checking

  • Conference paper
Book cover Integrated Formal Methods (IFM 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2999))

Included in the following conference series:

Abstract

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification.

We have implemented this work within our concurrent C model checker, MAGIC, and checked a number of properties of OpenSSL-0.9.6c (an open-source implementation of the SSL protocol) and Micro-C OS version 2 (a real-time operating system for embedded applications). Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework. We report a bug in the source code of Micro-C OS version 2, which was found during our experiments.

This research was sponsored by the Semiconductor Research Corporation (SRC) under contract no. 99-TJ-684, the National Science Foundation (NSF) under grants no. CCR-9803774 and CCR-0121547, the Office of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, and was conducted as part of the Predictable Assembly from Certifiable Components (PACC) project at the Software Engineering Institute (SEI). The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of SRC, NSF, ONR, NRL, ARO, the U.S. Government or any other entity.

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. Anantharaman, T.S., Clarke, E.M., Foster, M.J., Mishra, B.: Compiling path expressions into VLSI circuits. In: Proceedings of POPL, pp. 191–204 (1985)

    Google Scholar 

  2. BLAST website, http://www-cad.eecs.berkeley.edu/~rupak/blast

  3. Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 203–213 (2001)

    Google Scholar 

  5. Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Browne, M.C.: Automatic verification of finite state machines using temporal logic. PhD thesis, Carnegie Mellon University, Technical report no. CMU-CS-89-117 (1989)

    Google Scholar 

  7. Bradfield, J., Stirling, C.: Modal Logics and Mu-Calculi: An Introduction. Handbook of Process Algebra, pp. 293–330. Elsevier, Amsterdam (2001)

    Google Scholar 

  8. Burch, J.: Trace algebra for automatic verification of real-time concurrent systems. PhD thesis, Carnegie Mellon University, Technical report no. CMU-CS-92-179 (1992)

    Google Scholar 

  9. Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proceedings of ICSE 2003, pp. 385–395 (2003)

    Google Scholar 

  10. Chauhan, P., Clarke, E.M., Kukula, J.H., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Proceedings of FMCAD, pp. 33–51 (2002)

    Google Scholar 

  11. 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: Proceedings of ICSE, pp. 439–448. IEEE Computer Society, Los Alamitos (2000)

    Chapter  Google Scholar 

  12. 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, Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  13. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  14. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample guided abstraction refinement. Computer Aided Verification, 154–169 (2000)

    Google Scholar 

  15. Clarke, E.M., Gupta, A., Kukula, J.H., Shrichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Proceedings of CAV, pp. 265–279 (2002)

    Google Scholar 

  16. Clarke, E., Grumberg, O., Peled, D.: Model Checking, December 1999. MIT Press, Cambridge (1999)

    Google Scholar 

  17. Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Chaki, S., Ouaknine, J., Yorav, K., Clarke, E.M.: Automated compositional abstraction refinement for concurrent C programs: A two-level approach. In: Proceedings of SoftMC 2003. ENTCS, vol. 89(3) (2003)

    Google Scholar 

  19. Dill, D.L.: Trace theory for automatic hierarchical verification of speedindependent circuits. PhD thesis, Carnegie Mellon University, Technical report no. CMU-CS-88-119 (1988)

    Google Scholar 

  20. Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. on Programming Languages and Systems 16(3), 843–871 (1994)

    Article  Google Scholar 

  21. Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proceedings of FSE, ACM Press, New York (2003)

    Google Scholar 

  22. Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification, Warsaw, Poland, pp. 3–18. Chapman & Hall, Sydney (1995)

    Google Scholar 

  23. Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  24. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL, pp. 58–70 (2002)

    Google Scholar 

  25. Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 155. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  26. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  27. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Decomposing refinement proofs using assume-guarantee reasoning. In: Proceedings of ICCAD, pp. 245–252. IEEE Computer Society Press, Los Alamitos (2000)

    Google Scholar 

  28. Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  29. Kurshan, R.P.: Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton (1994)

    Google Scholar 

  30. Kindler, E., Vesper, T.: ESTL: A temporal logic for events and states. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, p. 365. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  31. Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  32. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of POPL (1985)

    Google Scholar 

  33. MAGIC website, http://www.cs.cmu.edu/~chaki/magic

  34. McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 24–35. Springer, Heidelberg (1997)

    Google Scholar 

  35. Milner, R.: Communication and Concurrency. Prentice-Hall International, London (1989)

    MATH  Google Scholar 

  36. Naumovich, G., Clarke, L.A., Osterweil, L.J., Dwyer, M.B.: Verification of concurrent software with FLAVERS. In: Proceedings of ICSE, pp. 594–595. ACM Press, New York (1997)

    Chapter  Google Scholar 

  37. De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems 25(7), 761–778 (1993)

    Article  MATH  Google Scholar 

  38. De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the ACM (JACM) 42(2), 458–487 (1995)

    Article  MATH  Google Scholar 

  39. Păsăreanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counterexamples when model checking abstracted Java programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 284–298. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  40. Pnueli, A.: Application of temporal logic to the specification and verification of reactive systems: A survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510–584. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  41. Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: proceedings of Fifth Intern. Symposium on Programming, pp. 337–350 (1981)

    Google Scholar 

  42. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, London (1997)

    Google Scholar 

  43. Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. Computer-Aided Verification, 248–263 (2000)

    Google Scholar 

  44. SLAM website, http://research.microsoft.com/slam

  45. OpenSSL, http://wp.netscape.com/eng/ssl3/ssl-toc.html

  46. Stoller, S.D.: Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer 4(1), 71–91 (2002)

    Article  Google Scholar 

  47. Wring website, http://vlsi.colorado.edu/~rbloem/wring.html

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA, 15213, USA

    Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina & Nishant Sinha

Authors
  1. Sagar Chaki
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Edmund M. Clarke
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Joël Ouaknine
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Natasha Sharygina
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Nishant Sinha
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Department of Computing, University of Sheffield, S1 4DP, Sheffield, UK

    John Derrick

  3. School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N. (2004). State/Event-Based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24756-2_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21377-2

  • Online ISBN: 978-3-540-24756-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation