kirancodes.me
To Proof Maintenance & Beyond!
ASE 2001

Model Checking for an Executable Subset of UML

Fei Xie, Vladimir Levin, James C. Browne

DOI 10.1109/ase.2001.989823dblp

Abstract

The paper presents an approach to model checking software system designs specified in xUML (http://www.kc.com/html/xuml.html), an executable subset of UML. This approach is enabled by the execution semantics of xUML and is based on automatic translation from xUML to S/R, the input language of the COSPAN model checker (R.H. Hardin et al., 1996). Model transformations are applied to reduce the state space of the resulting S/R model that is to be verified by COSPAN. An xUML level logic for specifying properties to be checked is defined. Automated support is provided for translating properties specified in the logic to S/R representations and mapping error traces generated by COSPAN to xUML representations.

BibTeX
@inproceedings{Xie-al:ASE01,
  author    = {Fei Xie and
               Vladimir Levin and
               James C. Browne},
  title     = {Model Checking for an Executable Subset of {UML}},
  booktitle = {ASE},
  pages     = {333--336},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Related papers