Towards Explainable Formal Methods: From LTL to Natural Language with Neural Machine Translation | SpringerLink
Skip to main content
Springer Nature Link
Log in

Towards Explainable Formal Methods: From LTL to Natural Language with Neural Machine Translation

  • Conference paper
  • First Online:
Requirements Engineering: Foundation for Software Quality (REFSQ 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13216))

Abstract

[Context and motivation] Requirements formalisation facilitates reasoning about inconsistencies, detection of ambiguities, and identification critical issues in system models. Temporal logic formulae are the natural choice when it comes to formalise requirements associated to desired system behaviours. [Question/problem] Understanding and mastering temporal logic requires a formal background. Means are therefore needed to make temporal logic formulae interpretable by engineers, domain experts and other stakeholders involved in the development process. [Principal ideas/results] In this paper, we propose to use a neural machine translation tool, named OpenNMT, to translate Linear Temporal Logic (LTL) formulae into corresponding natural language descriptions. Our results show that the translation system achieves an average BLEU (BiLingual Evaluation Understudy) score of 93.53%, which corresponds to high-quality translations. [Contribution] Our neural model can be applied to assess if requirements have been correctly formalised. This can be useful to requirements analysts, who may have limited confidence with LTL, and to other stakeholders involved in the requirements verification process. Overall, our research preview contributes to bridging the gap between formal methods and requirements engineering, and opens to further research in explainable formal methods.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 6291
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7864
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Ahmed, Z., et al.: Bringing LTL model checking to biologists. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 1–13. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_1

    Chapter  Google Scholar 

  2. Al-Thanyyan, S.S., Azmi, A.M.: Automated text simplification: a survey. ACM Comput. Surv. (CSUR) 54(2), 1–36 (2021)

    Article  Google Scholar 

  3. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. (TOSEM) 20(4), 1–64 (2011)

    Article  Google Scholar 

  4. Berry, D.M.: Empirical evaluation of tools for hairy requirements engineering tasks. Empirical Softw. Eng. 26(6) (2021). Article number: 111. https://doi.org/10.1007/s10664-021-09986-0

  5. Brunello, A., Montanari, A., Reynolds, M.: Synthesis of LTL formulas from natural language texts: state of the art and research directions. In: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019) (2019)

    Google Scholar 

  6. Clarke, E., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking. Cyber Physical Systems Series. MIT Press, Cambridge (2018)

    MATH  Google Scholar 

  7. Czepa, C., Zdun, U.: On the understandability of temporal properties formalized in linear temporal logic, property specification patterns and event processing language. IEEE Trans. Softw. Eng. 46(1), 100–112 (2018)

    Article  Google Scholar 

  8. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE 1999, pp. 411–420 (1999)

    Google Scholar 

  9. Ferrari, A., ter Beek, M.H.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. (2022). https://doi.org/10.1145/3520480

  10. Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W.: ARSENAL: automatic requirements specification extraction from natural language. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 41–46. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_4

    Chapter  Google Scholar 

  11. Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Automated formalization of structured natural language requirements. IST 137, 106590 (2021)

    Google Scholar 

  12. Gros, D., Sezhiyan, H., Devanbu, P., Yu, Z.: Code to comment “translation”: data, metrics, baselining & evaluation. In: ASE 2020, pp. 746–757. IEEE (2020)

    Google Scholar 

  13. Gupta, A., Agarwal, A., Singh, P., Rai, P.: A deep generative framework for paraphrase generation. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)

    Google Scholar 

  14. Klein, G., Kim, Y., Deng, Y., Senellart, J., Rush, A.: OpenNMT: open-source toolkit for neural machine translation. In: ACL 2017, pp. 67–72 (2017)

    Google Scholar 

  15. Letier, E., Kramer, J., Magee, J., Uchitel, S.: Deriving event-based transition systems from goal-oriented requirements models. Autom. Softw. Eng. 15(2), 175–206 (2008). https://doi.org/10.1007/s10515-008-0027-7

    Article  Google Scholar 

  16. Mavin, A., Wilkinson, P., Harwood, A., Novak, M.: Easy approach to requirements syntax (EARS). In: 2009 17th IEEE International Requirements Engineering Conference, pp. 317–322. IEEE (2009)

    Google Scholar 

  17. Menghi, C., Spoletini, P., Chechik, M., Ghezzi, C.: Supporting verification-driven incremental distributed design of components. In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 169–188. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89363-1_10

    Chapter  Google Scholar 

  18. Nikora, A.P., Balcom, G.: Automated identification of LTL patterns in natural language requirements. In: ISSRE 2009, pp. 185–194. IEEE (2009)

    Google Scholar 

  19. Papineni, K., Roukos, S., Ward, T., Zhu, W.J.: BLEU: a method for automatic evaluation of machine translation. In: ACL 2002, pp. 311–318 (2002)

    Google Scholar 

  20. Siddharthan, A.: A survey of research on text simplification. ITL-Int. J. Appl. Linguist. 165(2), 259–298 (2014)

    Article  Google Scholar 

  21. Van Lamsweerde, A., Letier, E.: Handling obstacles in goal-oriented requirements engineering. IEEE Trans. Softw. Eng. 26(10), 978–1005 (2000)

    Article  Google Scholar 

  22. Wieringa, R.J.: Design Science Methodology for Information Systems and Software Engineering. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43839-8

    Book  Google Scholar 

  23. Zhao, L., et al.: Natural language processing for requirements engineering: a systematic mapping study. ACM Comput. Surv. (CSUR) 54(3), 1–41 (2021)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Kennesaw State University, Atlanta, GA, USA

    Himaja Cherukuri & Paola Spoletini

  2. CNR-ISTI, Pisa, Italy

    Alessio Ferrari

Authors
  1. Himaja Cherukuri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alessio Ferrari
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paola Spoletini
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alessio Ferrari .

Editor information

Editors and Affiliations

  1. University of Pisa, Pisa, Italy

    Vincenzo Gervasi

  2. University of Cologne, Cologne, Germany

    Andreas Vogelsang

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cherukuri, H., Ferrari, A., Spoletini, P. (2022). Towards Explainable Formal Methods: From LTL to Natural Language with Neural Machine Translation. In: Gervasi, V., Vogelsang, A. (eds) Requirements Engineering: Foundation for Software Quality. REFSQ 2022. Lecture Notes in Computer Science, vol 13216. Springer, Cham. https://doi.org/10.1007/978-3-030-98464-9_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-98464-9_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-98463-2

  • Online ISBN: 978-3-030-98464-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation