Validating timed UML models by simulation and verification

This paper presents a technique and a tool for model-checking operational (design level) UML models based on a mapping to a model of communicating extended timed automata. The target language of the mapping is the IF format, for which existing model-checking and simulation tools can be used. Our app...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2006-04, Vol.8 (2), p.128-145
Main Authors: OBER, Iulian, GRAF, Susanne, OBER, Ileana
Format: Article
Language:English
Subjects:
Applied sciences
Computer based modeling
Computer science
control theory
systems
Exact sciences and technology
Programming languages
Software
Software engineering
Validation studies
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a technique and a tool for model-checking operational (design level) UML models based on a mapping to a model of communicating extended timed automata. The target language of the mapping is the IF format, for which existing model-checking and simulation tools can be used. Our approach takes into consideration most of the structural and behavioural features of UML, including object-oriented aspects. It handles the combination of operations, state machines, inheritance and polymorphism, with a particular semantic profile for communication and concurrency. We adopt a UML profile that includes extensions for expressing timing. The breadth of concepts covered by our mapping is an important point, as many previous approaches for applying formal validation to UML put much stronger limitations on the considered models. For expressing properties about models, a formalism called UML observers is defined in this paper. Observers reuse existing concepts like classes and state machines, and they allow expressing a significant class of linear temporal properties. The approach is implemented in a tool that imports UML models from an XMI repository, thus supporting several editors like Rational Rose, Rhapsody or Argo. The generated IF models may be simulated and verified via an interface that presents feedback in the vocabulary of the original UML model. [PUBLICATION ABSTRACT]
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-005-0205-x