Formal Engineering Methods for Software Development

我们在这个项目上取得了几项重要成果。首先，我们已经将SOFL规范语言和方法发展到了成熟的水平，并完成了一本关于SOFL最新发展的简介一书。其次，通过将形式证明和故障树分析相结合，开发了一种严格审查技术，该技术支持对SOFL规范和其他类型的形式规范进行系统的严格审查。第三，将程序测试技术和形式化证明方法相结合，开发了一种有效的形式化规范验证和验证方法，包括显式规范和隐式规范(如前置条件和后置条件)。通过这种方法，可以在正式规范实现之前对其进行验证和验证。第四，我们探索了形式化求精在捕获完整和准确的用户需求方面的力量，这证明了在提高软件产品的生产率和可靠性方面的潜在有效性，最后，我们研究了如何使用形式化方法来定义、预测和控制软件过程。我们在这个项目上取得的成果有助于将形式化工程方法作为一个新的研究领域。

We have achieved several important results on this project. Firstly, we have developed the SOFL specification language and method into a mature level and completed a book on the introduction to the latest development of SOFL. Secondly, we have developed a rigorous reviews technique by integrating formal proof and fault tree analysis, which supports systematically rigorous reviews of SOFL specifications and other kinds of formal specifications. Thirdly, we have developed an effective testing method for verifying and validating formal specifications, including both explicit and implicit specifications (e.g., with pre and post-conditions), by integrating program testing technique and formal proof approach. By this method formal specifications can be verified and validated before they are implemented. Fourthly, we have explored the power of formal refinement in capturing complete and accurate user requirements, which demonstrates the potential effectiveness in improving the productivity and reliability of software products, finally, we have investigated how formal methods can be used to define, predicate, and control software processes. Our results achieved on this project have contributed to the establishment of Formal Engineering Methods as a new research area.