Sciweavers

APSEC
2005
IEEE

A Formal Semantics of Timed Activity Diagrams and its PROMELA Translation

13 years 9 months ago
A Formal Semantics of Timed Activity Diagrams and its PROMELA Translation
The lack of a precise semantics for UML activity diagrams makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML activity diagrams, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML activity diagrams, which are recognized to be more tractable by engineers, and we extend them with timing constraints. We outline the translation of our semantics into the PROMELA input language of the SPIN model checker which can be used to check several properties.
Nicolas Guelfi, Amel Mammar
Added 24 Jun 2010
Updated 24 Jun 2010
Type Conference
Year 2005
Where APSEC
Authors Nicolas Guelfi, Amel Mammar
Comments (0)