A Compositional Proof Framework for FRETish Requirements

TL;DR

This paper introduces a formal proof framework for FRETish, a structured natural language for requirements, ensuring precise translation into temporal logic for safety-critical system verification.

Contribution

It provides a rigorous formalization and semantic proof of FRETish requirements, enhancing their reliability in safety-critical system verification.

Findings

Formal denotational semantics for FRETish

Proof of semantic equivalence with temporal logic

Implementation in PVS theorem prover

Abstract

Structured natural languages provide a trade space between ambiguous natural languages that make up most written requirements and mathematical formal specifications such as Linear Temporal Logic. FRETish is a structured natural language for the elicitation of system requirements developed at NASA. The related open-source tool Fret provides support for translating FRETish requirements into temporal logic formulas that can be input to several verification and analysis tools. In the context of safety-critical systems, it is crucial to ensure that a generated formula captures the semantics of the corresponding FRETish requirement precisely. This paper presents a rigorous formalization of the FRETish language including a new denotational semantics and a proof of semantic equivalence between FRETish specifications and their temporal logic counterparts computed by Fret. The complete formalization and the proof have been developed in the Prototype Verification System (PVS) theorem prover.