Interactive Model Based On an Extended CPN

The UML modeling of complex distributed systems often is a great challenge due to the large amount of parallel real-time operating components. In this paper the problems of verification of such systems are discussed. ECPN, an Extended Colored Petri Net is defined to formally describe state transitions of components and interactions among components. The relationship between sequence diagrams and Free Choice Petri Nets is investigated. Free Choice Petri Net theory helps verifying the liveness of sequence diagrams. By converting sequence diagrams to ECPNs and then comparing behaviors of sequence diagram ECPNs and statecharts, the consistency among models is analyzed. Finally, a verification process for an example model is demonstrated.

• Shuzhen Yao
• Fengjing Zhao
• Jianwei He

• Consistency
• liveness
• Petri Net
• sequence diagram.

[1] G. Engels, J. H. Hausmann, R. Heckel, and S. Sauer, "Testing the
consistency of dynamic UML diagrams", Integrated Design and Process
Technology, June 2002.
[2] S. K. Kim and D. Carrington, "A Formal Object-Oriented Approach to
defining Consistency Constraints for UML Models", 2004 Australian
Software Engineering Conference, 2004.
[3] T. Miyamoto, "A Survey of Object Oriented Petri Nets and Analysis
Methods", IEICE Trans. Fundamentals, Vol. E88-A, No. 11, 2005
[4] J. Rumbaugh, I. Jacobson, and G. Booch, The Unified Modeling
Language Reference Manual. Addison Wesley/Pearson, Jan. 2001.
[5] Tom Pender, UML Bible, Wiley, Sep. 2003.
[6] T. Schafer, A. Knapp, and S. Merz. Model Checking UML State
Machines and Collaborations on the Workshop on Software Model
Checking, Paris, Jul.2001.
[7] W. Dong, and Z. C. Qi, "Study on the checking of UML Models",
Dissertation of National Defense University of Science and Technology,
China, Oct. 2002.
[8] B.Simona,D.Susanna,M.Jose, from UML Sequence Diagrams and
Statecharts to analysable Petri Net models,In Proc. of 3. rd. Int.
Workshop on. Software and Performance (WOSP2002), .Rome, Italy,
July 2002.
[9] E. Guerra and J. D. Lara, "A Framework for the Verification of UML
models. Examples using Petri Nets",
http://www.ii.uam.es/~jlara/investigacion
[10] S.Z.Yao, F.G.Tang, and Y.F. Liu, "An object-oriented model for parallel
software", TOOLS27, China, Sep.1998.
[11] M.H.Hamza, Modelling, Identification, and Control (MIC 2004),
Grindelwald, Switzerland, Feb.2004.
[12] T. Murata, "Petri Nets: Properties, Analysis and Applications", Proc.
IEEE, Vol. 77, 1989.
[13] http://www.informatik.uni-hamburg.de/TGI/Petri Nets /tools.