Live and let die: LSC based verification of UML models

For verification, the paper proposes to transfer to the UML domain the methodology of K.L. McMillan [A methodology for hardware verification using compositional model checking, Science of Computer Programming 37 (2000) 279-309], comprising a first step which is based on results of C.N. Ip and D.L. Dill [Better verification through symmetry, Formal Methods in System Design 9 (1-2) (1996) 41-75] about symmetric data-types and for which F. Xie and J.C. Browne [Integrated state space reduction for model checking executable object-oriented software system designs, in: R.-D. Kutsche, H. Weber (Eds.), FASE, Lecture Notes in Computer Science, vol. 2306, Springer, 2002] coined the term “Query Reduction” and, as second step, an abstract interpretation called “data-type reduction” to construct a finite state over-approximation of the original model for each query. The paper also briefly discusses counter-measures against false-negatives occurring in the over-approximation.