Formalization of natural language requirements into temporal logics: a survey 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.

Prema: A Tool for Precise Requirements Editing, Modeling and Analysis We present Prema, a tool for Precise Requirement Editing, Modeling and Analysis. It can be used in various fields for describing precise requirements using formal notations and performing rigorous analysis. By parsing the requirements written in formal modeling language, Prema is able to get a model which aptly depicts the requirements. It also provides different rigorous verification and validation techniques to check whether the requirements meet usersu0027 expectation and find potential errors. We show that our tool can provide a unified environment for writing and verifying requirements without using tools that are not well interrelated. For experimental demonstration, we use the requirements of the automatic train protection (ATP) system of CASCO signal co. LTD., the largest railway signal control system manufacturer of China. The code of the tool cannot be released here because the project is commercially confidential. However, a demonstration video of the tool is available at https:youtu.beBX0yv8pRMWs.