Mashkoor and Jacquot discuss using the formal modeling and reasoning language Event-B for domain engineering, and provide an interesting (but rather simplistic) example of computer-controlled cars (CyCabs). They properly state that “a domain model is the right artifact to start with,” and observe that it is difficult for customers to read and understand formal specifications. They propose using animation to build a “mental bridge between complex formal specifications and their perception in the real world.” However, animation presents “typical behavioral scenarios of the specification,” that is, examples rather than a complete specification. Furthermore, a domain model presents invariants (about things and relationships), and only then all (rather than just typical) kinds of behavior. Thus, a narrative of the domain model, appropriately illustrated if needed, is essential. Bjørner, for example, emphasizes the importance and role of narratives [1].

The authors note that their research is closely related to Bjørner’s work on the formalization of as many domain facts as possible [1], and state that their objective was slightly different. They wanted “to check the capability of Event-B as a domain engineering tool and to point out and address (where possible) the issues with which [they were] confronted during this exercise.” The example domain appears to be closed rather than open. For example, it is unclear what happens if a vehicle in the system collides with a vehicle not in the system or with a pedestrian. This is possible because “CyCabs will move in the public space, possibly on dedicated lanes, and will have strong interactions with other road users.”

The most interesting part of the paper is in its “Lessons Learned” sections, where the authors note some serious problems with using Event-B, particularly problems due to the scattering of a behavioral law into the guards of several events (for example, “the assumption that a vehicle moves on a path only when it has some room to do so is scattered into four events”). This makes a specification rather difficult to read, and, in the same manner as for a program, reading is much more important than writing [2]. The authors deal at some length with Event-B technicalities, acknowledge the need to express facts at a high(er) abstraction level, and even present an example along the lines of Bertrand Meyer’s “Quantifiers Considered Harmful” [3]. They consider Event-B an “adequate language for domain engineering,” but observe that improvements--most importantly, better specification structuring mechanisms--would be very desirable. While noting that “animation alone is not sufficient to decide if a model is ‘good,’” they still overemphasize it. Animation may be very useful to explore new features, but it is not clear, for example, whether and how it may be made usable to understand domain invariants. Finally, the authors properly state that “tools based on a better understanding of the needs of the specifiers” would be a promising approach, but they do not mention that a language is also a tool, that is, a tool for thought.