Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method

Masaki NAKAMURA  Takahiro SEINO  

IEICE TRANSACTIONS on Information and Systems   Vol.E92-D   No.5   pp.1012-1021
Publication Date: 2009/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E92.D.1012
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)>>
Buy this Article

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.