This paper gives an overview of previous work in which the authors used NASA's Formal Requirement Elicitation Tool (FRET) to formalise requirements. We discuss four case studies where we used FRET to capture the system's requirements. These formalised requirements subsequently guided the case study specifications in a combination of formal paradigms. For each case study we summarise insights gained during this process, exploring the expressiveness and the potential interoperability of these approaches. Our experience confirms FRET's suitability as a framework for the elicitation and understanding of requirements and for providing traceability from requirements to specification.

翻译：本文综述了作者团队利用NASA形式化需求启发工具(FRET)开展需求形式化的系列研究。我们重点讨论了四个应用FRET捕获系统需求的案例研究，这些形式化需求随后指导了多形式化范式的案例研究规范制定。针对每个案例，我们总结了在此过程中获得的见解，深入探讨了这些方法的表现力与潜在互操作性。实践表明，FRET作为需求启发与理解的框架具有显著适用性，能够有效建立从需求到规范的可追溯链路。