From Textual to Formal Requirements: A Case Study Using Spectra in Safety-Critical Systems Domain
DOI:
https://doi.org/10.5753/jserd.2024.3745Keywords:
Textual Requirements, Formal Requirements, Spectra specification, Spectra LanguageAbstract
The requirements specification of any system is crucial for the correct development of the systems and software. It becomes even more relevant in the development of safety-critical systems (SCS). This paper aims to investigate the process of transforming requirements specification written in natural language (textual requirements) to requirements specification written in Spectra language (formal requirements). Spectra is a formal language built to specify reactive systems. The case study carried out in this research focuses on the requirements specification of a low-cost insulin infusion pump. The requirements were initially specified in natural language and later transformed into Spectra language. During the transformation process, we investigated the potential use of the Spectra language in the phase of requirements specification, identifying the difficulties in the transformation process and its advantages, taking into account the software engineer's point of view.
Downloads
References
Amram, G., Maoz, S., Segall, I., and Yossef, M. (2022). Dynamic Update for Synthesized GR(1) Controllers. Proc. of ICSE 2022, pp. 786-797, ACM.
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., and Sa’ar, Y. (2012). Synthesis of Reactive(1) Designs. J. Comput. Syst. Sci. 78(3), pp. 911–938. http://dx.doi.org/10.1016/j.jcss.2011.08.007.
Bozzano, M. and Villafiorita, A. (2006). The FSAP/NuSMV-SA Safety Analysis Platform. International Journal on Software Tools for Technology Transfer, 9(1), 5–24. http://doi.org/10.1007/s10009-006-0001-2.
Robson, C. (2002). Real World Research. 2nd Edition. USA: Blackwell Publishers.
Cabral, G. and Sampaio, A. (2008). Formal Specification Generation from Requirement Documents. In: Electronic Notes in Theoretical Computer Science, Vol. 195, 171-188, ISSN 1571-0661, https://doi.org/10.1016/j.entcs.2007.08.032.
Chen, Z. (2009). Formalizing Safety Requirements Using Controlling Automata. In Proceedings of the Second International Conference on Dependability (pp. 81–86). doi:10.1109/DEPEND.2009.18
Gorenstein, A., Maoz, S. and Ringert, J. O. (2024). Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) Specifications. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (ICSE '24). ACM, New York, NY, USA, Article 28, 1–12. https://doi.org/10.1145/3597503.3608131
Hatcliff, J., Wassyng, A., Kelly, T., Comar, C., and Jones, P. (2014). Certifiably safe software-dependent systems: challenges and directions. In Proceedings of the on Future of Software Engineering - FOSE, (pp. 182–200).
Heimdahl, M. P. E. (2007). Safety and Software Intensive Systems: Challenges Old and New. In FoSE 2007: Future of Software Engineering (pp. 137–152).
Hu, Y., Podder, T., Buzurovic, I., Yan, K., Ng, W. S., and Yu, I. (2007). Hazard analysis of EUCLIDIAN: An image-guided robotic brachytherapy system. In Proceedings of the 29th Annual International Conference of the IEEE EMBS (Vol. 1, pp. 1249–1252).
I. Sayar and J. Souquières. (2019). Bridging the Gap Between Requirements Document and Formal Specifications using Development Patterns. In: IEEE 27th International Requirements Engineering Conference Workshops (REW), 2019, pp. 116-122, doi: 10.1109/REW.2019.00026.
Ivarsson, M. and Gorschek, T. (2009). Technology Transfer Decision Support in Requirements Engineering Research: A Systematic Review of REj. Requirements Engineering Journal, vol. 14, no. 3, (pp. 155-175).
Jin, Y., Zhang, J., Hao, W. et al. (2010). A concern-based approach to generating formal requirements specifications. Front. Comput. Sci. China 4, 162–172. https://doi-org.ez69.periodicos.capes.gov.br/10.1007/s11704-010-0151-y.
Leveson, N. G. (2011). Engineering a Safer World: Systems Thinking Applied to Safety. The MIT Press.
Liu, S., Stavridou, V., and Dutertre, B. (1995). The Practice of Formal Methods in Safety-Critical Systems. Journal of Systems and Software, 1212(94), (pp. 77–87).
Ma'ayan, D. and Maoz, S. (2023). Using Reactive Synthesis: An End-to-End Exploratory Case Study," 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), Melbourne, Australia, pp. 742-754, doi: 10.1109/ICSE48619.2023.00071.
Ma'ayan, D., Shahar, M. and Rozi, R. (2022). Validating the Correctness of Reactive Systems Specifications Through Systematic Exploration. Proc. of MODELS 2022, pp. 132-142, ACM.
Maoz, S. and Ringert, J. O. (2019). Spectra Language & Spectra Tools User Guide. [link]
Maoz, S., and Ringert, J. O. (2021a). Reactive Synthesis with Spectra: A Tutorial, IEEE/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), Madrid, ES, pp. 320-321, doi: 10.1109/ICSE-Companion52605.2021.00136.
Maoz, S., Ringert, J.O. (2021b). Spectra: a specification language for reactive systems. Softw Syst Model 20, pp. 1553–1586. https://doi.org/10.1007/s10270-021-00868-z
Martins, L. E. G. and Gorschek, T. (2016). Requirements Engineering for Safety-Critical Systems: A Systematic Literature Review, Information and Software Technology, Vol. 75, July 2016, (pp.71–89).
Martins, L. E. G. and Gorschek, T. (2017). Requirements Engineering for Safety-Critical Systems: Overview and Challenges. IEEE Software, v. 34, (pp. 49-57).
Miller, S. P., Tribble, A. C., Whalen, M. W., and Heimdahl, M. P. E. (2006). Proving the shalls. International Journal on Software Tools for Technology Transfer, 8(4-5), (pp. 303–319). doi:10.1007/s10009-004-0173-6.
Nair, S., de la Vara, J. L., Sabetzadeh, M., and Falessi, D. (2015). Evidence management for compliance of critical systems with safety standards: A survey on the state of practice. Information and Software Technology, 60, (pp. 1–15).
Runeson, P. and Höst, M. (2009). Guidelines for conducting and reporting case study research in software engineering. Empirical Software Engineering, 14, 131–164. http://doi.org/10.1007/s10664-008-9102-8.
Sommerville, I. (2015) Software Engineering. Addison-Wesley, 10th edition.
Walter, B., Hammes, J., Piechotta, M. and S. Rudolph. (2017). A Formalization Method to Process Structured Natural Language to Logic Expressions to Detect Redundant Specification and Test Statements. In: IEEE 25th International Requirements Engineering Conference (RE), pp. 263-272, doi: 10.1109/RE.2017.38.
Wohlin, C., Runeson, P., Host, M., Ohlson, C., Regnell, B. and A. Wesslén. (2012). Experimentation in Software Engineering: An Introduction. Germany: Springer-Verlag.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2024 Luiz Eduardo Galvão Martins
This work is licensed under a Creative Commons Attribution 4.0 International License.
