Parametric Transformations for Flexible Analysis

We present an approach for flexible analysis of complex system models based on a parametric model-to-model (M2M) transformation where the target model has variants. We describe a M2M transformation from sequence diagrams (SDs) to coloured Petri nets (CPNs) with (untimed, timed, stochastic) variants enabling different forms of dependability and performance analysis. The transformation is parametric on the chosen variant with the core set of rules defining the transformation from SDs to CPNs. Moreover, the flexibility of the framework lies in the incremental nature of the transformation: given a SD (with stochastic and time annotations) and corresponding untimed CPN, we can generate other CPN variants by incrementally applying the specific variant rules. This paper contributes towards the theoretical foundations of parametric transformations, defines and proves the semantic correctness of a parametric transformation between SDs and CPN variants.