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.