Export

BIB

All authors

Damm, Werner and Westphal, Bernd

Booktitle

Formal Methods for Components and Objects: First International Symposium, FMCO 2002, Leiden, The Netherlands, November 5-8, 2002, Revised Lectures

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.

Publishing date

01 / 2003

ISBN / ISSN

3-540-20303-6

Type of Publication

inproceedings

Publisher

Springer Verlag

Series

Lecture Notes in Computer Science 2852

Pages

99 - 135

Editor

Springer Verlag