For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method
Masaki NAKAMURA Takahiro SEINO
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2009/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Software Testing
formal specification, proof score, software testing, OTS, CafeOBJ,
Full Text: PDF(233KB)>>
In the OTS/CafeOBJ method, software specifications are described in CafeOBJ executable formal specification language, and verification is done by giving scripts to the CafeOBJ system. The script is called a proof score. In this study, we propose a test case generator from an OTS/CafeOBJ specification together with a proof score. Our test case generator gives test cases by analyzing the proof score. The test cases are used to test whether an implementation satisfies the specification and the property verified by the proof score. Since a proof score involves important information for verifying a property, the generated test cases are also expected to be suitable to test the property.