Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E92-D No.5 pp.1012-1021
- Publication Date
- 2009/05/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E92.D.1012
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approach)
- Category
- Software Testing
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Masaki NAKAMURA, Takahiro SEINO, "Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method" in IEICE TRANSACTIONS on Information,
vol. E92-D, no. 5, pp. 1012-1021, May 2009, doi: 10.1587/transinf.E92.D.1012.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E92.D.1012/_p
Copy
@ARTICLE{e92-d_5_1012,
author={Masaki NAKAMURA, Takahiro SEINO, },
journal={IEICE TRANSACTIONS on Information},
title={Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method},
year={2009},
volume={E92-D},
number={5},
pages={1012-1021},
abstract={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.},
keywords={},
doi={10.1587/transinf.E92.D.1012},
ISSN={1745-1361},
month={May},}
Copy
TY - JOUR
TI - Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method
T2 - IEICE TRANSACTIONS on Information
SP - 1012
EP - 1021
AU - Masaki NAKAMURA
AU - Takahiro SEINO
PY - 2009
DO - 10.1587/transinf.E92.D.1012
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E92-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2009
AB - 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.
ER -
English
