@inproceedingsDam2003, Author = {Damm, Werner and Westphal, Bernd}, Title = {Live and Let Die: LSC-Based Verification of UML-Models}, Year = {2003}, Pages = {99 - 135}, Month = {01}, Editor = {Springer Verlag}, Publisher = {Springer Verlag}, Series = {Lecture Notes in Computer Science 2852}, Isbn = {3-540-20303-6}, Booktitle = {Formal Methods for Components and Objects: First International Symposium, FMCO 2002, Leiden, The Netherlands, November 5-8, 2002, Revised Lectures}, type = {inproceedings}, note = {We present a strategy for automatic formal verification of Live Sequence Chart (LSC) specifications against UML models in the semantics of [7] employing the symmetry-based technique of Query Reduction [18,34,44] and the abstraction technique Data-type Red}, Abstract = {We present a strategy for automatic formal verification of Live Sequence Chart (LSC) specifications against UML models in the semantics of [7] employing the symmetry-based technique of Query Reduction [18,34,44] and the abstraction technique Data-type Reduction [34]. Altogether this allows for automatic formal verification without providing finite bounds on the numbers of objects created during a run of the system. Our presentation is grounded on a specific formal interpretation of LSCs for the UML domain in terms of [7] which is rich enough to in particular express properties about objects which are created only during activation of the LSC. } @COMMENTBibtex file generated on