Research on rigorous verification techniques formal specification and design

我们已经进行了深入的研究，以探索验证正式规格说明和软件系统设计的严格技术，并取得了几个重要的结果。首先，我们将形式验证与故障树分析技术相结合，建立了严格的评审方法。通过这种方法，规范的各种属性的证明义务自动地从规范中派生出来，然后一个评审计划被自动地生成并图形化地表示出来。通过查看此图形表示中的任务，我们可以检查该规范是否存在错误。其次，通过集成程序测试技术和形式证明方法，我们开发了一种有效的测试方法来验证和确认形式规范，包括显式和隐式规范（例如，具有前置和后置条件）。通过这种方法，可以在正式规范实现之前对其进行验证和确认。最后，我们建立了一个软件工具的原型来支持规范测试，并进行了一个案例研究来评估我们的测试方法的有效性。

We have conducted intensive research to explore rigorous techniques for verifying formal specifications and designs of software systems, and achieved several important results. Firstly, we have combined formal verification and the fault tree analysis technique to establish a rigorous reviews method. By this method, proof obligations for various properties of a specification are automatically derived from the specification, and then a review plan is automatically generated and represented graphically. By reviewing the tasks in this graphical representation, we can check whether the specification has faults or not. Secondly, 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. Finally, we have built a prototype of software tool to support specification testing and conducted a case study to evaluate the effectiveness of our testing method.