State Based Static and Dynamic Formal Analysis of UML State Diagrams

Affiliation(s)

Department of Computer Science, College of Computer Sciences and Information Technology, King Faisal University, Hofuf, KSA.

Department of Computer Science, College of Computer Sciences and Information Technology, King Faisal University, Hofuf, KSA.

ABSTRACT

Design and specification is a serious issue in software engineering because of the semantics involved in transforming the real world problems to computer software systems. Unified Modeling Language (UML) has been accepted as a de facto standard for design and specification of object oriented systems. Unfortunately, UML structures lack defining semantics of a system. Formal methods are proved powerful, particularly, at requirement specification and design level. For a moment, formal methods are not welcomed because of much use of mathematics in formal languages. Therefore, a linkage between UML and formal methods is required to overcome the above deficiencies. In this paper, a new approach is developed by integrating UML and Z specification focusing on state diagram considering both the syntax and semantics. It is believed that this new approach will be effective and useful both at academics and industrial level. The resultant formal models of the approach are analyzed and validated using Z/Eves tool.

Design and specification is a serious issue in software engineering because of the semantics involved in transforming the real world problems to computer software systems. Unified Modeling Language (UML) has been accepted as a de facto standard for design and specification of object oriented systems. Unfortunately, UML structures lack defining semantics of a system. Formal methods are proved powerful, particularly, at requirement specification and design level. For a moment, formal methods are not welcomed because of much use of mathematics in formal languages. Therefore, a linkage between UML and formal methods is required to overcome the above deficiencies. In this paper, a new approach is developed by integrating UML and Z specification focusing on state diagram considering both the syntax and semantics. It is believed that this new approach will be effective and useful both at academics and industrial level. The resultant formal models of the approach are analyzed and validated using Z/Eves tool.

Cite this paper

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. doi: 10.4236/jsea.2012.57056.

F. Alhumaidan, "State Based Static and Dynamic Formal Analysis of UML State Diagrams,"

References

[1] B. Akbarpour, S. Tahar and A. Dekdouk, “Formalization of Cadence SPW Fixed-Point Arithmetic in HOL,” Formal Methods in System Design, Vol. 27, 2005, pp. 173-200. doi:10.1007/s10703-005-2256-8

[2] 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 Lumpur, 26-29 August 2007, pp. 539-546.

[3] K. Araki, A. Galloway and K. Taguchi, “Using a Process Algebra to Control B Operations,” Proceedings of 1st International Conference on Integrated Formal Methods, Springer-Verlag, London, 1999, pp. 437-456.

[4] H. Beek, A. Fantechi, S. Gnesi and F. Mazzanti, “State/ Event-Based Software Model Checking,” Proceedings of 4th International Conference on Integrated Formal Methods, Springer, Canterbury, Vol. 2999, 2004, pp. 128-147.

[5] M. Bo, W. Huang and J. Qin, “Automatic Verification of Security Properties of Remote Internet Voting Protocol in Symbolic Model,” Information Technology Journal, Vol. 9, No. 8, 2010, pp. 1521-1556. doi:10.3923/itj.2010.1521.1556

[6] R. Borges and A. Mota, “Integrating UML and Formal Methods,” Electronic Notes in Theoretical Computer Science, Vol. 84, 2003, pp. 97-112.

[7] M. Brendan and J. S. Dong, “Blending Object-Z and Timed CSP: An Introduction to TCOZ,” Proceedings of International Conference on Software Engineering, Kyoto, 19-25 April 1998, pp. 95-104.

[8] W. S. Changchien, J. J. Shen and T. Y. Lin, “A Preliminary Correctness Evaluation Model of Object-Oriented Software Based on UML,” Journal of Applied Sciences, Vol. 2, No. 3, 2002, pp. 356-365. doi:10.3923/jas.2002.356.365

[9] A. Dennis, B. H. Wixom and D. Tegarden, “Systems Analysis and Design with UML,” 3rd Edition, Wiley, New York, 2005, 576 p.

[10] Z. Derakhshandeh, B. T. Ladani and N. Nematbakhsh, “Modeling and Combining Access Control Policies Using Constrained Policy Graph,” Journal of Applied Sciences, Vol. 8, 2008, pp. 3561-3571. doi:10.3923/jas.2008.3561.3571

[11] J. Derrick and G. Smith, “Structural Refinement of Object-Z/CSP Specification,” Proceedings of 2nd International Conference on Integrated Formal Methods, Springer-Verlag, London, Vol. 1945, 2000, pp. 194-213.

[12] S. A. Ehikioya and B. Ola, “A Comparison of Formalisms for Electronic Commerce Systems,” Proceedings of In- ternational Conference on Computational Cybernetics, Vienna, 30 August-1 September 2004, pp. 253-258.

[13] F. Gervais, M. Frappier and R. Laleau, “Synthesizing B Specifications from EB3 Attribute Definitions,” Proceedings of 5th International Conference on Integrated Formal Methods, Springer, Berlin, Vol. 3771, 2005, pp. 207-226.

[14] A. Hall, “Correctness by Construction: Integrating Formality into a Commercial Development Process,” Proceedings of International Symposium of Formal Methods Europe, Vol. 2391, 2002, pp. 139-157.

[15] K. E. Hamdy, M. A. Elsoud and A. M. El-Halawany, “UML-Based Web Engineering Framework for Modeling Web Application,” Journal of Software Engineering, Vol. 5, No. 2, 2011, pp. 49-63. doi:10.3923/jse.2011.49.63

[16] O. Hasan and S. Tahar, “Verification of Probabilistic Properties in the HOL Theorem Prover,” Proceedings of the Integrated Formal Methods, Vol. 4591, 2007, pp. 333-352. doi:10.1007/978-3-540-73210-5_18

[17] X. He, “Formalizing UML Class Diagrams: A Hiera- rchical Predicate Transition Net Approach,” Proceedings of 24th Annual International Computer Software and Applications Conference, Taipei, 25-28 October 2000, pp. 217-222.

[18] M. Heiner and M. Heisel, “Modeling Safety Critical Systems with Z and Petri-Nets,” Proceedings of International Conference on Computer Safety, Reliability and Security, Springer-Verlag, London, 26-28 October 1999, pp. 361-374. doi:10.1007/3-540-48249-0_31

[19] D. Jackson, I. Schechter and I. Shlyakhter, “Alcoa: The Alloy Constraint Analyzer,” Proceedings of International Conference on Software Engineering, Limerick, 4-11 June 2000, pp. 730-733.

[20] 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, 4-6 December 2002, p. 495. doi:10.1109/APSEC.2002.1183053

[21] Liu and C. Chen, “An Improved Quasi-Static Scheduling Algorithm for Mixed Data-Control Embedded Software,” Journal of Applied Sciences, Vol. 6, No. 7, 2006, pp. 1571-1575. doi:10.3923/jas.2006.1571.1575

[22] Z. M. Ma, “Fuzzy Conceptual Information Modeling in UML Data Model,” International Symposium on Computer Science and Computational Technology, Shanghai, 20-22 December 2008, pp. 331-334. doi:10.1109/ISCSCT.2008.353

[23] R. Miles and K. Hamilton, “Learning UML 2.0,” 1st Edition, O’Reilly Media, Sebastopol, 2006, 288 p.

[24] A. Moeini and R. O. Mesbah, “Specification and Development of Database Applications Based on Z and SQL,” Proceedings of International Conference on Information Management and Engineering, Kuala Lumpur, 3-5 April 2009, pp. 399-405.

[25] 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. doi:10.1109/SNPD.2007.508

[26] H. Podeswa, “UML for IT Business Analyst,” 2nd Edition, Course Technology, 2009, 372 p.

[27] T. B. Raymond, “Integrating Formal Methods by Unifying Abstractions,” Springer, Berlin, Vol. 2999, 2004, pp. 441-460.

[28] S. Sengupta and S. Bhattacharya, “Formalization of UML Diagrams and Consistency Verification: A Z Notation Based Approach,” Proceedings of India Software Engineering Conference, Hyderabad, 19-22 February 2008, pp. 151-152. doi:10.1145/1342211.1342248

[29] Z. Shi, “Intelligent Target Fusion Recognition Based on Fuzzy Petri Nets,” Information Technology Journal, Vol. 11, No. 4, 2012, pp. 500-503. doi:10.3923/itj.2012.500.503

[30] M. Shroff and R. B. France, “Towards Formalization of UML Class Structures in Z,” 21st International Conference on Computer Software and Applications, Washington, 11-15 August 1997, pp. 646-651.

[31] J. M. Spivey, “The Z Notation: A Reference Manual,” Prentice-Hall, Englewood Cliffs, 1989.

[32] 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, 4-7 December 2001, pp. 453-460.

[33] X. Than, H. Miao and L. Liu, “Formalizing Semantics of UML Statecharts with Z,” Proceedings of 4th International Conference on Computer & Information Technology, Wuhan, 14-16 September 2004, pp. 1116-1121.

[34] J. M. Wing, “A Specifier, Introduction to Formal Me- thods,” Computer Journal, Vol. 23, No. 9, 1990, pp. 8-24. doi:10.1109/2.58215

[35] Z. Xiuguo and H. Liu, “Formal Verification for CCML Based Web Service Composition,” Information Technology Journal, Vol. 10, No. 9, 2011, pp. 1692-1700.

[36] C. Yong, “Application of Wu’s Method to Proving Total Correctness of Recursive Program,” Information Technology Journal, Vol. 9, No. 7, 2010, pp. 1431-1439. doi:10.3923/itj.2010.1431.1439

[37] N. A. Zafar and F. Alhumaidan, “Transformation of Class Diagrams into Formal Specification,” International Journal Computer Science and Network Security, Vol. 11, No. 5, 2011, pp. 289-295.

[38] 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. doi:10.3923/jas.2006.1712.1719

[39] Z. X. Wu, H. He, L. Chen and Y. Zhang, “Ontology Based Semantics Checking for UML Activity Model,” Information Technology Journal, Vol. 11, No. 3, 2012, pp. 301-306. doi:10.3923/itj.2012.301.306

[40] N. A. Zafar, “Event-Action Based Model for Identification and Formalization of Relations in UML State Diagrams,” Archive De Science Journal, Vol. 65, No. 4, 2012, pp. 17-30.

[1] B. Akbarpour, S. Tahar and A. Dekdouk, “Formalization of Cadence SPW Fixed-Point Arithmetic in HOL,” Formal Methods in System Design, Vol. 27, 2005, pp. 173-200. doi:10.1007/s10703-005-2256-8

[2] 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 Lumpur, 26-29 August 2007, pp. 539-546.

[3] K. Araki, A. Galloway and K. Taguchi, “Using a Process Algebra to Control B Operations,” Proceedings of 1st International Conference on Integrated Formal Methods, Springer-Verlag, London, 1999, pp. 437-456.

[4] H. Beek, A. Fantechi, S. Gnesi and F. Mazzanti, “State/ Event-Based Software Model Checking,” Proceedings of 4th International Conference on Integrated Formal Methods, Springer, Canterbury, Vol. 2999, 2004, pp. 128-147.

[5] M. Bo, W. Huang and J. Qin, “Automatic Verification of Security Properties of Remote Internet Voting Protocol in Symbolic Model,” Information Technology Journal, Vol. 9, No. 8, 2010, pp. 1521-1556. doi:10.3923/itj.2010.1521.1556

[6] R. Borges and A. Mota, “Integrating UML and Formal Methods,” Electronic Notes in Theoretical Computer Science, Vol. 84, 2003, pp. 97-112.

[7] M. Brendan and J. S. Dong, “Blending Object-Z and Timed CSP: An Introduction to TCOZ,” Proceedings of International Conference on Software Engineering, Kyoto, 19-25 April 1998, pp. 95-104.

[8] W. S. Changchien, J. J. Shen and T. Y. Lin, “A Preliminary Correctness Evaluation Model of Object-Oriented Software Based on UML,” Journal of Applied Sciences, Vol. 2, No. 3, 2002, pp. 356-365. doi:10.3923/jas.2002.356.365

[9] A. Dennis, B. H. Wixom and D. Tegarden, “Systems Analysis and Design with UML,” 3rd Edition, Wiley, New York, 2005, 576 p.

[10] Z. Derakhshandeh, B. T. Ladani and N. Nematbakhsh, “Modeling and Combining Access Control Policies Using Constrained Policy Graph,” Journal of Applied Sciences, Vol. 8, 2008, pp. 3561-3571. doi:10.3923/jas.2008.3561.3571

[11] J. Derrick and G. Smith, “Structural Refinement of Object-Z/CSP Specification,” Proceedings of 2nd International Conference on Integrated Formal Methods, Springer-Verlag, London, Vol. 1945, 2000, pp. 194-213.

[12] S. A. Ehikioya and B. Ola, “A Comparison of Formalisms for Electronic Commerce Systems,” Proceedings of In- ternational Conference on Computational Cybernetics, Vienna, 30 August-1 September 2004, pp. 253-258.

[13] F. Gervais, M. Frappier and R. Laleau, “Synthesizing B Specifications from EB3 Attribute Definitions,” Proceedings of 5th International Conference on Integrated Formal Methods, Springer, Berlin, Vol. 3771, 2005, pp. 207-226.

[14] A. Hall, “Correctness by Construction: Integrating Formality into a Commercial Development Process,” Proceedings of International Symposium of Formal Methods Europe, Vol. 2391, 2002, pp. 139-157.

[15] K. E. Hamdy, M. A. Elsoud and A. M. El-Halawany, “UML-Based Web Engineering Framework for Modeling Web Application,” Journal of Software Engineering, Vol. 5, No. 2, 2011, pp. 49-63. doi:10.3923/jse.2011.49.63

[16] O. Hasan and S. Tahar, “Verification of Probabilistic Properties in the HOL Theorem Prover,” Proceedings of the Integrated Formal Methods, Vol. 4591, 2007, pp. 333-352. doi:10.1007/978-3-540-73210-5_18

[17] X. He, “Formalizing UML Class Diagrams: A Hiera- rchical Predicate Transition Net Approach,” Proceedings of 24th Annual International Computer Software and Applications Conference, Taipei, 25-28 October 2000, pp. 217-222.

[18] M. Heiner and M. Heisel, “Modeling Safety Critical Systems with Z and Petri-Nets,” Proceedings of International Conference on Computer Safety, Reliability and Security, Springer-Verlag, London, 26-28 October 1999, pp. 361-374. doi:10.1007/3-540-48249-0_31

[19] D. Jackson, I. Schechter and I. Shlyakhter, “Alcoa: The Alloy Constraint Analyzer,” Proceedings of International Conference on Software Engineering, Limerick, 4-11 June 2000, pp. 730-733.

[20] 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, 4-6 December 2002, p. 495. doi:10.1109/APSEC.2002.1183053

[21] Liu and C. Chen, “An Improved Quasi-Static Scheduling Algorithm for Mixed Data-Control Embedded Software,” Journal of Applied Sciences, Vol. 6, No. 7, 2006, pp. 1571-1575. doi:10.3923/jas.2006.1571.1575

[22] Z. M. Ma, “Fuzzy Conceptual Information Modeling in UML Data Model,” International Symposium on Computer Science and Computational Technology, Shanghai, 20-22 December 2008, pp. 331-334. doi:10.1109/ISCSCT.2008.353

[23] R. Miles and K. Hamilton, “Learning UML 2.0,” 1st Edition, O’Reilly Media, Sebastopol, 2006, 288 p.

[24] A. Moeini and R. O. Mesbah, “Specification and Development of Database Applications Based on Z and SQL,” Proceedings of International Conference on Information Management and Engineering, Kuala Lumpur, 3-5 April 2009, pp. 399-405.

[25] 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. doi:10.1109/SNPD.2007.508

[26] H. Podeswa, “UML for IT Business Analyst,” 2nd Edition, Course Technology, 2009, 372 p.

[27] T. B. Raymond, “Integrating Formal Methods by Unifying Abstractions,” Springer, Berlin, Vol. 2999, 2004, pp. 441-460.

[28] S. Sengupta and S. Bhattacharya, “Formalization of UML Diagrams and Consistency Verification: A Z Notation Based Approach,” Proceedings of India Software Engineering Conference, Hyderabad, 19-22 February 2008, pp. 151-152. doi:10.1145/1342211.1342248

[29] Z. Shi, “Intelligent Target Fusion Recognition Based on Fuzzy Petri Nets,” Information Technology Journal, Vol. 11, No. 4, 2012, pp. 500-503. doi:10.3923/itj.2012.500.503

[30] M. Shroff and R. B. France, “Towards Formalization of UML Class Structures in Z,” 21st International Conference on Computer Software and Applications, Washington, 11-15 August 1997, pp. 646-651.

[31] J. M. Spivey, “The Z Notation: A Reference Manual,” Prentice-Hall, Englewood Cliffs, 1989.

[32] 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, 4-7 December 2001, pp. 453-460.

[33] X. Than, H. Miao and L. Liu, “Formalizing Semantics of UML Statecharts with Z,” Proceedings of 4th International Conference on Computer & Information Technology, Wuhan, 14-16 September 2004, pp. 1116-1121.

[34] J. M. Wing, “A Specifier, Introduction to Formal Me- thods,” Computer Journal, Vol. 23, No. 9, 1990, pp. 8-24. doi:10.1109/2.58215

[35] Z. Xiuguo and H. Liu, “Formal Verification for CCML Based Web Service Composition,” Information Technology Journal, Vol. 10, No. 9, 2011, pp. 1692-1700.

[36] C. Yong, “Application of Wu’s Method to Proving Total Correctness of Recursive Program,” Information Technology Journal, Vol. 9, No. 7, 2010, pp. 1431-1439. doi:10.3923/itj.2010.1431.1439

[37] N. A. Zafar and F. Alhumaidan, “Transformation of Class Diagrams into Formal Specification,” International Journal Computer Science and Network Security, Vol. 11, No. 5, 2011, pp. 289-295.

[38] 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. doi:10.3923/jas.2006.1712.1719

[39] Z. X. Wu, H. He, L. Chen and Y. Zhang, “Ontology Based Semantics Checking for UML Activity Model,” Information Technology Journal, Vol. 11, No. 3, 2012, pp. 301-306. doi:10.3923/itj.2012.301.306

[40] N. A. Zafar, “Event-Action Based Model for Identification and Formalization of Relations in UML State Diagrams,” Archive De Science Journal, Vol. 65, No. 4, 2012, pp. 17-30.