Realizability Checking of Requirements in FRET

Requirements formalization has become increasingly popular in industrial settings as an
effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis
tools to prove important properties, such as consistency and realizability. In this report,
we present the realizability analysis framework that we developed as part of the Formal
Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs
state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of
conflicts between requirements and simulation of counterexamples, and discuss results from
industrial-level case studies.