PV0 ⊧ FRET (Formal Requirements Elicitation tool)

Application domain/field

• Requirements engineering
• Requirements formalization
• Specification
• Realizability checking

Type of tool

Framework for writing and analyzing requirements

Expected input

Requirements

Format:

Restricted natural language called FRETish (own language)

Expected output

Depends on how the tool is used. It provides a dashboard through which the user can interact with the requirements, including editing, visualization and analysis.

Internals

Uses JKind and Kind 2 to implement realizability checks.

Comments

Developed at NASA