| Research Abstract |
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.
|
