Output details
11 - Computer Science and Informatics
University of St Andrews
Formal Transformation from Sequence Diagrams to Coloured Petri Nets
<07>We describe a novel formal approach to model-driven transformation of UML2 behavioural models for formal verification. The main contribution is a detailed proof of semantic correctness for the transformation of
sequence diagrams into coloured Petri nets which guarantees a one-to-one correspondence between the legal traces of both models. Semantic correctness is rarely addressed in model transformations where most work covers syntactic correctness, termination and confluence. Our result is crucial to guarantee the absence of implied (unspecified) behaviour in the target model, and enables an accurate analysis of the source model. This paper sets the foundation of more recent published work.