Formally Verifying a Transformation from MLTL Formulas to Regular Expressions

TL;DR

This paper presents a formal verification of the WEST algorithm that converts MLTL formulas to regular expressions, ensuring the correctness of the transformation through theorem proving and experimental validation.

Contribution

It provides a formal proof of the WEST algorithm's correctness in Isabelle/HOL and develops verified tools for regular expression equivalence checking.

Findings

The WEST algorithm is proven correct in Isabelle/HOL.

Verified support tools for regular expression equivalence are developed.

Experimental validation confirms the correctness of the WEST tool.

Abstract

Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification logics like STL and MTL, is often used to model and verify real world systems in safety-critical contexts. As the results of formal verification are only as trustworthy as their input specifications, the WEST tool was created to facilitate writing MLTL specifications. Accordingly, it is vital to demonstrate that WEST itself works correctly. To that end, we verify the WEST algorithm, which converts MLTL formulas to (logically equivalent) regular expressions, in the theorem prover Isabelle/HOL. Our top-level result establishes the correctness of the regular expression transformation; we then generate a code export from our verified development and use this to experimentally validate the existing WEST tool. To facilitate this, we develop some verified support for checking the equivalence of two regular expressions.