FRET (software)

FRET (Formal Reasoning and Evaluation Tool) is a software tool developed by the [[NASA Langley Research Center]]'s Safety-Critical Avionics Systems Branch. Its primary purpose is to assist engineers in the development, analysis, and formalization of requirements for [[safety-critical systems]]. FRET aims to bridge the gap between informal natural language requirements and precise formal specifications, facilitating rigorous analysis and verification processes.

Overview

FRET addresses the challenges associated with ambiguity, incompleteness, and inconsistency often found in requirements written in natural language. It provides a structured environment for defining requirements and automatically translates them into various formalisms suitable for analysis by formal verification tools. This helps to detect issues early in the system development lifecycle, significantly reducing potential errors and costs.

Key Features

• Structured Natural Language Input: FRET allows users to write requirements using a controlled or structured subset of English. This approach maintains readability for human engineers while enabling automated processing.
• Formalization Engine: The tool can automatically translate structured natural language requirements into various formal specification languages, such as [[Linear Temporal Logic]] (LTL), [[Computation Tree Logic]] (CTL), or other forms compatible with formal verification tools.
• Consistency and Completeness Checking: FRET can perform automated checks to identify contradictions, redundancies, and potential gaps within a set of requirements.
• Property Generation: It can derive formal properties directly from the stated requirements, which can then be used as inputs for [[model checking]] or [[theorem proving]] tools.
• Traceability: FRET supports linking formal properties back to their original natural language requirements, enhancing traceability throughout the development process.
• Integration with Formal Verification Tools: It is designed to integrate seamlessly with external formal verification tools like [[NuSMV]], [[SPIN]], [[PVS]], and others, by generating outputs in their respective input formats.
• Scenario and Test Case Generation: The tool can assist in generating scenarios or potential test cases based on the formalized requirements, aiding in validation and testing efforts.

Methodology

The typical workflow with FRET involves:

1. Requirement Capture: Engineers input system requirements using FRET's structured natural language interface.
2. Parsing and Formalization: FRET parses these requirements and, with user guidance, translates them into formal logical expressions.
3. Analysis: The tool then performs internal analyses (e.g., consistency checks) and generates output for external formal verification tools.
4. Verification and Validation: Engineers use the generated formal specifications with tools like model checkers to verify system properties or validate designs against requirements.
5. Feedback and Refinement: Any issues discovered during formal analysis are fed back to the requirements engineering process for refinement and correction.

Applications

FRET is primarily utilized in domains where the assurance of correctness and safety is paramount. Its main applications include:

• [[Aerospace engineering]]: For flight control systems, avionics, and critical software.
• [[Automotive industry]]: For autonomous driving systems, engine control units, and safety features.
• [[Medical devices]]: For life-support systems, diagnostic equipment, and medical software.
• Any field requiring high-integrity systems where requirements must be unambiguously defined and formally verifiable.

Benefits

The use of FRET contributes to:

• Early Error Detection: Identifying and correcting requirement flaws early, when they are least costly to fix.
• Reduced Ambiguity: Ensuring requirements are precise and unambiguous, minimizing misinterpretations.
• Improved System Safety and Reliability: Contributing to the development of more robust and dependable systems.
• Enhanced Verification: Providing a solid foundation for the application of formal verification techniques.
• Cost Reduction: By preventing costly rework later in the development cycle.