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. © Springer-Verlag Berlin Heidelberg 2003.
Cite
CITATION STYLE
Damm, W., & Westphal, B. (2003). Live and let die: LSC-based verification of UML-models. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2852, 99–135. https://doi.org/10.1007/978-3-540-39656-7_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
