FRET2WEST: Exploring translation between temporal logic representations.

Software requirements are commonly expressed in natural-language, which must be formalised if they are to be used by formal methods, where we verify that an implementation abides by its requirements during execution.Tools such as Formal Requirements Elicitation Tool (FRET) support this formalization of requirements, and generates Linear Temporal Logic (LTL) for each, providing formulas that can be used in their formal verification, typically via model checking.In this paper, we explore the integration of tools which work with different representations of the requirements.Specifically, we focus on the translation of the LTL output from FRET to Mission-time LTL (MLTL).This allows the integration of FRET with WEST, a tool that transforms MLTL formulas into logically equivalent regular expressions describing the set of all satisfying traces, which facilitates the verification of the specifications via Runtime Verification tools such as R2U2.This integration therefore allows WEST to validate the specifications generated by FRET.Our solution, FRET2WEST, utilizes regular expression-based mapping, variable normalization, and mission-time interval translation to transform FRET's LTL specifications to WEST's MLTL syntax.A proof-of-concept JavaScript translator iteratively constructed through case studies, is added as a feature within the FRET tool.