Synthesis and Consistency Verification of UML Sequence Diagrams with Hierarchical Structure
Abstract
Automatic consistency checking for UML state machine diagrams and sequence diagrams has been expected since developers spend considerable effort to keep the consistency. In particular, the verification of diagrams with a hierarchical structure is required. Although formalization of state machine diagrams with hierarchical structure has been widely treated, it is not yet sufficient for sequence diagrams. In this paper, we propose an automatic method for verifying the consistency between state machine diagrams and sequence diagrams with a hierarchical structure. In our verification framework, the consistency of diagrams is defined as an inclusive relation between the sets of traces and is checked using the FDR model checker. FDR can check refinement relation between processes described as CSPM notation. We provide a process description of state machine diagrams and sequence diagrams and can verify the consistency by checking traces inclusion of processes using FDR. Our description supports for sequence diagrams with a hierarchical structure. We applied the proposed process representation to an example diagram that describes interactions of basic components of a wireless sensor network system and showed that the hierarchical behavior of the diagram could be correctly represented.
References
M. Petre, “UML in practice,” Proc. on Int’l Conf. on Softw. Eng. (ICSE 2013), pp. 722–731, 2013.
D. Torre, Y. Labiche, and M. Genero, “UML Consistency Rules: A Systematic Mapping Study,” Proc. of the 18th Int’l Conf. on Evaluation and Assessment in Softw. Eng., (EASE 2014), pp. 1–10, 2014.
K. Thramboulidis and F. Christoulakis, “UML4IoT - UML-based approach to exploit IoT in cyber-physical manufacturing systems,” Computers in Industry, vol. 82, pp. 259–272, 2016.
B. Wang and J. S. Baras, “Integrated modeling and simulation framework for wireless sensor networks,” in 2012 IEEE 21st Int’l Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, June 2012, pp. 268–273.
V. H. D´ıaz, J.-F. Mart´ınez, N. L. Mart´ınez, and R. M. Del Toro, “Self-Adaptive Strategy Based on Fuzzy Control Systems for Improving Performance in Wireless Sensors Networks,” Sensors, vol. 15, no. 9, pp. 24 125–24 142, sep 2015. [Online]. Available: http://www.mdpi.com/1424-8220/15/9/24125
S. Uke and R. Thool, “UML Based Modeling for Data Aggregation in Secured Wireless Sensor Network,” Procedia Comp. Sci., vol. 78, pp. 706–713, 2016, 1st Int’l Conf. on Inf. Security and Privacy 2015.
Z. Huzar, L. Kuzniarz, G. Reggio, and J. L. Sourrouille, “Consistency Problems in UML-Based Software Development,” in UML Modeling Languages and Applications, UML 2004 Satellite Activities, 2005, pp. 1–12.
F. J. Lucas, F. Molina, and A. Toval, “A systematic review of UML model consistency management,” Information and Software Technology, vol. 51, no. 12, pp. 1631–1645, 2009.
F. ul Muram, H. Tran, and U. Zdun, “Systematic Review of Software Behavioral Model Consistency Checking,” ACM Computing Surveys, vol. 50, no. 2, pp. 1–39, 2017. [Online]. Available: http://dl.acm.org/citation.cfm?doid=3071073.3037755
D. Torre, Y. Labiche, M. Genero, and M. Elaasar, “A systematic identification of consistency rules for UML diagrams,” Journal of Systems and Software, vol. 144, no. June, pp. 121–142, 2018.
X. Zhao, Q. Long, and Z. Qiu, “Model Checking Dynamic UML Consistency,” in Proc. of the 8th Int’l Conf. on Formal Engineering Methods, ICFEM 2006, 2006, Book, pp. 440–459.
A. Egyed, “Automatically detecting and tracking inconsistencies in software design models,” IEEE Trans. Softw. Eng., vol. 37, pp. 188–204, March 2011.
P. Kaufmann, M. Kronegger, A. Pfandler, M. Seidl, and M. Widl, “A SAT-Based Debugging Tool for State Machines and Sequence Diagrams,” in Proc. of the7th Int’l Conf. on Softw. Language Eng. (SLE 2014), 2014, pp. 21–40.
T. Yokogawa, S. Amasaki, K. Okazaki, Y. Sato, K. Arimoto, and H. Miyazaki, “Consistency verification of UML diagrams based on process bisimulation (fast abstract),” in Proc. of the 19th IEEE Pacific Rim Int’l Symp. on Dependable Computing (PRDC’13), 2013, pp. 126–127.
T. Gibson-Robinson, P. Armstrong, A. Boulgakov, and A. Roscoe, “FDR3: a parallel refinement checker for CSP,” International Journal on Software Tools for Technology Transfer, vol. 18, no. 2, pp. 149–167, 2016.
S. Phuklang, T. Yokogawa, P. Leelaprute, and K. Arimoto, “Tool Support for Consistency Verification of UML Diagrams,” in Poster Session on The 18th Int’l Conf. on Product-Focused Softw. Process Improvement (Profes 2017), 2017.
E. Andr ´ e, C. Choppy, and K. Klai, “Formalizing non-concurrent UML state machines ´ using colored petri nets,” ACM SIGSOFT Software Engineering Notes, vol. 37, no. 4, pp. 1–8, 2012.
E. Andr ´ e, M. M. Benmoussa, and C. Choppy, “Formalising concurrent UML state ´ machines using coloured Petri nets,” Formal Aspects of Computing, vol. 28, no. 5, pp. 805–845, 2016.
S. J. Zhang and Y. Liu, “An automatic approach to model checking UML state machines,” in Proc. of the 4th Int’l Conf. on Secure Softw. Integration and Reliability Improvement Companion (SSIRI-C), 2010, pp. 1–6.
J. Sun, Y. Liu, and J. S. Dong, “Model checking CSP revisited: Introducing a process analysis toolkit,” in Proc. International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, vol. 17 CCIS, 2008, pp. 307–322.
H. Miyazaki, T. Yokogawa, S. Amasaki, K. Asada, and Y. Sato, “Synthesis and refinement check of sequence diagrams.” IEICE Trans. on Inf. and Syst., vol. E95-D, no. 9, pp. 2193–2201, 2012.
J. Magee and J. Kramer, Concurrency: State Models & Java Programs. New York, NY, USA: John Wiley & Sons, Inc., 1999.
A. Matsumoto, T. Yokogawa, S. Amasaki, K. Arimoto, and H. Aman, “Consistency Verification of UML Sequence Diagrams Modeling Wireless Sensor Networks,” in Proc. 8th International Congress on Advanced Applied Informatics (IIAI-AAI 2019), 2019, pp. 458–461.
C. A. R. Hoare, “Communicating sequential processes,” Commun. ACM, vol. 21, no. 8, pp. 666–677, 1978.
