{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T03:18:43Z","timestamp":1771298323334,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,11]],"date-time":"2020-11-11T00:00:00Z","timestamp":1605052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,11]]},"DOI":"10.1145\/3436829.3436845","type":"proceedings-article","created":{"date-parts":[[2021,1,5]],"date-time":"2021-01-05T11:35:15Z","timestamp":1609846515000},"page":"61-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Formal Requirements Specification"],"prefix":"10.1145","author":[{"given":"Misbah Mehboob","family":"Awan","sequence":"first","affiliation":[{"name":"Department of Computer & Software Engineering, College of E&ME, National University of Sciences and Technology (NUST), Islamabad, Pakistan"}]},{"given":"Farooque","family":"Azam","sequence":"additional","affiliation":[{"name":"Department of Computer & Software Engineering, College of E&ME, National University of Sciences and Technology (NUST), Islamabad, Pakistan"}]},{"given":"Muhammad Waseem","family":"Anwar","sequence":"additional","affiliation":[{"name":"Department of Computer & Software Engineering, College of E&ME, National University of Sciences and Technology (NUST), Islamabad, Pakistan"}]},{"given":"Yawar","family":"Rasheed","sequence":"additional","affiliation":[{"name":"Department of Computer & Software Engineering, College of E&ME, National University of Sciences and Technology (NUST), Islamabad, Pakistan"}]}],"member":"320","published-online":{"date-parts":[[2021,1,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proof in the validation of a formal model of a tracking system for a nuclear plant","author":"Fitzgerald J.S.","year":"1998","unstructured":"J.S. Fitzgerald and C.B. Jones . Proof in the validation of a formal model of a tracking system for a nuclear plant . In J.C. Bicarregui, editor, FACIT Series. Springer-Verlag , 1998 . J.S. Fitzgerald and C.B. Jones. Proof in the validation of a formal model of a tracking system for a nuclear plant. In J.C. Bicarregui, editor, FACIT Series. Springer-Verlag, 1998."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_3_2_1_3_1","volume-title":"An Introduction to Formal Specification and Z","author":"Potter B.","year":"1991","unstructured":"B. Potter , J. Sinclair , and D. Till , An Introduction to Formal Specification and Z . Prentice Hall , 1991 . B. Potter, J. Sinclair, and D. Till, An Introduction to Formal Specification and Z. Prentice Hall, 1991."},{"key":"e_1_3_2_1_4_1","first-page":"72","volume-title":"The Z\/EVES System. 19th International Conference on the Z Formal Method (ZUM)","year":"1997","unstructured":"Saaltink, M.. The Z\/EVES System. 19th International Conference on the Z Formal Method (ZUM) , Reading, UK, LNCS 1212 , pp. 72 -- 88 , 1997 . Saaltink, M.. The Z\/EVES System. 19th International Conference on the Z Formal Method (ZUM), Reading, UK, LNCS 1212, pp. 72--88, 1997."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 2019 7th ICCCM. ACM","year":"2019","unstructured":"Rasheed, Yawar, A Model-Driven Approach for Creating Storyboards of Web Based User Interfaces . Proceedings of the 2019 7th ICCCM. ACM , 2019 Rasheed, Yawar, et al. A Model-Driven Approach for Creating Storyboards of Web Based User Interfaces. Proceedings of the 2019 7th ICCCM. ACM, 2019"},{"issue":"4","key":"e_1_3_2_1_6_1","first-page":"5","article-title":"Proving the shalls","volume":"8","author":"Miller S. P.","year":"2006","unstructured":"S. P. Miller , A. C. Tribble , M. W. Whalen , and M. P. Heimdahl . Proving the shalls . Int. J. Softw. Tools Technol. Transf. , vol. 8 , no. 4 -- 5 , pp. 303--319, Aug. 2006 . S. P. Miller, A. C. Tribble, M. W. Whalen, and M. P. Heimdahl. Proving the shalls. Int. J. Softw. Tools Technol. Transf., vol. 8, no. 4--5, pp. 303--319, Aug. 2006.","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.453.0451"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2000.896705"},{"key":"e_1_3_2_1_9_1","volume-title":"10th International World Wide Web Conference (WWW-10)","author":"Sun Jing","year":"2001","unstructured":"Jing Sun , Jin Song Dong , Jing Liu , Hai Wang , Object- Z Web Environment and Projections to UML , 10th International World Wide Web Conference (WWW-10) , May 2001 . Jing Sun, Jin Song Dong, Jing Liu, Hai Wang, Object-Z Web Environment and Projections to UML, 10th International World Wide Web Conference (WWW-10), May 2001."},{"key":"e_1_3_2_1_10_1","volume-title":"Des Autom Embed Syst","author":"Rashid M.W.","year":"2019","unstructured":"Anwar, M.W. , Rashid , M., Azam, F. et al. A model-driven framework for design and verification of embedded systems through SystemVerilog , Des Autom Embed Syst , 2019 . Anwar, M.W., Rashid, M., Azam, F. et al. A model-driven framework for design and verification of embedded systems through SystemVerilog, Des Autom Embed Syst, 2019."},{"issue":"11","key":"e_1_3_2_1_12_1","first-page":"1217","article-title":"Improving Software Requirements through Formal Methods","volume":"3","author":"Rizvi S.W.A","year":"2013","unstructured":"S.W.A Rizvi , R.A. Khan and R. Asthana . Improving Software Requirements through Formal Methods : A Review. International Journal of Information and Computation Technology. 3 ( 11 ), 1217 -- 1224 , 2013 S.W.A Rizvi, R.A. Khan and R. Asthana. Improving Software Requirements through Formal Methods: A Review. International Journal of Information and Computation Technology. 3(11), 1217--1224, 2013","journal-title":"A Review. International Journal of Information and Computation Technology."},{"key":"e_1_3_2_1_13_1","first-page":"97","volume-title":"Integrating UML and Formal Methods. Electron. Notes Theor. Comput. Sci","author":"Borges R. M.","year":"2007","unstructured":"R. M. Borges and A. C. Mota . Integrating UML and Formal Methods. Electron. Notes Theor. Comput. Sci ., vol. 184 , no. SPEC. ISS. , pp. 97 -- 112 , 2007 . R. M. Borges and A. C. Mota. Integrating UML and Formal Methods. Electron. Notes Theor. Comput. Sci., vol. 184, no. SPEC. ISS., pp. 97--112, 2007."},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of International Conference on ICT4SD, vol 409","author":"Singh","unstructured":"Singh M., Sharma A.K. , Saxena R., Formal Transformation of UML Diagram : Use Case, Class, Sequence Diagram with Z Notation for Representing the Static and Dynamic Perspectives of System . Proceedings of International Conference on ICT4SD, vol 409 . Springer. Singh M., Sharma A.K., Saxena R., Formal Transformation of UML Diagram: Use Case, Class, Sequence Diagram with Z Notation for Representing the Static and Dynamic Perspectives of System. Proceedings of International Conference on ICT4SD, vol 409. Springer."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICOSST.2016.7838579"},{"key":"e_1_3_2_1_16_1","unstructured":"An UML+ Z framework for validating and verifying the Static aspect of Safety Critical System 2016.  An UML+ Z framework for validating and verifying the Static aspect of Safety Critical System 2016."},{"issue":"1","key":"e_1_3_2_1_17_1","article-title":"Transforms Class to Formal Specification By Object-Z","volume":"6","author":"Wasun","year":"2016","unstructured":"Wasun Khan-am . Transforms Class to Formal Specification By Object-Z . International Journal of Applied Computer Technology and Information Systems : Volume 6 , No. 1 , 2016 Wasun Khan-am. Transforms Class to Formal Specification By Object-Z. International Journal of Applied Computer Technology and Information Systems: Volume 6, No.1, 2016","journal-title":"International Journal of Applied Computer Technology and Information Systems"},{"key":"e_1_3_2_1_18_1","first-page":"28","volume":"1","author":"Wu Fangjun","year":"2016","unstructured":"Fangjun Wu , Formalizing UML Model Metrics Using Z Language , Advances in Computer , Signals and Systems 1 : 28 -- 32 , 2016 . Fangjun Wu, Formalizing UML Model Metrics Using Z Language, Advances in Computer, Signals and Systems 1: 28--32, 2016.","journal-title":"Signals and Systems"},{"key":"e_1_3_2_1_19_1","volume-title":"International Journal of Advanced Computer Science and Applications","author":"Awais Muhammad","unstructured":"RaoSohailIqbal, RamzanTalib, HaseebUrRehman, Muhammad Awais , WajidRaza , Formalization of UML Composite Structure using Colored Petri Nets , International Journal of Advanced Computer Science and Applications , Vol. 9 , No. 10, 2018 RaoSohailIqbal, RamzanTalib, HaseebUrRehman, Muhammad Awais, WajidRaza, Formalization of UML Composite Structure using Colored Petri Nets, International Journal of Advanced Computer Science and Applications, Vol. 9, No. 10, 2018"},{"key":"e_1_3_2_1_20_1","first-page":"16","article-title":"Towards Rigorous Transformation Rules for Converting UML Operation Signatures to Z Schema","author":"Grant Emanuel S.","year":"2016","unstructured":"Emanuel S. Grant , Member, IAENG , Tamaike Brown . Towards Rigorous Transformation Rules for Converting UML Operation Signatures to Z Schema . Proceedings of the IMECS , Vol I , 16 -- 18 , 2016 , Hong Kong Emanuel S. Grant, Member, IAENG, Tamaike Brown. Towards Rigorous Transformation Rules for Converting UML Operation Signatures to Z Schema. Proceedings of the IMECS, Vol I, 16--18, 2016, Hong Kong","journal-title":"Proceedings of the IMECS"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRTCCM.2017.59"},{"issue":"4","key":"e_1_3_2_1_22_1","first-page":"3069","article-title":"An integration of uml use case diagram and activity diagram with Z language for formalization of library management system","volume":"9","author":"Muhamad Zainab Hassan","year":"2019","unstructured":"Zainab Hassan Muhamad , An integration of uml use case diagram and activity diagram with Z language for formalization of library management system . International Journal of Electrical and Computer Engineering Vol. 9 , No. 4 , pp. 3069 -- 3076 , 2019 . Zainab Hassan Muhamad, et al. An integration of uml use case diagram and activity diagram with Z language for formalization of library management system. International Journal of Electrical and Computer Engineering Vol. 9, No. 4, pp. 3069--3076, 2019.","journal-title":"International Journal of Electrical and Computer Engineering"},{"key":"e_1_3_2_1_23_1","first-page":"2018","volume-title":"Article ID 6854920, 9","author":"ElMiloudi Khadija","unstructured":"Khadija ElMiloudi and Aziz Ettouhami , A Multiview Formal Model of Use Case Diagrams Using Z Notation: Towards Improving Functional Requirements Quality. Journal of Engineering Volume , Article ID 6854920, 9 pages 2018 , Khadija ElMiloudi and Aziz Ettouhami, A Multiview Formal Model of Use Case Diagrams Using Z Notation: Towards Improving Functional Requirements Quality. Journal of Engineering Volume, Article ID 6854920, 9 pages 2018,"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFRKM.2016.7806329"},{"key":"e_1_3_2_1_25_1","first-page":"225","volume-title":"Deriving formal specification using Z notation. ICCTD, (Vol. 1","author":"R.","year":"2009","unstructured":"Sidek, R. M., & Ahmad, N. Deriving formal specification using Z notation. ICCTD, (Vol. 1 , pp. 225 -- 229 ). IEEE , 2009 . Sidek, R. M., & Ahmad, N. Deriving formal specification using Z notation. ICCTD, (Vol. 1, pp. 225--229). IEEE, 2009."},{"key":"e_1_3_2_1_26_1","volume-title":"14th International Conference on ENASE","year":"2019","unstructured":"RacemBougacha. et al. A Model-based Approach for the Modeling and the Verification of Railway Signaling System , 14th International Conference on ENASE , 2019 . RacemBougacha. et al. A Model-based Approach for the Modeling and the Verification of Railway Signaling System, 14th International Conference on ENASE, 2019."}],"event":{"name":"ICSIE 2020: 2020 9th International Conference on Software and Information Engineering","location":"Cairo Egypt","acronym":"ICSIE 2020","sponsor":["Ain Shams University Ain Shams University, Egypt"]},"container-title":["Proceedings of the 2020 9th International Conference on Software and Information Engineering (ICSIE)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3436829.3436845","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3436829.3436845","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:45:05Z","timestamp":1750268705000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3436829.3436845"}},"subtitle":["Z Notation Meta Model Facilitating Model to Model Transformation"],"short-title":[],"issued":{"date-parts":[[2020,11,11]]},"references-count":25,"alternative-id":["10.1145\/3436829.3436845","10.1145\/3436829"],"URL":"https:\/\/doi.org\/10.1145\/3436829.3436845","relation":{},"subject":[],"published":{"date-parts":[[2020,11,11]]},"assertion":[{"value":"2021-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}