skip to main content
research-article

The Role of Formalism in System Requirements

Published:25 May 2021Publication History
Skip Abstract Section

Abstract

A major determinant of the quality of software systems is the quality of their requirements, which should be both understandable and precise. Most requirements are written in natural language, which is good for understandability but lacks precision.

To make requirements precise, researchers have for years advocated the use of mathematics-based notations and methods, known as “formal.” Many exist, differing in their style, scope, and applicability. The present survey discusses some of the main formal approaches and compares them to informal methods.

The analysis uses a set of nine complementary criteria, such as level of abstraction, tool availability, and traceability support. It classifies the approaches into five categories based on their principal style for specifying requirements: natural-language, semi-formal, automata/graphs, mathematical, and seamless (programming-language-based). It includes examples from all of these categories, altogether 21 different approaches, including for example SysML, Relax, Eiffel, Event-B, and Alloy.

The review discusses a number of open questions, including seamlessness, the role of tools and education, and how to make industrial applications benefit more from the contributions of formal approaches.

References

  1. J. R. Abrial. 2010. Modeling in Event-B: System and Software Engineering. Cambridge University Press.Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. J. R. Abrial, S. A. Schuman, and B. Meyer. 1980. Specification language. In On the Construction of Programs. Cambridge University Press, 343--410.Google ScholarGoogle Scholar
  3. S. Abualhaija, C. Arora, M. Sabetzadeh, L. C. Briand, and E. Vaz. 2019. A machine learning-based approach for demarcating requirements in textual specifications. In RE. IEEE, 51--62.Google ScholarGoogle Scholar
  4. D. Aceituna, H. Do, G. Singh Walia, and S. W. Lee. 2011. Evaluating the use of model-based requirements verification method: A feasibility study. In EmpiRE. IEEE Computer Society, 13--20.Google ScholarGoogle Scholar
  5. L. Aceto, A. Ingólfsdóttir, K. Guldstrand Larsen, and J.í Srba. 2009. Teaching concurrency: Theory in practice. In TFM, Lecture Notes in Computer Science, Vol. 5846. Springer, 158--175.Google ScholarGoogle Scholar
  6. D. Amyot. 2003. Introduction to the user requirements notation: Learning by example. Comput. Netw. 42, 3 (2003), 285--301.Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. P. Arcaini, A. Gargantini, and E. Riccobene. 2017. Rigorous development process of a safety-critical system: From ASM models to Java code. Int. J. Softw. Tools Technol. Transf. 19, 2 (2017), 247--269.Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. P. Arnoux and A. Finkel. 2010. Using mental imagery processes for teaching and research in mathematics and computer science. Int. J. Math. Educ. Sci. Technol. 41, 2 (2010), 229--242.Google ScholarGoogle ScholarCross RefCross Ref
  9. C. Arora, M. Sabetzadeh, L. C. Briand, and F. Zimmer. 2015. Automated checking of conformance to requirements templates using natural language processing. IEEE Trans. Softw. Eng. 41, 10 (2015), 944--968.Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. S. Bechhofer. 2018. OWL: Web ontology language. In Encyclopedia of Database Systems (2nd ed.). Springer.Google ScholarGoogle Scholar
  11. B. Berenbach, F. Schneider, and H. Naughton. 2012. The use of a requirements modeling language for industrial applications. In RE. IEEE Computer Society, 285--290.Google ScholarGoogle Scholar
  12. D. Bjørner and C. B. Jones (Eds.). 1978. The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, Vol. 61. Springer.Google ScholarGoogle Scholar
  13. F. Boniol and V. Wiels. 2014. The landing gear system case study. In ABZ (Case Study), Communications in Computer and Information Science, Vol. 433. Springer, 1--18.Google ScholarGoogle Scholar
  14. P. Bourque and Richard E. Fairley (Eds.). 2014. Guide to the Software Engineering Body of Knowledge (SWEBOK(R)): Version 3.0 (3rd ed.). IEEE Computer Society Press.Google ScholarGoogle Scholar
  15. M. Broy. 2018. A logical approach to systems engineering artifacts: Semantic relationships and dependencies beyond traceability - from requirements to functional and architectural views. Softw. Syst. Model. 17, 2 (2018), 365--393.Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. J. M. Bruel, S. Ebersold, F. Galinier, A. Naumchev, M. Mazzara, and B. Meyer. 2021. The role of formalism in system requirements (additional material). https://github.com/anaumchev/requirements_survey/blob/main/The_role_of_formalism_in_system_requirements___additional_material_.pdf.Google ScholarGoogle Scholar
  17. Capterra. 2015. Retrieved from https://www.capterra.com/requirements-management-software/.Google ScholarGoogle Scholar
  18. J. M. Carrillo-de-Gea, J. Nicolás, J. L. Fernández Alemán, J. A. Toval Álvarez, C. Ebert, and A. Vizcaíno. 2011. Requirements engineering tools. IEEE Softw. 28, 4 (2011), 86--91.Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. N. Cataño and C. Rueda. 2009. Teaching formal methods for the unconquered territory. In TFM, Lecture Notes in Computer Science, Vol. 5846. Springer, 2--19.Google ScholarGoogle Scholar
  20. F. E. Cellier. 1991. Continuous System Modeling. Springer.Google ScholarGoogle Scholar
  21. P. Pin-Shan Chen. 2002. The entity relationship model - Toward a unified view of data (reprint). In Software Pioneers. Springer, Berlin, 311--339.Google ScholarGoogle Scholar
  22. E. F. Codd. 1983. A relational model of data for large shared data banks. Comm. ACM 26, 1 (1983), 64--69.Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. J. L. Colaço, B. Pagano, and M. Pouzet. 2005. A conservative extension of synchronous data-flow with state machines. In EMSOFT. ACM, 173--182.Google ScholarGoogle Scholar
  24. A. Cuccuru, C. Mraidha, F. Terrier, and S. Gérard. 2007. Enhancing UML extensions with operational semantics. In MoDELS, Lecture Notes in Computer Science, Vol. 4735. Springer, 271--285.Google ScholarGoogle Scholar
  25. P. L. da R. Rodrigues, M. Ecar, S. V. Menezes, J. P. S. da Silva, G. T. A. Guedes, and E. de M. Rodrigues. 2018. Empirical evaluation of formal method for requirements specification in agile approaches. In SBSI. ACM, 53:1--53:8.Google ScholarGoogle Scholar
  26. F. Dalpiaz. 2015. Teaching goal modeling in undergraduate education. In iStarT@CAiSE (CEUR Workshop Proceedings), Vol. 1370. CEUR-WS.org, 1--6.Google ScholarGoogle Scholar
  27. A. Dardenne, A. van Lamsweerde, and S. Fickas. 1993. Goal-directed requirements acquisition. Sci. Comput. Program. 20, 1-2 (1993), 3--50.Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. N. Dean and M. Hinchey. 1996. Teaching and Learning Formal Methods. Academic Press.Google ScholarGoogle Scholar
  29. M. dos Santos Soares, J. L. M. Vrancken, and A. Verbraeck. 2011. User requirements modeling and analysis of software-intensive systems. J. Syst. Softw. 84, 2 (2011), 328--339.Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. 1998. Property specification patterns for finite-state verification. In FMSP. ACM, 7--15.Google ScholarGoogle Scholar
  31. Event-b. 2018. Retrieved from http://www.event-b.org/.Google ScholarGoogle Scholar
  32. M. Eysholdt and H. Behrens. 2010. Xtext: Implement your language faster than the quick and dirty way. In SPLASH/OOPSLA Companion. ACM, 307--309.Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. A. Ferrari, F. Dell’Orletta, A. Esuli, V. Gervasi, and S. Gnesi. 2017. Natural language requirements processing: A 4D vision. IEEE Softw. 34, 6 (2017), 28--35.Google ScholarGoogle ScholarCross RefCross Ref
  34. A. Ferrari, G. Gori, B. Rosadini, I. Trotta, S. Bacherini, S. Fantechi, and S. Gnesi. 2018. Detecting requirements defects with NLP patterns: An industrial experience in the railway domain. Emp. Soft. Eng. 23, 6 (2018), 3684--3733.Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. Eclipse foundation. 2015. Papyrus. Retrieved from https://eclipse.org/papyrus/.Google ScholarGoogle Scholar
  36. R. B. France, S. Ghosh, T. T. Dinh-Trong, and A. Solberg. 2006. Model-Driven development using UML 2.0: Promises and pitfalls. Computer 39, 2 (2006), 59--66.Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. M. D. Fraser, K. Kumar, and V. K. Vaishnavi. 1991. Informal and formal requirements specification languages: Bridging the gap. IEEE Trans. Softw. Eng. 17, 5 (1991), 454--466.Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. J. Gibbons and J. Nuno Oliveira (Eds.). 2009. TFM. Lecture Notes in Computer Science, Vol. 5846. Springer.Google ScholarGoogle Scholar
  39. J. P. Gibson and D. Méry. 1998. Teaching formal methods: Lessons to learn. In IWFM (Workshops in Computing). BCS.Google ScholarGoogle Scholar
  40. Mario Gleirscher, Simon Foster, and Jim Woodcock. 2019. New opportunities for integrated formal methods. ACM Comput. Surv. 52, 6, Article 117 (Oct. 2019), 36 pages.Google ScholarGoogle Scholar
  41. Mario Gleirscher and Diego Marmsoler. 2018. Formal methods: Oversold? Underused? A survey. arxiv:1812.08815. Retrieved from https://arxiv.orb/abs/1812.08815.Google ScholarGoogle Scholar
  42. R. Gmehlich, K. Grau, F. Loesch, A. Iliasov, M. Jackson, and M. Mazzara. 2013. Towards a formalism-based toolkit for automotive applications. In FormaliSE@ICSE. IEEE Computer Society, 36--42.Google ScholarGoogle Scholar
  43. F. H. Golra, F. Dagnat, J. Souquières, I. Sayar, and S. Guérin. 2018. Bridging the gap between informal requirements and formal specifications using model federation. In SEFM, Lecture Notes in Computer Science, Vol. 10886. Springer, 54--69.Google ScholarGoogle Scholar
  44. M. T. Grinder. 2002. Animating automata: A cross-platform program for teaching finite automata. In SIGCSE. ACM, 63--67.Google ScholarGoogle Scholar
  45. R. Hähnle, K. Johannisson, and A. Ranta. 2002. An authoring tool for informal and formal requirements specifications. In FASE, Lecture Notes in Computer Science, Vol. 2306. Springer, 233--248.Google ScholarGoogle Scholar
  46. T. Hainey, T. M. Connolly, M. Stansfield, and E. A. Boyle. 2011. Evaluation of a game to teach requirements collection and analysis in software engineering at tertiary education level. Comput. Educ. 56, 1 (2011), 21--35.Google ScholarGoogle ScholarDigital LibraryDigital Library
  47. D. Harel. 1987. Statecharts: A visual formalism for complex systems. Sci. Comput. Program. 8, 3 (1987), 231--274.Google ScholarGoogle ScholarDigital LibraryDigital Library
  48. R. M. Hierons, K. Bogdanov, J. P. Bowen, R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapoor, P. J. Krause, G. Lüttgen, A. J. H. Simons, S. A. Vilkomir, M. R. Woodward, and H. Zedan. 2009. Using formal specifications to support testing. ACM Comput. Surv. 41, 2 (2009), 9:1--9:76.Google ScholarGoogle Scholar
  49. C. A. R. Hoare. 1978. Communicating sequential processes. Commun. ACM 21, 8 (1978), 666--677.Google ScholarGoogle ScholarDigital LibraryDigital Library
  50. C. A. R. Hoare. 2002. An axiomatic basis for computer programming (reprint). In Software Pioneers. Springer, Berlin, 367--383.Google ScholarGoogle Scholar
  51. IBM. 2020. Rational Doors. Retrieved from https://www.ibm.com/products/requirements-management.Google ScholarGoogle Scholar
  52. IBM. 2020. Rational Rhapsody 8.1.5. Retrieved from https://www.ibm.com/products/systems-design-rhapsody.Google ScholarGoogle Scholar
  53. IEEE. 1998. IEEE Recommended Practice for Software Requirements Specifications, IEEE Std 830-1998. DOI:https://doi.org/10.1109/IEEESTD.1998.88286Google ScholarGoogle Scholar
  54. IEEE. 2011. ISO/IEC/IEEE Int. Standard - Systems and Software Engineering -- Life Cycle Processes --Requirements Engineering, ISO/IEC/IEEE 29148:2011(E), 2011.Google ScholarGoogle Scholar
  55. M. H. L. Wong Cheng In. 1994. Informal, Semi-formal, and Formal Approaches to the Specification of Software Requirements. MSc. Dissertation. University of British Columbia.Google ScholarGoogle Scholar
  56. F. Ishikawa, K. Taguchi, N. Yoshioka, and S. Honiden. 2009. What top-level software engineers tackle after learning formal methods: Experiences from the top SE project. In TFM. Lecture Notes in Computer Science, Vol. 5846. Springer, 57--71.Google ScholarGoogle Scholar
  57. D. Jackson. 2006. Software Abstractions—Logic, Language, and Analysis. MIT Press.Google ScholarGoogle Scholar
  58. M. Jackson. 2001. Problem Frames: Analyzing and Structuring Software Development Problems. Addison-Wesley.Google ScholarGoogle Scholar
  59. B. Jeannet and F. Gaucher. 2015. Debugging real-time systems requirements: Simulate the “what” before the “how.” In Embedded World Conf. 6.Google ScholarGoogle Scholar
  60. M. Kassab, C. J. Neill, and P. A. Laplante. 2014. State of practice in requirements engineering: Contemporary data. Innov. Syst. Softw. Eng. 10, 4 (2014), 235--241.Google ScholarGoogle ScholarDigital LibraryDigital Library
  61. L. Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley.Google ScholarGoogle ScholarDigital LibraryDigital Library
  62. P. Laplante. 2017. Requirements Engineering for Software and Systems. Auerbach Publications.Google ScholarGoogle ScholarDigital LibraryDigital Library
  63. P. Gorm Larsen, J. S. Fitzgerald, and S. Riddle. 2009. Practice-oriented courses in formal methods using VDM. Formal Aspects Comput. 21, 3 (2009), 245--257.Google ScholarGoogle ScholarDigital LibraryDigital Library
  64. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. 1998. JML: A Java modeling language. In Formal Underpinnings of Java Workshop (at OOPSLA’98). 404--420.Google ScholarGoogle Scholar
  65. F. L. Li, J. Horkoff, A. Borgida, G. Guizzardi, L. Liu, and J. Mylopoulos. 2015. From stakeholder requirements to formal specifications through refinement. In REFSQ, Lecture Notes in Computer Science, Vol. 9013. Springer, 164--180.Google ScholarGoogle Scholar
  66. S. Liu, K. Takahashi, T. Hayashi, and T. Nakayama. 2009. Teaching formal methods in the context of software engineering. ACM SIGCSE Bull. 41, 2 (2009), 17--23.Google ScholarGoogle ScholarDigital LibraryDigital Library
  67. M. Luckcuck, M. Farrell, L. A. Dennis, C. Dixon, and M. Fisher. 2019. Formal specification and verification of autonomous robotic systems: A survey. ACM Comput. Surv. 52, 5 (2019), 100:1--100:41.Google ScholarGoogle Scholar
  68. R. R. Lutz. 1993. Analyzing software requirements errors in safety-critical, embedded systems. In RE. IEEE Computer Society, 126--133.Google ScholarGoogle Scholar
  69. J. Magee and J. Kramer. 2006. Concurrency—State Models and Java Programs (2. ed.). Wiley.Google ScholarGoogle Scholar
  70. A. Matoussi, F. Gervais, and R. Laleau. 2010. An Event-B Formalization of KAOS Goal Refinement Patterns. [Research Report] TR-LACL-2010-1, LACL. Technical Report. University Paris 12. 1--34 pages.Google ScholarGoogle Scholar
  71. A. Mavin, P. Wilkinson, A. Harwood, and M. Novak. 2009. Easy approach to requirements syntax (EARS). In RE. IEEE Computer Society, 317--322.Google ScholarGoogle Scholar
  72. B. Meyer. 1985. On formalism in specifications. IEEE Softw. 2, 1 (1985), 6--26.Google ScholarGoogle ScholarDigital LibraryDigital Library
  73. B. Meyer. 1988, 1997. Object-Oriented Software Construction (1st and 2nd editions). Prentice Hall.Google ScholarGoogle Scholar
  74. B. Meyer. 2003. A framework for proving contract-equipped classes. In Abstract State Machines, Lecture Notes in Computer Science, Vol. 2589. Springer, 108--125.Google ScholarGoogle Scholar
  75. B. Meyer. 2013. Multirequirements. Modeling and Quality in Req. Engineering (Glinz Festscrhift) (2013).Google ScholarGoogle Scholar
  76. B. Meyer, A. Fiva, I. Ciupa, A. Leitner, Y. Wei, and E. Stapf. 2009. Programs that test themselves. Computer 42, 9 (2009), 46--55.Google ScholarGoogle ScholarDigital LibraryDigital Library
  77. L. Mich. 1996. NL-OOPS: From natural language to object oriented requirements using the natural language processing system LOLITA. Nat. Lang. Eng. 2, 2 (1996), 161--187.Google ScholarGoogle ScholarDigital LibraryDigital Library
  78. L. Mich, M. Franch, and P. Novi Inverardi. 2004. Market research for requirements analysis using linguistic tools. Requir. Eng. 9, 1 (2004), 40--56.Google ScholarGoogle ScholarCross RefCross Ref
  79. R. Milner. 1980. A Calculus of Communicating Systems. Lecture Notes in Computer Science, Vol. 92. Springer.Google ScholarGoogle Scholar
  80. M. L. Minsky. 1967. Computation: Finite and Infinite Machines. Prentice Hall.Google ScholarGoogle ScholarDigital LibraryDigital Library
  81. Modelica. 2017. Retrieved from https://doc.modelica.org/.Google ScholarGoogle Scholar
  82. ModelioSoft. 2017. Retrieved from https://www.modeliosoft.com/products/modelio-sa-system-architects.html.Google ScholarGoogle Scholar
  83. S. Moon, K. Hyung Lee, and D. Lee. 2004. Fuzzy branching temporal logic. IEEE Trans. Syst. Man Cybern. Part B 34, 2 (2004), 1045--1055.Google ScholarGoogle ScholarDigital LibraryDigital Library
  84. T. Nakatani. 2008. Requirements engineering education for professional engineers. In JCKBSE, Frontiers in Artificial Intelligence and Applications, Vol. 180. IOS Press, 495--504.Google ScholarGoogle Scholar
  85. A. Naumchev. 2019. Exigences orientées objets dans un cycle de vie continu. Ph.D. Dissertation. Université de Toulouse, Université Toulouse III-Paul Sabatier.Google ScholarGoogle Scholar
  86. A. Naumchev. 2019. Object-oriented requirements: Reusable, understandable, verifiable. In TOOLS, Lecture Notes in Computer Science, Vol. 11771. Springer, 150--162.Google ScholarGoogle Scholar
  87. A. Naumchev. 2019. Seamless object-oriented requirements. In SIBIRCON. 0743--0748.Google ScholarGoogle Scholar
  88. A. Naumchev and B. Meyer. 2016. Complete contracts through specification drivers. In TASE. IEEE Computer Society, 160--167.Google ScholarGoogle Scholar
  89. A. Naumchev, B. Meyer, M. Mazzara, F. Galinier, J.M. Bruel, and S. Ebersold. 2019. AutoReq: Expressing and verifying requirements for control systems. J. Comput. Lang. 51 (2019), 131--142.Google ScholarGoogle ScholarCross RefCross Ref
  90. A. Naumchev, B. Meyer, and V. Rivera. 2015. Unifying requirements and code: An example. In Ershov Memorial Conference, Lecture Notes in Computer Science, Vol. 9609. Springer, 233--244.Google ScholarGoogle Scholar
  91. T. Nguyen. 2015. Verification of behavioural requirements for complex systems with FORM-L, a MODELICA extension. In ICSSEA.Google ScholarGoogle Scholar
  92. OMG. 2011. Unified Modeling Language, Superstructure, Version 2.4.1. Retrieved from http://www.omg.org/spec/UML/2.4.1.Google ScholarGoogle Scholar
  93. OMG, Sanford Friedenthal, Alan Moore, and Rick Steiner. 2008. SysMl Tutorial. Retrieved from http://www.omgsysml.org/INCOSE-2008-OMGSysML-Tutorial-Final-revb.pdf.Google ScholarGoogle Scholar
  94. Object Management Group (OMG). 2007. OMG Systems Modeling Language (OMG SysML™), V1.0. OMG Document Number: Formal/2007-09-01. Retrieved from http://www.omg.org/spec/SysML/1.0/PDF.Google ScholarGoogle Scholar
  95. Object Management Group (OMG). 2015. UML 2.5. Retrieved from http://www.omg.org/spec/UML/2.5/.Google ScholarGoogle Scholar
  96. S. Ouhbi, A. Idri, J. Luis Fernández Alemán, and A. Toval. 2015. Requirements engineering education: A systematic mapping study. Requir. Eng. 20, 2 (2015), 119--138.Google ScholarGoogle ScholarDigital LibraryDigital Library
  97. R. F. Paige and J. S. Ostroff. 2002. The single model principle. J. Object Technol. 1, 5 (2002), 63--81.Google ScholarGoogle ScholarCross RefCross Ref
  98. D. Lorge Parnas. 2010. Precise documentation: The key to better software. In The Future of Software Engineering. Springer, 125--148.Google ScholarGoogle Scholar
  99. J. L. Peterson. 1977. Petri nets. ACM Comput. Surv. 9, 3 (1977), 223--252.Google ScholarGoogle ScholarDigital LibraryDigital Library
  100. P. Pettersson and K/ G. Larsen. 2000. Uppaal2k. In Bull. Eur. Assoc. for Theoretical Computer Sc., Vol. 70. 40--44.Google ScholarGoogle Scholar
  101. The Overture Project. 2017. Overture Tool: Formal Modelling in VDM. Retrieved from http://overturetool.org/method/.Google ScholarGoogle Scholar
  102. Protégé. 2016. Retrieved from https://protege.stanford.edu/.Google ScholarGoogle Scholar
  103. Aarne Ranta. 2011. Grammatical Framework—Programming with Multilingual Grammars. Cambridge University Press.Google ScholarGoogle Scholar
  104. P. Raymond, Y. Roux, and E. Jahier. 2008. Specifying and executing reactive scenarios with Lutin. Electron. Notes Theor. Comput. Sci. 203, 4 (2008), 19--34.Google ScholarGoogle ScholarDigital LibraryDigital Library
  105. J. N. Reed and J. E. Sinclair. 2004. Motivating study of formal methods in the classroom. In TFM, Lecture Notes in Computer Science, Vol. 3294. Springer, 32--46.Google ScholarGoogle Scholar
  106. Respect-it. 2011. Objectiver V3. Retrieved from http://www.objectiver.com.Google ScholarGoogle Scholar
  107. A. B. Romanovsky and M. Thomas (Eds.). 2013. Industrial Deployment of System Engineering Methods. Springer.Google ScholarGoogle Scholar
  108. A. W. Roscoe. 1997. The Theory and Practice of Concurrency. Prentice Hall.Google ScholarGoogle ScholarDigital LibraryDigital Library
  109. R. E. Schneider and D. M. Buede. 2000. Properties of a high quality informal requirements document. INCOSE Springer Symp. 10, 1 (Jul. 2000), 352--359.Google ScholarGoogle Scholar
  110. S. A. Schneider, H. Treharne, and H. Wehrheim. 2014. The behavioural semantics of Event-B refinement. Formal Aspects Comput. 26, 2 (2014), 251--280.Google ScholarGoogle ScholarDigital LibraryDigital Library
  111. W. Scott and S. Cook. 2004. A context-free requirements grammar to facilitate automatic assessment. In AWRE. 4.1--4.10.Google ScholarGoogle Scholar
  112. J. Slankas and L. Williams. 2013. Automated extraction of non-functional requirements in available documentation. In NaturaLiSE. IEEE Computer Society, 9--16.Google ScholarGoogle Scholar
  113. SPIN / Promela. 2020. Retrieved from http://spinroot.com/spin/Man/promela.html.Google ScholarGoogle Scholar
  114. State Chart XML (SCXML) 2012. State Chart XML (SCXML): State Machine Notation for Control Abstraction. W3C Working Draft 16 February 2012. Retrieved from https://www.w3.org/TR/scxml/.Google ScholarGoogle Scholar
  115. Stimulus. 2015. Retrieved from http://argosim.com/product-overview/.Google ScholarGoogle Scholar
  116. I. Stoica, R. Tappan Morris, D. R. Karger, M. F. Kaashoek, and H. Balakrishnan. 2001. Chord: A scalable peer-to-peer lookup service for internet applications. SIGCOMM Comput. Commun. Rev. 31, 4 (October 2001), 149--160.Google ScholarGoogle ScholarDigital LibraryDigital Library
  117. W. Su and J. R. Abrial. 2017. Aircraft landing gear system: Approaches with Event-B to the modeling of an industrial system. Int. J. Softw. Tools Technol. Transf. 19, 2 (2017), 141--166.Google ScholarGoogle ScholarDigital LibraryDigital Library
  118. Dassault Systems. 2016. CATIA Reqtify. Retrieved from https://www.3ds.com/products-services/catia/products/reqtify.Google ScholarGoogle Scholar
  119. Sparx Systems. 2017. Enterprise Architect. Retrieved from https://sparxsystems.eu/enterprisearchitect/system-requirements/.Google ScholarGoogle Scholar
  120. S. Tarkan and V. Sazawal. 2009. Chief chefs of Z to Alloy: Using a kitchen example to teach Alloy with Z. In TFM, Lecture Notes in Computer Science,Vol. 5846. Springer, 72--91.Google ScholarGoogle Scholar
  121. Thomas Tilley, Richard Cole, Peter Becker, and Peter W. Eklund. 2005. A survey of formal concept analysis support for software engineering activities. In Formal Concept Analysis, Lecture Notes in Computer Science, Vol. 3626. Springer, 250--271.Google ScholarGoogle Scholar
  122. N. Tillmann, F. Chen, and W. Schulte. 2006. Discovering likely method specifications. In ICFEM, Lecture Notes in Computer Science, Vol. 4260. Springer, 717--736.Google ScholarGoogle Scholar
  123. N. Tillmann and J. de Halleux. 2008. Pex-white box test generation for .NET. In TAP, Lecture Notes in Computer Science, Vol. 4966. Springer, 134--153.Google ScholarGoogle Scholar
  124. N. Tillmann and W. Schulte. 2005. Parameterized unit tests. In ESEC/SIGSOFT FSE. ACM, 253--262.Google ScholarGoogle Scholar
  125. J. Tschannen, C. A. Furia, M. Nordio, and N. Polikarpova. 2015. AutoProof: Auto-active functional verification of object-oriented programs. In TACAS, Lecture Notes in Computer Science,Vol. 9035. Springer, 566--580.Google ScholarGoogle Scholar
  126. A. van Lamsweerde. 2000. Formal specification: A roadmap. In ICSE–Future of SE Track. ACM, 147--159.Google ScholarGoogle Scholar
  127. A. van Lamsweerde. 2001. Goal-oriented requirements engineering: A guided tour. In RE. IEEE Computer Society, 249.Google ScholarGoogle Scholar
  128. A. van Lamsweerde. 2004. Goal-oriented requirements engineering: A roundtrip from research to practice. In RE.IEEE Computer Society, 4--8.Google ScholarGoogle Scholar
  129. M. von der Beeck. 1994. A comparison of statecharts variants. In FTRTFT, Lecture Notes in Computer Science,Vol. 863. Springer, 128--148.Google ScholarGoogle Scholar
  130. J. Whittle, P. Sawyer, N. Bencomo, B. H. C. Cheng, and J.M. Bruel. 2009. RELAX: Incorporating uncertainty into the specification of self-adaptive systems. In RE. IEEE Computer Society, 79--88.Google ScholarGoogle Scholar
  131. K. Wiegers and J. Beatty. 2013. Software Requirements. Pearson Education.Google ScholarGoogle Scholar
  132. Jeannette M. Wing. 1988. A study of 12 specifications of the library problem. IEEE Softw. 5, 4 (1988), 66--76.Google ScholarGoogle ScholarDigital LibraryDigital Library
  133. Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. 2009. Formal methods: Practice and experience. ACM Comput. Surv. 41, 4 (2009), 19:1--19:36.Google ScholarGoogle Scholar
  134. E. Yu. 1997. Towards modelling and reasoning support for early-phase requirements engineering. In ISRE. IEEE Computer Society, 226--235.Google ScholarGoogle Scholar
  135. E. S. K. Yu and J. Mylopoulos. 1998. Why goal-oriented requirements engineering. In REFSQ. Presses Universitaires de Namur, 15--22.Google ScholarGoogle Scholar
  136. P. Zave. 2017. Reasoning about identifier spaces: How to make chord correct. IEEE Trans. Softw. Eng. 43, 12 (2017), 1144--1156.Google ScholarGoogle ScholarDigital LibraryDigital Library
  137. P. Zave and M. Jackson. 1997. Four dark corners of requirements engineering. ACM Trans. Softw. Eng. Methodol. 6, 1 (1997), 1--30.Google ScholarGoogle ScholarDigital LibraryDigital Library
  138. L. Zhao, W. Alhoshan, A. Ferrari, K. J. Letsholo, M. A. Ajagbe, E. V. Chioasca, and R. T. Batista-Navarro. 2020. Natural language processing (NLP) for requirements engineering: A systematic mapping study. CoRR abs/2004.01099 (2020).Google ScholarGoogle Scholar
  139. D. Zowghi and S. Paryani. 2003. Teaching requirements engineering through role playing: Lessons learnt. In RE. IEEE Computer Society, 233.Google ScholarGoogle Scholar

Index Terms

  1. The Role of Formalism in System Requirements

      Recommendations

      Comments

      Login options

      Check if you have access through your login credentials or your institution to get full access on this article.

      Sign in

      Full Access

      • Published in

        cover image ACM Computing Surveys
        ACM Computing Surveys  Volume 54, Issue 5
        June 2022
        719 pages
        ISSN:0360-0300
        EISSN:1557-7341
        DOI:10.1145/3467690
        Issue’s Table of Contents

        Copyright © 2021 ACM

        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        • Published: 25 May 2021
        • Accepted: 1 February 2021
        • Revised: 1 September 2020
        • Received: 1 April 2020
        Published in csur Volume 54, Issue 5

        Permissions

        Request permissions about this article.

        Request Permissions

        Check for updates

        Qualifiers

        • research-article
        • Research
        • Refereed

      PDF Format

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      HTML Format

      View this article in HTML Format .

      View HTML Format