F. ALHUMAIDAN
236
stage of developm ent, formal methods a re not sufficient i n
complete modeling of a system. In this way, UML and
formal methods are both useful for design and specific-
ation of software systems but an integration of these
approaches will facilitate the software development proc-
ess which is proposed in this paper.
Based on the identification of limitations, weaknesses
and critical analysis of UML diagrams, an integrated
approach will be proposed and developed for modeling
of complex systems in our future work.
7. Acknowledgements
I would like to thank Deanship of Scientific Research,
King Faisal University (KFU), providing funds for con-
ducting this research. I would like to acknowledge the
Software Engineering Research Group at College of Co-
mputer Sciences and Information Technology, KFU, for
their valuable comments to improve quality of the rese-
arch.
REFERENCES
[1] N. H. Ali, Z. Shukur and S. Idris, “A Design of an As-
sessment System for UML Cla ss Diagram,” International
Conference on Computational Science and Applications,
Kuala Lampur, 26-29 August 2007, pp. 539-546.
doi:10.1109/ICCSA.2007. 31
[2] A. M. Mostafa, A. I. Mana l, E. B. Hatem and E. M. Saa d,
“Toward a Formalization of UML2.0 Meta-Model Using
Z Specifications,” Proceedings of 8th ACIS International
Conference on Software Engineering, Artificial Intelli-
gence, Networking and Parallel/Distributed Computing,
Qingdao, 30 July-1 August 2007, pp. 694-701.
doi:10.1109/SNPD. 2007.508
[3] K. E. Hamdy, M. A. Elsoud and A. M. El-Halawany,
“UML-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
[4] X. He, “Formalizing UML Class Diagrams: A Hierarchi-
cal Predicate Transition Net Approach,” Proceedings of
Twenty-Fourth Annual International Computer Software
and Applications Conference, Taipei, 25-27 October 2000,
pp. 217-222. doi:10.1109/CMPSAC.2000. 884721
[5] M. Shroff and R. B. France, “Towards Formalization of
UML Class Structures in Z,” 21st International Confe-
rence on Computer Software and Applications, Washing-
ton DC, 11-15 August 1997, pp. 646-651.
[6] N. A. Zafar and F. Alhumaidan, “Transformation of Class
Diagrams into Formal Specification,” International Jour-
nal Computer Science and Network Security, Vol. 11, No.
5, 2011, pp. 289-295.
[7] B. Akbarpour, S. Tahar and A. Dekdouk, “Formalization
of Cadence SPW Fixed-Point Arithmetic in HOL,” For-
mal Methods in System Design, Vol. 27, 2005, pp. 173-
200.
[8] H. Beek, A. Fantechi, S. Gnesi and F. Mazzanti, “State/
Event-Based Software Model Checking,” Proceedings of
4th International Conference on Integrated Formal Meth-
ods, Canterbury, 4-7 April 2004, pp. 128-147.
[9] J. Derrick and G. Smith, “Structural Refine ment of Object-
Z/CSP Specification,” Proceedings of 2nd International
Conference on Integrated Formal Methods, Dagstuhl
Castle, 1-3 November 2000, pp. 194-213.
[10] O. Hasan and S. Tahar, “Verification of Probabilistic Pro-
perties in the HOL Theorem Prover,” Proceedings of the
6th International Conference of Integrated Formal Meth-
ods, Oxford, 2-5 July 2007, pp. 333-352.
[11] T. B. Raymond, “Integrating Formal Methods by Uni-
fying Abstractions,” Springer, Berlin, 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, 4-11 June
2000, pp. 730-733. doi:10.1109/ICSE. 2000.870482
[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, 4-7 December 2001, pp. 453-460.
doi:10.1109/APSEC.2001.991514
[14] A. Moeini and R. O. Mesbah, “Specification and Develop-
ment 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. doi:10.1109/ICIME.2009.143
[15] X. G. Zhang and H. Liu, “Formal Verification for CCML
Based Web Service Composition,” Information Techno-
logy Journal, Vol. 10, No. 9, 2011, pp. 1692-1700.
doi:10.3923/ itj.2011.1692.1700
[16] S.-K. Kim and D. Carrington, “An Integrated Framework
with UML and Object-Z for Developing a Precise and
Understandable Specification: The Light Control Case
Study,” Proceedings of 7th Asia-Pacific Software Engi-
neering Conference (APSEC), 5-8 December 2000, pp.
240-248. doi:10.1109/APSEC.2000.896705
[17] M. Heiner, and M. Heisel, “Modeling Safety Critical Sys-
tems with Z and Petri-Nets,” Proceedings of International
Conference on Computer Safety, Reliability and Security,
Toulouse, 27-29 September 1999, pp. 361-374.
[18] E. Cunha, M. Custodio, H. Rocha and R. Barreto, “For-
mal Verification of UML Sequence Diagrams in the Em-
bedded Systems Context,” Brazilian Symposium on Com-
puting System Engineering (SBESC), 2011, pp. 39-45.
[19] H. Leading and J. Souquieres, “Integration of UML and B
Specification Techniques: Sy stematic Transformation from
OCL Expressions into B,” Proceedings of 9th Asia-Pa-
cific Software Engineering Conference, Gold Coast, 4-6
December 2002, p. 495.
[20] 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
[21] C. Yong, “Application of Wu’s Method to Proving Total
Correctness of Recursive Program,” Information Techn-
ology Journal, Vol. 9, No. 7, 2010, pp. 1431-1439.
doi:10.3923/ itj.2010.1431.1439
Copyright © 2012 SciRes. IIM