Interactive Model Based On an Extended CPN

Authors: Shuzhen Yao, Fengjing Zhao, Jianwei He

Abstract:

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.

Keywords: Consistency, liveness, Petri Net, sequence diagram.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1070971

References:

[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.