Formal Requirements Elicitation with FRET

Abstract

FRET is a tool for writing, understanding, formalizing and analyzing requirements. Users write requirements in an intuitive, restricted natural language, called FRETISH, with precise, unambiguous meaning. For a FRETISH requirement, FRET: 1) produces natural language and diagrammatic explanations of its exact meaning, 2) formalizes the requirement in logics, and 3) supports interactive simulation of produced logic formulas to ensure that they capture user intentions. FRET connects to analysis tools by facilitating the mapping between requirements and models/code, and by generating verification code. FRET is available open source at https://github.com/NASA-SW-VnV/fret; a video can be accessed at : https://tinyurl.com/fretForREFSQ.