Utilizing Test Case Generation to Inspect Formal Specifications for Completeness and Feasibility

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.