This paper addresses the problem of formal verification of UML models in the semantics of Damm and Josko et al. (Science of Computer Programming, this issue). The problem is twofold in that it requires on the one hand a specification language which is rich enough to express properties about entities that are only created during a run of the system and on the other hand a means to abstract the a priori unbounded state space to a finite one which lends itself to treatment by approved finite state methods. As the specification language, the paper proposes to extend Live Sequence Charts as presented by W. Damm and D. Harel [LSCs: breathing life into message sequence charts, Formal Methods in System Design 19 (1) (2001) 121-141] and J. Klose [Live sequence charts: A graphical formalism for the specification of communication behavior, Ph.D. Thesis, Carl von Ossietzky Universitat Oldenburg, 2003] by means of dynamically bound instance lines and equips it with a formal semantics w.r.t. the UML domain. 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.), EASE, 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.
展开▼
