Feedback on paper of Anastasakis et al.


FLAWS

* Since the paper's main contribution is the set of transformation rules, not
describing them is a major omission. Similarly, the subset of the UML that is
transformed is not precisely defined. 

* In translating from one formalism to another, one would hope that the
transformation was sound in some sense. Unfortunately, although most of the
discussion is about the differences between the language and how they can be
addressed in the transformation, there is no attempt to prove the soundness of
the solutions. From the discussion, one can extract evidence that the
transformation is unsound.  

* The evaluation is cursory: one simple example was tested and found to be valid
within the scope of the Alloy tool. Very few details are given. Since no example
of the detection of an invalid model is given, it is hard to see whether this
might be useful. If more examples have been tested, one would expect at least
some summary of the results. 


HYPOTHESES

No hypotheses are given explicitly. From the amount of space given to different
issues, one can infer some implicit hypotheses. 

* Soundness: despite the absence of a formal proof of the soundness of the
transformation, the paper is dominated by discussion of the sound transformation
when UML and Alloy differ. Example transformations are given together with
informal arguments as to their correctness. Especially in section 6.2, there is
evidence that the current transformation is unsound. 

* Usefulness: implicit in the whole point of building such a tool is that it
will be useful to system developers in spotting bugs early by applying a model
checker. However, if this was the main hypothesis, one would expect far more
evaluation of it.

* Usability: implicit in the criticism of related work using theorem provers, is
the claim that this model-checking approach is easier for ordinary programmers
to use. However, no evidence is provided to support this, e.g., experiments in
which such users had successfully used the system, contrasted with their failure
on theorem-proving based systems. 



COMMON MISTAKES

* Several of you identified as the claim that UML could be translated to
Alloy. This is correct, but a *very* weak claim in the absence of some claim
about the properties of this translation, e.g., that it was correct or nearly
correct, and/or complete, efficient, etc. Some kind of correctness claim is
essential, otherwise, they could just generate random Alloy and the claim would
be vacuously true.