Mu-FRET Demonstration

Formalisation of natural-language requirements, facilitating automatic translation to other formalisms and the application of refactoring techniques to improve structure

Short Description

MU-FRET is a fork of the Formal Requirements Elicitation Tool (FRET) by a team at Maynooth University, Ireland. FRET is a framework for the elicitation, specification, formalisation and understanding of requirements. It was developed by a Software Verification and Validation team at NASA. In FRET, users enter system requirements in a structured natural language called FRETISH. FRET automatically translates FRETISH requirements to past- and future-time metric temporal logic. MU-FRET extends FRET by adding refactoring functionality. Refactoring, when applied to software, is the process of rearranging the software's internal structure without changing its external behaviour. This is helpful for the maintainability of software, and has similar benefits for requirements.

Use cases

Responsible(s)/Contact(s)

TRL

Demonstrator Evaluation Criterias

Highlights/Rationale of the demonstrator

Transferability Comment Transferability defines how easily the technology can be applied in different systems or areas.

Transferability level 1-Minor, 2-Fair, 3-Good , 4-Very good , 5-Excellent (Minor: The purpose of the technology is connected to a specific system. It is hardly possible or even impossible to adopt the Technology in different systems. Fair: The technology is strongly coupled with another technology that is limited to be used elsewhere (e.g., due to licensing). Good: The technology is developed for a specific purpose but enables modifications to be applied elsewhere. Some specifics must be taken into consideration while adopting it. Very good: The technology is not purpose specific and can be applied elsewhere with small modifications. Excellent: The technology is general, implements standard interfaces, or has already been used in different areas with no or minor modifications.)

Improvement Level 1-Minor, 2-Fair, 3-Good , 4-Very good , 5-Excellent

Demonstrator Result/Measurement of V&V process Improvement List of V&V process improvement measurement based on VALU3S Evaluation Criterias per Use case Test Case and requirement

Demonstrator Result/Measurement of V&V SCP Improvement List of V&V of SCP improvement based on VALU3S Evaluation Criterias per Use case Test Case and requirement

Link to use cases

Qualitative Results

Qualitative Evaluation results obtained through QAM

Demonstrator pitch video Demonstrator pitch video hosted in VALU3S youtube channel

Contents

UC5 Eval Criteria SCP-2/Mapping 1-4

Reduction of requirement violations from the outset by following a methodical requirements elicitation and specification process

UC5 Eval Criteria SCP-2/Mapping 1-3

Construction of Event-B model to verify the system design against the formalised requirements

Qualitative Evaluation results obtained through QAM