Model checking for an executable subset of UML

Author

Xie, Fei ; Levin, Vladimir ; Browne, James C.

Author_Institution

Dept. of Comput. Sci., Texas Univ., Austin, TX, USA

fYear

2001

fDate

26-29 Nov. 2001

Firstpage

333

Lastpage

336

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.

Keywords

formal specification; language translation; program verification; programming language semantics; specification languages; COSPAN model checker; S/R language; S/R representations; automated support; automatic translation; error traces; executable UML subset; execution semantics; input language; model checking; model checking software system designs; model transformations; state space; xUML level logic; xUML representations; Computer languages; Handicapped aids; Interleaved codes; Logic design; Phase detection; Proposals; Software systems; State-space methods; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on

ISSN

1938-4300

Print_ISBN

0-7695-1426-X

Type

conf

DOI

10.1109/ASE.2001.989823

Filename

989823