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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
BLAST website, http://www-cad.eecs.berkeley.edu/~rupak/blast
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)
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)
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)
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)
Bradfield, J., Stirling, C.: Modal Logics and Mu-Calculi: An Introduction. Handbook of Process Algebra, pp. 293–330. Elsevier, Amsterdam (2001)
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)
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)
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)
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)
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)
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)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample guided abstraction refinement. Computer Aided Verification, 154–169 (2000)
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)
Clarke, E., Grumberg, O., Peled, D.: Model Checking, December 1999. MIT Press, Cambridge (1999)
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)
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)
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)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. on Programming Languages and Systems 16(3), 843–871 (1994)
Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proceedings of FSE, ACM Press, New York (2003)
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)
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)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL, pp. 58–70 (2002)
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)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
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)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)
Kurshan, R.P.: Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton (1994)
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)
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)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of POPL (1985)
MAGIC website, http://www.cs.cmu.edu/~chaki/magic
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)
Milner, R.: Communication and Concurrency. Prentice-Hall International, London (1989)
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)
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)
De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the ACM (JACM) 42(2), 458–487 (1995)
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)
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)
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)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, London (1997)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. Computer-Aided Verification, 248–263 (2000)
SLAM website, http://research.microsoft.com/slam
Stoller, S.D.: Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer 4(1), 71–91 (2002)
Wring website, http://vlsi.colorado.edu/~rbloem/wring.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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