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
DOI Bookmark:
http://doi.ieeecomputersociety.org/10.1109/HASE.2007.15
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.
Citation:
Shaoying Liu, "Utilizing Test Case Generation to Inspect Formal Specifications for Completeness and Feasibility," hase, pp.349-356, 10th IEEE High Assurance Systems Engineering Symposium (HASE'07), 2007
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||