FRET2WEST: Exploring translation between temporal logic representations

By: Songyan Lai, Rosemary Monahan

Abstract

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. 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), allowing the integration of FRET with WEST. 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.

Keywords

Safety-critical systems, Formal verification, Temporal logic, FRET, WEST, Toolchain interoperability

Cite as:

Songyan Lai, Rosemary Monahan, “FRET2WEST: Exploring translation between temporal logic representations”, Journal of Object Technology, Volume 25, no. 1 ( 2026), pp. 1:1-18, doi:10.5381/jot.2026.25.1.a2.

DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn