Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Programming assistance based on contracts and modular verification in the automation domain
Hurnaus D., Prähofer H.  SAC 2010 (Proceedings of the 2010 ACM Symposium on Applied Computing, Sierre, Switzerland, Mar 22-26, 2010)2544-2551.2010.Type:Proceedings
Date Reviewed: Jul 30 2010

While formal methods may not be a part of the mainstream [1], they have been shown, in many projects, to improve quality. Perhaps their mathematics and logic should be hidden inside special tools for specific domains.

This paper reports on a graphical integrated development environment (IDE), an example of such a tool. The domain is industrial control systems, and the hidden method is model checking (plus some artificial intelligence). Two case studies show that end users produce software that can be proven to be correct. The paper describes MONACO, the domain-specific language used by the end users. Experts define a logical model with integrity conditions and requirements, and also contracts, for parts of MONACO. They add explicit assertion/retraction actions to express changing conditions. The system uses the satisfiability modulo theories (SMT) satisfaction solver. As a result, the user is presented with options that are not only syntactically correct, but also fit the requirements.

As a criticism, on page 2,548, the knowledge update operator’s definition is unclear. It implies that a new condition removes older facts that will be inconsistent with the integrity conditions and the new condition, even if they share a common symbol with the new knowledge. What if the new condition contains an irrelevant symbol or is not consistent with the integrity constraints?

This paper is for people who are interested in improving software quality. The paper has minimal formalism, and it is easy to follow if you are knowledgeable about model checking.

Reviewer:  Richard Botting Review #: CR138204 (1106-0636)
1) Parnas, D.L. Really rethinking ‘formal methods’. IEEE Computer 43, 1(2010), 28–34.
Bookmark and Share
  Featured Reviewer  
 
Model Checking (D.2.4 ... )
 
 
Graphical Environments (D.2.6 ... )
 
 
Specification Techniques (F.3.1 ... )
 
 
User Interfaces (D.2.2 ... )
 
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