Coherency through formalisations of Structured Natural Language, A case study on FRETish

TL;DR

This paper introduces a new guideline for requirement formalisation called Coherency through Formalisations, emphasizing consistent logical structure across different formalisation levels, and applies it to FRETish with a novel translation approach.

Contribution

It proposes a new formalisation guideline and demonstrates its application to FRETish, including an automated translation to MTL and a comparison with existing methods.

Findings

The new translation of FRETish to MTL is proven equivalent via model checking.

Statistics favor the new translation over the original.

The process revealed inconsistencies and prompted reflections on formalisation.

Abstract

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.