Process and evolution of formal methods in requirements engineering

  • Jorge Hernán Suaza Jiménez Instituto Tecnológico Metropolitano
  • Gloria Amparo Lora Patiño Instituto Tecnológico Metropolitano
Keywords: Formal methods, requirements engineering, software quality, mathematic language


Requirements Engineering is considered the most important phase of the life cycle of software products because it specifies the needs of the customers, and it is also the basis for the execution of the other phases of software engineering. The models currently used to perform the requirements elicitation have been proposed and widely documented, but they are focused only on the techniques to collect information, disregarding the activity of properly documenting this information. Moreover, to structure the requirements specification, natural language continues to be used as a means of communication and understanding with the customer. Due to the ambiguities caused by this language, its interpretation becomes difficult, and this leads to reprocesses in the later stages of the software life cycle. According to the above, it is necessary for software development organizations to consider formalizing the process of requirements elicitation if they wish to make their development process more efficient. A literature review is carried out in this paper to determine the process and evolution of the formal methods from the requirements engineering perspective.

  • References

    [1] Å. Dahlstedt, y A. Persson, “Requirements interdependencies - Moulding the state of research into a research agenda”, en Ninth International Workshop on Requirements Engineering Foundation for Software Quality (REFSQ 2003), Klagenfurt, 2003.

    [2] R. Gore, y S. Diallo, “The need for usable formal methods in verification and validation”, en 2013 Winter Simulation Conference (WSC), Washington, 2013. DOI:

    [3] C. Burgess, The Role of Formal Methods in Software Engineering Education and Industry, Bristol: University of Bristol, 1995.

    [4] P. Zave, “Classification of research efforts in requirements engineering”, ACM Computing Surveys, vol. 29, n.° 4, pp. 315-321, 1997. DOI:

    [5] E. Serna, “Métodos formales e Ingeniería de Software”, Revista Virtual Universidad Católica del Norte, n.° 30, pp. 158-184, 2010, Disponible en:

    [6] L. Mathiassen y A. Munk-Madsen, “Formalization in systems development”, en International Joint Conference on Theory and Practice of Software Development on Formal Methods and Software Development, Berlín, 1985. DOI: https://10.1007/3-540-15199-0_7.

    [7] S. Vilkomir, J. Bowen y A. Ghose, “Formalization and assessment of regulatory requirements for safety-critical software”, Innovations in Systems and Software Engineering, vol. 2, n.° 3-4, pp. 165-178, 2006. DOI: https://10.1007/s11334-006-0006-8.

    [8] C. Webel y R. Gotzhein, “Formalization of Network Quality-of-Service Requirements”, Lecture Notes in Computer Science, vol. 4574, pp. 309-324, 2007. DOI: https://10.1007/978-3-540-73196-2_20.

    [9] M. Schraps y M. Peters, “Semantic annotation of a formal grammar by Semantic Patterns”, en 2014 IEEE 4th International Workshop on Requirements Patterns (RePa), Karlskrona, 2014. DOI: https://10.1109/repa.2014.6894838.

    [10] R. Chatterjee y K. Johari, “A Simplified and Corroborative Approach towards Formalization of Requirements”, Communications in Computer and Information Science, vol. 94, pp. 486-496, 2010. DOI: https://10.1007/978-3-642-14834-7_46.

    [11] R. Cavada, A. Cimatti, A. Micheli, M. Roveri, A. Susi y S. Tonetta, “OthelloPlay – A Plug-in based tool for requirement formalization and validation”, en The 1st workshop on Developing tools as plug-ins – TOPI’11, Honolulu, 2011. DOI: https://10.1145/1984708.1984728.

    [12] A. Post y J. Hoenicke, “Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH”, Lecture Notes in Computer Science, vol. 7152, pp. 225-240, 2012. DOI: https://10.1007/978-3-642-27705-4_18.

    [13] F. Li, J. Horkoff, A. Borgida, G. Guizzardi, L. Liu y J. Mylopoulos, “From Stakeholder Requirements to Formal Specifications Through Refinement”, Requirements Engineering: Foundation for Software Quality, vol. 9013, pp. 164-180, 2015. DOI: https://10.1007/978-3-319-16101-3_11.

    [14] H. Ehrig, G. Engels, F. Orejas y M. Wirsing, “Semi-Formal and Formal Specification Techniques for Software Systems” [internet], 2000. Disponible en:

    [15] C. Snook y M. Butler, “UML-B: Formal Modeling and Design Aided by UML”, ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 15, n.° 1, pp. 92-122, 2006.

    [16] S. Pandey y M. Batra, “Formal methods in requirements phase of SDLC”, International Journal of Computer Applications (0975 – 8887), vol. 70, n.° 13, pp. 7-14, 2013.

    [17] E. Serna y A. Serna, “La especificación formal en contexto: actual y futuro”, Ingeniare– Revista Chilena de Ingeniería, vol. 22, n.° 2, pp. 243-256, 2014. DOI: https://10.4067/S0718-33052014000200010.

    [18] H. Krad, “Formal methods and automation for system verification”, en 2011 Fourth International Conference on Modeling, Simulation and Applied Optimization (ICMSAO 2011), Kuala Lumpur, 2011. DOI: https://10.1109/icmsao.2011.5775479.

    [19] F. Yan, “Studying Formal Methods Applications in CBTC”, en 2011 International Conference on Management and Service Science (MASS2011), Bangkok, 2011. DOI: https://10.1109/icmss.2011.5999325.

    [20] A. Bollin y D. Rauner-Reithmayer, “Formal specification comprehension: the art of reading and writing z”, en The 2nd FME Workshop on Formal Methods in Software Engineering - FormaliSE 2014, Hyderabad, 2014. DOI: https://10.1145/2593489.2593491.

    [21] S. Wolff, “Scrum goes formal: Agile methods for safety-critical systems”, en 2012 First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA), Zurich, 2012. DOI: https://10.1109/formsera.2012.6229784.

    [22] M. Bhavsar, “Analysis of Multiagent Based Interactive Grid Using Formal Methods - A Reliable Approach”, en 2010 3rd International Conference on Emerging Trends in Engineering and Technology, Goa, 2010. DOI: https://10.1109/icetet.2010.5.

    [23] E. Serna, “Métodos formales: Perspectiva y aplicación futura”, en III Jornadas de Investigación de la Facultad de Ingenierías, pp. 64-68, Medellín, 2011.

    [24] M. Bishop, B. Hay y K. Nance, “Applying Formal Methods Informally”, en 2011 44th Hawaii International Conference on System Sciences, Kauai, 2011. DOI: https://10.1109/hicss.2011.71.

    [25] T. de Sousa, J. Almeida, S. Viana y J. Pavón, “Automatic analysis of requirements consistency with the B method”, ACM SIGSOFT Software Engineering Notes, vol. 35, n.° 2, pp. 1-4, 2010. DOI: https://10.1145/1734103.1734114.

    [26] H. Gao y S. Wang, “Based on Formal Methods in Trustable Software Requirements Engineering”, en 2010 International Conference on Internet Technology and Applications, Wuhan, 2010. DOI: https://10.1109/itapp.2010.5566647.

    [27] R. Hassan, M. Eltoweissy, S. Bohner y S. El-Kassas, “Formal analysis and design for engineering security automated derivation of formal software security specifications from goal-oriented security requirements”, IET Software, vol. 4, n.° 2, pp. 149-160, 2010. DOI:https://10.1049/iet-sen.2009.0059.

    [28] J. Van der Poll, “Formal methods in software development: A road less travelled”, South African Computer Journal, vol. 45, pp. 165-178, 2010. DOI: https://10.18489/sacj.v45i0.33.

    [29] M. Singh y M. Patterh, “Formal Specification of Common Criteria Based Access Control Policy Model”, International Journal of Network Security, vol. 11, n.° 3, pp. 139-148, 2010.

    [30] A. Cimatti, M. Roveri, A. Susi y S. Tonetta, “Formalization and Validation of Safety-Critical Requirements”, Electronic Proceedings in Theoretical Computer Science, vol. 20, pp. 68-75, 2010. DOI: https://10.4204/eptcs.20.

    [31] H. Barringer, A. Groce, K. Havelund y M. Smith, “An Entry Point for Formal Methods: Specification and Analysis of Event Logs”, Electronic Proceedings in Theoretical Computer Science, vol. 20, pp. 16-21, 2010. DOI: https://10.4204/eptcs.20.2.

    [32] C. Fernández et al., “Métodos formales aplicados en la industria del software”, Temas de Ciencia y Tecnología, vol. 5, n.° 43, pp. 3-12, 2011. Disponible en:

    [33] N. Ibrahim, V. Alagar y M. Mohammad, “Specification and Verification of Context-dependent Services”, Electronic Proceedings in Theoretical Computer Science, vol. 61, pp. 17-33, 2011. DOI: https://10.4204/eptcs.61.2.

    [34] B. Ammar y K. Abdallah, “Towards the formal specification and verification of multiagent- based systems”, International Journal of Computer Science Issues, vol. 8, n° 4, pp.200-210, 2011.

    [35] A. Kaur, S. Gulati y S. Singh, “A comparative study of two formal specification languages: Z-notation & B-method”, en The Second International Conference on Computational Science, Engineering and Information Technology - CCSEIT ‘12, Coimbatore, 2012. DOI: https://10.1145/2393216.2393304.

    [36] J. You, S. Xia y J. Li, “A survey on formal methods using in software development”, en IET International Conference on Information Science and Control Engineering 2012 (ICISCE 2012), Shenzhen, 2012. DOI: https://10.1049/cp.2012.2353.

    [37] K. Barlas, G. Koletsos y P. Stefaneas, “Extending standards with formal methods: Open Document Architecture”, en 2012 International Symposium on Innovations in Intelligent Systems and Applications, Trabzon, 2012. DOI: https://10.1109/INISTA.2012.6246931.

    [38] A. Bollin, “Do you speak Z? Formal methods under the perspective of a cross-cultural adaptation problem”, en 2013 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE), San Francisco, 2013. DOI: https://10.1109/formalise.2013.6612271.

    [39] E. Serna y A. Serna, “Desafíos y Oportunidades de la Investigación en Métodos Formales”, en XII Conferencia Iberoamericana en Sistemas, Cibernética e Informática, Orlando, 2011.

    [40] J. Atlee, S. Beidu, N. Day, F. Faghih y P. Shaker, “Recommendations for improving the usability of formal methods for product lines”, en 2013 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE), San Francisco, 2013. DOI: https://10.1109/formalise.2013.6612276.

    [41] E. Serna y A. Serna, “Especificación formal - Presente y Futuro”, en XV International Convention and Fair Informatica, La Habana, 2013.

    [42] X. Chen y D. Ouyang, “Research on the Implementation of Internal Control in Enterprise Information System by Domain Analysis and Formal Methods: A Case Study of Sales Activities Internal Control Under Chinese Enterprise Environment”, en 2013 Fourth World Congress on Software Engineering (WCSE 2013), Hong Kong, 2013. DOI: https://10.1109/wcse.2013.31.

    [43] L. Chan, R. Hexel y L. Wen, “Rule-Based Behaviour Engineering: Integrated, Intuitive Formal Rule Modelling”, en 2013 22nd Australian Software Engineering Conference (ASWEC’ 2013), Melbourne, 2013. DOI: https://10.1109/aswec.2013.13.

    [44] M. Noaman, I. Alsmadi y A. Jaradat, “The specifications of E-Commerce Secure System using Z language”, The Research Bulletin of Jordan ACM, vol. II, n.° III, pp. 127-131, 2013.

    [45] J. Lockhart, C. Purdy y P. Wilsey, “Formal methods for safety critical system specification”, en 2014 IEEE 57th International Midwest Symposium on Circuits and Systems (MWSCAS), College Station, 2014. DOI: https://10.1109/mwscas.2014.6908387.

    [46] T. Wu, Y. Dong y N. Hu, “Formal Specification and Transformation Method of System Requirements from B Method to AADL Model”, en 2014 IEEE 17th International Conference on Computational Science and Engineering (CSE 2014), Chengdu, 2014. DOI: https://10.1109/cse.2014.299.

    [47] E. Serna y A. Serna, “Los Métodos Formales en Contexto”, en XIII Conferencia Iberoamericana en Sistemas, Cibernética e Informática (CISCI 2014), Orlando, 2014.

    [48] M. Azeem, M. Ahsan, N. Minhas y K. Noreen, “Specification of e-Health system using Z: A motivation to formal methods”, en International Conference for Convergence for Technology - 2014, Pune, 2014. DOI: https://10.1109/i2ct.2014.7092123.

    [49] Y. Li, X. Pan, T. Hu, S. Sung y H. Yuan, “Specifying Complex Systems in Object-Z: A Case Study of Petrol Supply Systems”, Journal of Software, vol. 9, n.° 7, pp. 1707-1717, 2014. DOI: https://10.4304/jsw.9.7.1707-1717.

    [50] E. Serna y A. Serna, “Perspectiva y Aplicación de los Métodos Formales”, en XIII Conferencia Iberoamericana en Sistemas, Cibernética e Informática, Orlando, 2014.

    [51] R. Jeffery, M. Staples, J. Andronick, G. Klein y T. Murray, “An empirical research agenda for understanding formal methods productivity”, Information and Software Technology, vol. 60, pp. 102-112, 2015. DOI: https://10.1016/j.infsof.2014.11.005.

    [52] S. Tamrakar y A. Sharma, “Comparative Study and Performance Evaluation of Formal Specification Language based on Z, B and VDM Tools”, International Journal of Scientific & Engineering Research, vol. 6, n.° 9, pp. 1540-1543, 2015.

    [53] A. Singh y D. Yadav, “Formal Specification and Verification of Total Order Broadcast through Destination Agreement Using Event-B”, International Journal of Computer Science and Information Technology, vol. 7, n.° 5, pp. 85-95, 2015. DOI: https://10.5121/ijcsit.2015.7506.

    [54] S. Walter, A. Rettberg y M. Kreutz, “Towards Formalized Model-Based Requirements for a Seamless Design Approach in Safety-Critical Systems Development”, en 2015 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, Auckland, 2015. DOI: https://10.1109/isorcw.2015.51.

    [55] A. Serna, “Los Métodos Formales en la Industria”, Revista Antioqueña de las Ciencias Computacionales y la Ingeniería de Software (RACCIS), vol. 2, n.° 2, pp. 44-51, 2012, Disponible en:

  • Author Biographies

    Jorge Hernán Suaza Jiménez, Instituto Tecnológico Metropolitano

    Magíster en ingeniería de software e ingeniero informático. Profesor investigador del Instituto Tecnológico
    Metropolitano, Facultad de Ingeniería, Grupo de Investigación Automática, Electrónica y Ciencias Computacionales.

    Gloria Amparo Lora Patiño, Instituto Tecnológico Metropolitano

    Magister en seguridad informática. Instituto Tecnológico Metropolitano. Correo electrónico: glorialora231287@

How to Cite
Suaza Jiménez, J. H., & Lora Patiño, G. A. (2019). Process and evolution of formal methods in requirements engineering. Revista Ingenierías Universidad De Medellín, 19(37), 119-136.


Download data is not yet available.