Consistency Checking of UML Dynamic Models Based on Petri Net Techniques

To aid the development of high quality software applications, we present an approach for consistency checking of UML dynamic models based on Petri net techniques. ECPN, an extended colored Petri net, is used to formally describe state transitions of individual objects and interactions among objects, and is therefore capable of verifying the consistency of the models based on Petri net theory. In this work, we consider UML sequence diagrams and statecharts. The approach begins with a flattening strategy for UML dynamic models and then discusses translation of statecharts with composite states to an ECPN notation. The coverability graph is used to drive the consistency checking process. The paper discusses all phases of the approach and illustrates the concept by an example