An Integration of UML Sequence Diagram with Formal Specification Methods—A Formal Solution Based on Z


UML Diagrams are considered as a main component in requirement engineering process and these become an industry standard in many organizations. UML diagrams are useful to show an interaction, behavior and structure of the system. Similarly, in requirement engineering, formal specification methods are also being used in crucial systems where precise information is required. It is necessary to integrate System Models with such formal methods to overcome the requirements errors i.e. contradiction, ambiguities, vagueness, incompleteness and mixed values of abstraction. Our objective is to integrate the Formal Specification Language (Z) with UML Sequence diagram, as sequence diagram is an interaction diagram which shows the interaction and proper sequence of components (Methods, procedures etc.) of the system. In this paper, we focus on components of UML Sequence diagram and then implement these components in formal specification language Z. And the results of this research papers are complete integrated components of Sequence diagram with Z schemas, which are verified by using tools and model based testing technique of Formal Specifications. Results can be more improved by integrating remaining components of Sequence and other UML diagrams into Formal Specification Language.

Share and Cite:

Minhas, N. , Qazi, A. , Shahzadi, S. and Ghafoor, S. (2015) An Integration of UML Sequence Diagram with Formal Specification Methods—A Formal Solution Based on Z. Journal of Software Engineering and Applications, 8, 372-383. doi: 10.4236/jsea.2015.88037.

Conflicts of Interest

The authors declare no conflicts of interest.


[1] Selby, R.W., Basili, V.R. and Baker, F.T. (2006) Cleanroom Software Development: An Empirical Evaluation. IEEE Transactions on Software Engineering, SE-13, 1027-1037.
[2] Chikh, A. (2011) A Knowledge Management Framework in Software Requirements Engineering Based on SECI Model. Journal of Software Engineering and Applications, 4, 718-728.
[3] Flores, F., Mora, M., álvarez, F., et al. (2010) Towards a Systematic Service Oriented Requirement Engineering Process (S-SoRE). Proceedings of the International Conference, CENTERIS 2010, Viana do Castelo, 20-22 October 2010, 111-120.
[4] Batra, M., Malik, A. and Dave, M. (2013) Formal Methods: Benefits, Challenges and Future Direction. Journal of Global Research in Computer Science, 4.
[5] Boehm, B.W. (1984) Verifying and Validating Software Requirements and Design Specifications. IEEE Software Journal, 1, 75-88.
[6] Andriole, S. and Safeguard Sci. Inc. (1998) The Politics of Requirements Management. IEEE Software Journal, 15, 82-84.
[7] Flores, F., Mora, M., álvarez, F., O’Connor, R. and Macias, J. (2008) Handbook of Research on Modern Systems Analysis and Design Technologies and Applications. In: Global, I.G.I., Ed., Chapter VI: Requirements Engineering: A Review of Processes and Techniques, Minnesota State University; Mankato, 96-111.
[8] Rountev, A. and Connell, B.H. (2005) Object Naming Analysis for Reverse-Engineered Sequence Diagrams. Proceedings of the International Conference on Software Engineering, St. Louis, 15-21 May 2005, 254-263.
[9] Zafar, N.A. and Alhumaidan, F. (2013) Scenarios Verification in Sequence Diagram. The Journal of American Science, 9, 287-293.
[10] UML Basics: The Sequence Diagram.
[11] Shroff, M. and France, R.B. (1997) Towards a Formalization of UML Class Structures in Z. The 21st Annual International Computer Software and Applications Conference, 1997 (COMPSAC’ 97), Washington DC, 11-15 August 1997, 646-651.
[12] Sgafiq, S. and Minhas, N.M. (2014) Integrating Formal Methods in XP—A Conceptual Solution. Journal of Software Engineering and Applications, 7, 299-310.
[13] Sengupta, S. and Bhattacharya, S. (2006) Formalization of UML Use Case Diagram—A Z Notation Based Approach.
[14] Black, S., Boca, P.P., Bowen, J.P., Gorman, J. and Hinchey, M. (2009) Formal versus Agile: Survival of the Fittest? IEEE Computer, 42, 37-45.
[15] Fernández-y-Fernández, C.A. and José, M.J. (2012) Towards an Integration of Formal Specification in the áncora Methodology.
[16] Spivey, J.M. (1998) The Z Notation: A Reference Manual. Prentice Hall International, Oxford.
[17] El Miloudi, K., El Armani, Y. and Attouhami, A. (2013) Using Z Formal Specification for Ensuring Consistency in Multi View Modeling. Journal of Theoretical and Applied Information Technology, 57, 407-411.
[18] Staines, T.S. (2007) Supporting UML Sequence Diagrams with a Processor Net Approach. Journal of Software, 2, 64-73.
[19] Alhumaidan, F. and Zafar, N.A. (2013) Automated Semantics Treatment of Sequence Diagram Defining Grammar Rules.
[20] Zafar, N.A. (2006) Modeling and Formal Specification of Automated Train Control System Using Z Notation. IEEE Multi-Topic Conference (INMIC’06), Islamabad, 23-24 December 2006, 438-443.
[21] Zafar, N.A., Khan, S.A. and Araki, K. (2012) Towards the Safety Properties of Moving Block Railway Interlocking System. International Journal of Innovative Computing, Information & Control, 8, 5677-5690.
[22] Heitmeyer, C.L., Jeffords, R.D. and Labaw, B.G. (1996) Automated Consistency Checking of Requirements Specifications. ACM Transactions on Software Engineering and Methodology, 5, 231-261.
[23] Hall, A. (1996) Using Formal Methods to Develop an ATC Information System. IEEE Software, 13, 66-76.
[24] Bano, M. and Zwoghi, D. (2013) User’s Involvement in Requirement Engineering and System Success. IEEE 3rd International Workshop on Empirical Requirement Engineering, Rio de Janeiro, 15 July 2013, 24-31.

Copyright © 2022 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.