10th IEEE High Assurance Systems Engineering Symposium (HASE'07)
Utilizing Test Case Generation to Inspect Formal Specifications for Completeness and Feasibility
Dallas, Texas, USA
November 14-November 16
ISBN: 0-7695-3043-5
Completeness and feasibility of a specification are important properties for the assurance of a valid and correct implementation, but they are extremely difficult to be formally verified. In this paper, we describe an inspection method for analyzing the completeness and feasibility of an operation specified using pre- and postconditions. The characteristic of the method is that it utilizes test case generation criteria in forming questions of checklist and test case generation process as a reading technique for inspection. We formally define the properties, the criteria for test case generation, and discuss how they are used for inspection in practice.