Formalization of natural language requirements into temporal logics: A survey

Igor Buzhinsky*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


One of the challenges of requirements engineering is the fact that requirements are often formulated in natural language. This represents difficulty if requirements must be processed by formal approaches, especially if these approaches are intended to check the requirements. In model checking, a formal technique of verification by exhaustive state space exploration, requirements must be stated in formal languages (most commonly, temporal logics) which are essentially supersets of the Boolean propositional logic. Translation of natural language requirements to these languages is a process which requires much knowledge and expertise in model checking as well the ability to correctly understand these requirements, and hence automating this process is desirable. This paper reviews existing approaches of requirements formalization that are applicable for, or at least can be adapted to generation of discrete time temporal logic requirements. Based on the review, conclusions are made regarding the practical applicability of these approaches for the considered problem.

Original languageEnglish
Title of host publicationProceedings of the 17th IEEE International Conference on Industrial Informatics, INDIN 2019
Number of pages7
ISBN (Electronic)9781728129273
Publication statusPublished - 1 Jul 2019
MoE publication typeA4 Article in a conference publication
EventIEEE International Conference on Industrial Informatics - Aalto University, Helsinki-Espoo, Finland
Duration: 22 Jul 201925 Jul 2019
Conference number: 17

Publication series

NameIEEE International Conference on Industrial Informatics
ISSN (Print)1935-4576
ISSN (Electronic)2378-363X


ConferenceIEEE International Conference on Industrial Informatics
Abbreviated titleINDIN
Internet address

Fingerprint Dive into the research topics of 'Formalization of natural language requirements into temporal logics: A survey'. Together they form a unique fingerprint.

Cite this