Defining Stochastic Process Algebraic Semantics of UML Activity Diagrams for Model-driven Performance Analysis

The popular model-driven development (MDD) methodology strongly
promotes model-based approach to modular system development, which often
implies as its integral part automatic code generation from UML design components.
When applying MDD for verifying performance-related system speci
cations, UML designs decorated with these specications in a certain prole
language need to be transformed to stochastic (Markovian) models or timed simulation
models. However, most of the previous efforts have focused on transformations
of (variants of) UML state machine models and/or transformations to
stochastic Petri net models, which entail two problems; Designing state machine
diagrams often becomes a burden for non-experts and graph-oriented Petri net
models complicates modular transformations of UML models.
To resolve these, we propose model transformation of UML activity diagrams
(UML AD) annotated with temporal information in RT-UML into stochastic process
algebraic forms for performance verication. To our knowledge, this is the
rst attempt to dene stochastic process algebraic semantics for the UML AD
with RT-UML annotations. Unlike those previous efforts, ours will facilitate veri
cation in early development stages, in which consultants and architects enjoy
the natural expressiveness of the UML AD, and modular component-based development,
thanks to the inherent compositionality of process algebra. Further, to
guarantee the validity of the transformation, we have proved the equivalence of
our semantics with existing stochastic Petri net semantics of UML AD. Through
preliminary evaluation, we have applied our transformation mechanism to a large
scale embedded system example and have shown its feasibility and strong potential.