Model Analysis of Equivalence Classes in UML Events Relations

Nazir Ahmad Zafar

Department of Computer Science, King Faisal University, Hofuf, KSA.

DOI: 10.4236/jsea.2013.612078                

Abstract

Unified Modeling Language (UML) has become a de facto standard for design, specification and modeling of object oriented software systems. UML structures being graphical in nature lack defining semantics of the systems and are prone to causing errors. Formal methods are proved to be a powerful tool for requirement analysis, design and specification of software systems. Hence, linking UML with formal approaches will enhance modeling power of software systems. In this paper, an approach is developed by integrating UML and Z notation focusing on equivalence relation of the state diagrams. The Z is used because it is based on the first order predicate logic having rigorous computer tool support. The reflexivity, symmetry and transitivity properties, being important at design level, are identified and described. It is believed that this approach will be effective and useful at both academics and industrial level. The need, reasoning and benefits of the integrated approach are discussed. The resultant formal models are analyzed and validated using Z/Eves tool.

Keywords

UML; State Diagrams; Equivalence Relations; Formal Methods; Z notation; Validation and Verification

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	R. Borges and A. Mota, “Integrating UML and Formal Methods”, Electronic Notes in Theoretical Computer Science, Vol. 184, 2003, pp. 97-112. http://dx.doi.org/10.1016/j.entcs.2007.03.017
[2]	W. L. Yeung, K. R. P. H. Leung, J. Wang and W. Dong, “Improvements towards Formalizing UML State Diagrams in CSP,” Proceedings of 12th Asia Pacific Software Engineering Conference, Taiwan, 2005, p. 7. http://dx.doi.org/10.1109/APSEC.2005.70
[3]	M. Shroff and R. B. France, “Towards Formalization of UML Class Structures in Z,” 21st International Conference on Computer Software and Applications, Washington, DC, 1997, pp. 646-651.
[4]	A. M. Mostafa, A. I. Manal, E. B. Hatem and E. M. Saad, “Toward a Formalization of UML2.0 Meta-model using Z Specifications,” Proceedings of 8th ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, Qingdao, Vol. 3, 2007, pp. 694-701.
[5]	B. Akbarpour, S. Tahar and A. Dekdouk, “Formalization of Cadence SPW Fixed-Point Arithmetic in HOL,” Formal Methods in System Design, Vol. 27, No. 1-2, 2005, pp. 173-200. http://dx.doi.org/ 10.1007/s10703-005-2256-8
[6]	K. Araki, A. Galloway and K. Taguchi, “Using Process Algebra to Control B Operations,” Proceedings of 1st International Conference on Integrated Formal Methods, London, 1999, pp. 437-456.
[7]	H. Beek, A. Fantechi, S. Gnesi and F. Mazzanti, “State/ Event-Based Software Model Checking,” Proceedings of 4th International Conference on Integrated Formal Methods, Canterbury, Vol. 2999, 2004, pp. 128-147.
[8]	J. Derrick and G. Smith, “Structural Refinement of Object-Z/CSP Specification,” Proceedings of 2nd International Conference on Integrated Formal Methods, London, Vol. 1945, 2000, pp. 194-213. http://dx.doi.org/10.1007/3-540-40911-4_12
[9]	F. Gervais, M. Frappier and R. Laleau, “Synthesizing B Specifications from EB3 Attribute Definitions,” Proceedings of 5th International Conference on Integrated Formal Methods, Berlin/Heidelberg, Vol. 3771, 2005, pp. 207-226. http://dx.doi.org/10.1007/11589976_13
[10]	O. Hasan and S. Tahar, “Verification of Probabilistic Properties in the HOL Theorem Prover,” Proceedings of the Integrated Formal Methods, Oxford, Vol. 4591, 2007, pp. 333-352. http://dx.doi.org/10.1007/978-3-540-73210-5_18
[11]	T. B. Raymond, “Integrating Formal Methods by Unifying Abstractions,” Vol. 2999, 2004, pp. 441-460.
[12]	D. Jackson, I. Schechter and I. Shlyakhter, “Alcoa: The Alloy Constraint Analyzer,” Proceedings of International Conference on Software Engineering, Limerick, 2000, pp. 730-733.
[13]	J. Sun, J. S. Dong, J. Liu and H. Wang, “A XML/XSL Approach to Visualize and Animate TCOZ,” Proceedings of 8th Asia-Pacific Software Engineering Conference, Macao, 2001, pp. 453-460.
[14]	A. Moeini and R. O. Mesbah, “Specification and Development of Database Applications based on Z and SQL,” Proceedings of 2009 International Conference on Information Management and Engineering, Kuala 2009, pp. 399-405.
[15]	M. Heiner and M. Heisel, “Modeling Safety Critical Systems with Z and Petri-Nets,” Proceedings of International Conference on Computer Safety, Reliability and Security, London, 1999, pp. 361-374. http://dx.doi.org/10.1007/3-540-48249-0_31
[16]	H. Leading and J. Souquieres, “Integration of UML and B Specification Techniques: Systematic Transformation from OCL Expressions into B,” Proceedings of 9th Asia-Pacific Software Engineering Conference, Gold Coast, 2002, p. 495.
[17]	Z. M. Ma, “Fuzzy Conceptual Information Modeling in UML Data Model,” International Symposium on Computer Science and Computational Technology, Shanghai, 2008, pp. 331-334. http://dx.doi.org/ 10.1109/ISCSCT.2008.353
[18]	N. H. Ali, Z. Shukur and S. Idris, “A Design of an Assessment System for UML Class Diagram,” International Conference on Computational Science and Applications, Kuala Lampur, 2007, pp. 539-546.
[19]	S. A. Ehikioya and B. Ola, “A Comparison of Formalisms for Electronic Commerce Systems,’ Proceedings of International Conference on Computational Cybernetics, Vienna, 2004, pp. 253-258.
[20]	F. Alhumaidan, “State Based Static and Dynamic Formal Analysis of UML State Diagrams,” Journal of Software Engineering and Applications, Vol. 5 No. 7, 2012, pp. 483-491. http://dx.doi.org/10.4236/ jsea.2012.57056
[21]	Zafar, N. A. “LR(K) Parser Construction Using Bottomup Formal Analysis,” Journal of Software Engineering and Applications, Vol. 5, No. 1, 2012, pp. 21-28. http://dx.doi.org/10.4236/jsea. 2012.51004
[22]	Liu and C. Chen, “An Improved Quasi-Static Scheduling Algorithm for Mixed Data-Control Embedded Software,” Journal of Applied Sciences, Vol. 6, 2006, pp. 1571-1575. http://dx.doi.org/10.3923/jas. 2006.1571.1575
[23]	N. A. Zafar and F. Alsaade, “Syntax-Tree Regular Expression Based DFA Formal Construction,” Intelligent Information Management (IIM), Vol. 4, No. 4, 2012, pp. 138-146. http://dx.doi.org/10. 4236/iim.2012.44021
[24]	N. A. Zafar, A. Hussain and A. Ali, “Verifying Monoid and Group Morphisms over Strongly Connected Algebraic Automata,” Journal of Software Engineering and Applications, Vol. 3, No. 8, 2010, pp. 803-812. http://dx.doi.org/10.4236/jsea.2010.38093
[25]	N. A. Zafar, N. Sabir and A. Ali, “Construction of Intersection of Nondeterministic Finite Automata using Z Notation,” International Journal of Electrical and Computer Engineering, Vol. 3, No. 2, 2008, pp. 96-101.
[26]	N. A. Zafar, “Formal Specification and Validation of Railway Network Components Using Z Notation,” IET, Software, Vol. 3, No. 4, 2009, pp. 312-320. http://dx.doi.org/10.1049/iet-sen.2008.0082
[27]	N. A. Zafar, A. Hussain and A. Ali, “Refinement: Formal Proof of Equivalence in Endomorphisms and Automorphisms over Strongly Connected Automata,” Journal of Software Engineering and Applications, Vol. 2, No. 2, 2009, pp. 77-85. http://dx.doi.org/10.4236/jsea.2009.22012
[28]	Z. Derakhshandeh, B. T. Ladani and N. Nematbakhsh, “Modeling and Combining Access Control Policies Using Constrained Policy Graph (CPG),” Journal of Applied Sciences, Vol. 8, No. 20, 2008, pp. 3561-3571. http://dx.doi.org/10.3923/jas.2008.3561.3571
[29]	X. Than, H. Miao and L. Liu, “Formalizing Semantics of UML Statecharts with Z,” Proceedings of 4th International Conference on Computer & Information Technology, Wuhan, 2004, pp. 1116-1121.
[30]	S. Sengupta and S. Bhattacharya, “Formalization of UML Diagrams and Consistency Verification: A Z Notation Based Approach,” Proceedings of India Software Engineering Conference, 2008, pp. 151-152.
[31]	M. L. Shahreza, B. A. L. Gwandu and D. J. Creasey, “Importance of Formal Specification in Design of Hardware Systems,” IEE Colloquium on Structured Methods for Hardware Systems Design, London, 1994, pp. 1-3.
[32]	A. Hall, “Correctness by Construction: Integrating Formality into a Commercial Development Process,” Proceedings of International Symposium of Formal Methods Europe, Copenhagen, Vol. 2391, 2002, pp. 139-157.
[33]	M. Brendan and J. S. Dong, “Blending Object-Z and Timed CSP: An Introduction to TCOZ,” Proceedings of International Conference on Software Engineering, Kyoto, 1998, pp. 95-104.
[34]	J. M. Spivey, “The Z Notation: A Reference Manual,” Englewood Cliffs NJ, Prentice-Hall, 1989.
[35]	J. M. Wing, “A Specifier, Introduction to Formal Methods,” Computer Journal, Vol. 23, No. 9, 1990, pp. 8-24. http://dx.doi.org/10.1109/2.58215
[36]	S. Zarina, N. Alias, M. M. Halip and B. Idrus, “Formal Specification and Validation of Selective Acknowledgement Protocol Using Z/EVES Theorem Prover,” Journal of Applied Sciences, Vol. 6, No. 8, 2006, pp. 1712-1719. http://dx.doi.org/10.3923/jas.2006.1712.1719
[37]	H. Miao, L. Liu and L. Li, “Formalizing UML Models with Object-Z,” Proceedings of 4th International Conference on Formal Methods and Software Engineering, London, Vol. 2495, 2002, pp. 523-534. http://dx.doi.org/10.1007/3-540-36103-0_53
[38]	N. A. Zafar and F. Alhumaidan, “Transformation of Class Diagrams into Formal Specification,” International Journal of Computer Science and Network Security, Vol. 11, No. 5, 2011, pp. 289-295.
[39]	S. A. Vilkomir and J. P. Bowen, “Formalization of Software Testing Criterion using Z Notation,” 25th Annual International Computer Software and Applications, Chicago, 2001, pp. 351-356.
[40]	X. He, “Formalizing UML Class Diagrams: A Hierarchical Predicate Transition Net Approach,” Proceedings of Twenty-Fourth Annual International Computer Software and Applications Conference, Taipei, 2000, pp. 217-222.
[41]	N. A. Zafar, N. Sabir and A. Ali, “Formal Transformation from NFA to Z Notation by Constructing Union of Regular Languages,” International Journal of Mathematical Models and Methods in Applied Sciences, Vol. 3, No. 2, 2009, pp. 115-122.