Coherency through formalisations of Structured Natural Language, A case study on FRETish
For practitioners in formal methods and requirements engineering, this work provides a principle to improve consistency across formalization levels, though the contribution is incremental as it focuses on a specific tool and language.
The paper introduces a new guideline called 'Coherency through Formalisations' for requirement formalization, and applies it to NASA's FRET tool by proposing an alternative translation from FRETish to MTL. The new translation is proven equivalent via model checking and shows statistical improvements, while also revealing inconsistencies in the original translation.
Formalisation is the process of writing system requirements in a formal language. These requirements mostly originate in Natural Language. In the field of Formal Methods, formalisation is often identified as one of the most delicate and complicated steps in the verification process. Not seldomly, formalisation tools and environments choose various levels of requirement descriptions: Natural Language, Technical Language, Diagram Representations and Formal Language, to mention a few. In the literature, there are various maxims and principles of good practice to guide the process of requirement formalisation. In this paper we propose a new guideline: Coherency through Formalisations. The guideline states that the different levels of formalisation mentioned above should roughly follow the same logical structure. The principle seems particularly relevant in the setting where LLMs are prompted to perform reasoning tasks that can be checked by formal tools using Structured Natural Language to act as an intermediate layer bridging both paradigms. In the light of coherency, we analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL. We compare our translation to the original translation and prove equivalence using model checking. Some statistics are performed which seem to favor the new translation. As expected, the translation process yielded interesting reflections and revealed inconsistencies which we present and discuss.