Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Model driven code checking
Holzmann G., Joshi R., Groce A. Automated Software Engineering15 (3-4):283-297,2008.Type:Article
Date Reviewed: Mar 5 2009

An erstwhile corollary of “thinking in C” was that we felt the specification and the program to be one and the same. Decades of collective suffering led us to realize the value of abstracting high-level models of the design and applying such methods to ensure pre-implementation consistency, correctness, and other desiderata for our designs.

This paper tells us that we can finally eat our cake and have it too: “The code of the application is now executed as is by the model checker. ... [This] allows us to verify implementation level code ... for ... safety and liveness properties.”

The paper begins with clear examples of SPIN/Promela-based “classical,” that is, high-level, model checking and also of SPIN as enhanced by new primitives that enable embedding of C code fragments into Promela text. Section 4, “The use of abstraction,” explains how to “define abstractions that can optimize ... exploration” of the enormous state-space that implementation-level C code engenders. Section 4.3 points out the price to be paid: “Not all user-defined abstractions will necessarily preserve ... logical soundness” in such code checking. The authors cite two conditions that are sufficient for an abstraction to be sound [1]. Section 6 states it simply: “We no longer attempt to extract models from the C code, we directly embed the ... C code into the verification model.”

This is an excellent, state-of-the-art paper that will benefit practitioners and students alike.

Reviewer:  George Hacken Review #: CR136557 (0910-0936)
1) Graf, S.; Mounier, L. Model checking software, 11th International SPIN WorkshopLNCS: LNCS. Springer, New York, NY, 2004.
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Model Checking (D.2.4 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Program Verification (I.2.2 ... )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Model Checking": Date
Systems and software verification: model-checking techniques and tools
B ., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L., Schnoebelen P., McKenzie P., Springer-Verlag New York, Inc., New York, NY, 1999.  190, Type: Book (9783540415237)
Sep 30 2002
Module checking
Kupferman O., Vardi M., Wolper P. Information and Computation 164(2): 322-344, 2001. Type: Article
Mar 1 2002
SMC: a symmetry-based model checker for verification of safety and liveness properties
Sistla A., Gyuris V., Emerson E. ACM Transactions on Software Engineering and Methodology 9(2): 133-166, 2000. Type: Article
Sep 1 2000
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy