Abstract Formal methods enable the verification of system behavior against requirements that are expressed as formal, mathematical properties. However, translating the often ambiguous natural language requirements that are typically produced by developers and engineers into precise mathematical specifications remains a significant bottleneck in the formal verification process. NASA’s Formal Requirements Elicitation Tool ( FRET ) is an open source tool that addresses this challenge by bridging the gap between natural language requirements and formal specifications that are suitable for automated verification. FRET enables practitioners to express requirements in FRETish , a structured natural language, that balances intuitive readability with formal rigor. FRET automatically translates these requirements into formal properties that verification tools can directly process. This tutorial paper introduces FRET and guides readers through expressing requirements in FRETish . We present the tool’s key analysis capabilities, including simulation, realizability checking, test-case generation, and automated generation of verification conditions for external formal verification tools. Our goal is to provide a comprehensive guide that helps practitioners, regardless of their formal methods background, to effectively leverage FRET in their verification and validation (V&V) workflows.

Abstract 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 paper, 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.

Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification, while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed framework unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems.