DOCSEARCHbyAlgolia
Submit Docs

FRET (Formal Requirements Elicitation Tool)

repository·master·Indexed 19 days ago

https://github.com/nasa-sw-vnv/fret

FRET is a framework for specifying, formalizing, and analyzing system requirements using restricted English, mathematical logic, and visual diagrams. It features multi-representation generation, hierarchical organization, consistency checking, and automated test generation. The tool supports realizability analysis via engines like JKind and Kind 2, and integrates with z3 and NuSMV. It includes the ltlsim-core Javascript API for managing LTL formulas and simulations, and supports exporting requirements to CoCoSpec format for formal verification and testing.

Tokens
108.3K
Snippets
118
Records
609
Agent score
64%

What's inside FRET

  1. Overview of FRET capabilities

    master

    FRET (Formal Requirements Elicitation Tool) is a framework designed for the elicitation, specification, formalization, and understanding of requirements.

    Key features include:

    • Multi-modal representation: Requirements are represented using natural language descriptions, formal mathematical logics, and diagrams to aid semantic review.
    • Hierarchical definition: Requirements can be structured in a hierarchy.
    • Interoperability: Requirements can be exported in various formats for use with external analysis tools.
    • Specialized Language: Users enter requirements using a specialized natural language (FRETish).

  2. Overview of FRET: Formal Requirements Elicitation Tool

    master

    FRET is a framework designed for the elicitation, specification, formalization, and analysis of system requirements. It allows users to define unambiguous requirements using restricted English sentences and provides multiple representations to ensure clarity and semantic validation.

    Key capabilities include:

    • Multi-representation: Generates natural language descriptions, formal mathematical logics, and visual diagrams.
    • Hierarchical Organization: Supports organizing requirements into different levels.
    • Export Capabilities: Supports various formats for integration with external formal analysis tools.
    • Automated Test Generation: Generates requirement-based test cases and provides a coverage metric to assess test adequacy.
    • Consistency Checking: Includes built-in mechanisms to detect conflicts between requirements to ensure completeness and correctness.

  3. What is realizability checking in FRET

    master

    Realizability checking is a formal analysis used to determine if a set of requirements for a system component is realizable. A component is considered realizable if an implementation exists that conforms to all requirements for any possible input from the system's environment.

    FRET offers two modes of analysis:

    1. Monolithic Analysis: Checks the entire set of requirements for a component at once.
    2. Compositional Analysis: Automatically decomposes the original requirements into smaller 'connected components' (sets of requirements expressed over a subset of system outputs). This approach typically yields better performance and provides clearer visibility into requirement dependencies.

    Note on Variable Types: Realizability checking is only supported for System components containing variables of type Input, Output, and Internal. Support for Function types is limited to requirements using Lustre nodes from the pre-defined library at fret-electron/support/CommonTemplates/LibraryOfOperators.ejs.

  4. Understand the [onlyIn,only,immediately,action] pattern

    master

    The [onlyIn,only,immediately,action] pattern is a formal requirement template used to specify conditional actions that must occur under specific constraints.

    Pattern Structure:

    • onlyIn: Specifies the scope or context (e.g., a specific phase or package) where the requirement applies.
    • only: Specifies the specific condition or state that must be met.
    • immediately: Specifies the temporal constraint (the action must happen without delay).
    • action: The system behavior that follows.

    Example Usage:

    only in PackageInstallation, only when lowLevel > highLevel shall the system immediately reset System

    Note: Formal semantics for this pattern (FT and PT) are currently under construction.

  5. Understand the [null,null,null,satisfaction] pattern

    master

    The [null,null,null,satisfaction] pattern is used to express that a component must satisfy a specific condition at some point in the future. This pattern maps to specific temporal logic semantics depending on whether you are using Formal Task (FT) or Property Task (PT) semantics.

    Semantics Mapping

    • FT Semantics: F $post_condition$
    • PT Semantics: O $post_condition$

    Usage

    Description: At some future point, the component $component_name$ shall satisfy $post_condition$.

    Example:

    • Natural Language: "the system shall satisfy (indicationLight = orange)"
    • FT Semantics: F ( indicationLight = orange )
    • PT Semantics: O ( indicationLight = orange )
    • Formal Description: At some future point, the component "system" shall satisfy ( indicationLight = orange ).

  6. Identify the [before,regular,eventually,not_order] pattern in requirements

    master

    The [before,regular,eventually,not_order] pattern identifies requirements that are considered 'meaningless' by the FRET tool. Requirements matching this pattern lack assigned semantics for both Formal Theory (FT) and Property Testing (PT).

    This pattern typically occurs when a requirement combines temporal operators like before and eventually with negation (not) in a way that creates an ambiguous or logically unsound ordering of events.

    Example of a meaningless requirement:

    before PackageInstallation, when lowLevel > highLevel, the system shall eventually not first increment the lowLevel variable and then decrement the highLevel variable

  7. Understand the [before, regular, always, action] pattern

    master

    The [before, regular, always, action] pattern is a formal requirement template currently under development in FRET. It is used to specify a condition that must hold true before a regular event occurs, followed by a mandatory system action.

    Template Structure: before [Event], when [Condition], the system shall always [Action]

    Example: before PackageInstallation, when lowLevel > highLevel, the system shall always reset System

  8. Understand the [before,null,immediately,action] pattern

    master

    The [before,null,immediately,action] pattern identifies a requirement that is considered 'meaningless' within the FRET semantics. This occurs when a requirement specifies a temporal condition (using before) but fails to provide a valid or meaningful trigger/event (the null component) before an action.

    In such cases, the tool cannot assign Formal Theory (FT) or Property Theory (PT) semantics because the precondition for the action is undefined or logically void.

    /* Example of a meaningless requirement matching this pattern: */
// "before PackageInstallation, the system shall immediately reset System"

  9. Understand the [notin,regular,immediately,action] pattern

    master

    The [notin,regular,immediately,action] pattern is a formal requirement template currently under development. It describes a condition where a specific state is not present, a comparison between two levels is met, and an immediate action must follow.

    Pattern Structure Example: when not in <State>, when <LevelA> > <LevelB>, the system shall immediately <Action>

    Example usage: when not in PackageInstallation, when lowLevel > highLevel, the system shall immediately reset System

    Note: Formal semantics for both FT (Formal Template) and PT (Property Template) are currently under construction.

  10. Understand the [notin,regular,within,order] pattern

    master

    The [notin,regular,within,order] pattern is a requirement template currently under formalization. It describes a conditional behavior where, if a specific state is NOT active, a sequence of ordered events must occur within a specified time constraint.

    Pattern Structure: When [Condition A (notin)], when [Condition B (regular)], the system shall [within Time Constraint] [Ordered Event 1] and then [Ordered Event 2].

    Example: "when not in PackageInstallation, when lowLevel > highLevel, the system shall within 10 secs first increment the lowLevel variable and then decrement the highLevel variable"

  11. Understand the [notin,null,immediately,action] pattern

    master

    The [notin,null,immediately,action] pattern is a formal requirement template used in FRET. It describes a state where, if a specific condition (being 'in' a certain state or package) is not met, an immediate action must be taken.

    Example Requirement: "when not in PackageInstallation, the system shall immediately reset System"

    Note: Formal semantics for both FT (Formal Template) and PT (Property Template) are currently under construction.

  12. Understand the [notin,null,immediately,satisfaction] pattern

    master

    The [notin,null,immediately,satisfaction] pattern is a requirement template used for formalizing system behaviors. It describes a state where, if a specific condition is not met (the notin part), the system must transition to or maintain a specific state immediately (the satisfaction part).

    Example Requirement: "when not in PackageInstallation, the system shall immediately satisfy (indicationLight = orange)"

    Note: Formal semantics (FT and PT) for this pattern are currently under construction.