| 講演抄録/キーワード |
| 講演名 |
2007-12-17 11:15
OTS/CafeOBJ法における証明譜からのテスト生成 ○中村正樹(北陸先端大)・清野貴博(産総研) SS2007-42 |
| 抄録 |
(和) |
OTS/CafeOBJ法では,形式仕様言語CafeOBJで仕様を作成し,
証明譜と呼ばれる検証スクリプトにより仕様の形式的な検証を行う.
本研究では,OTS/CafeOBJ仕様およびその証明譜からのテスト生成手法を提案する.
提案するテスト生成手法では,
証明譜に含まれる場合分けなどの情報を指針として適切なテストを与える.
生成されたテストは,実装が仕様および検証された性質を満たすかどうかを検査する. |
| (英) |
In the OTS/CafeOBJ method, we describe a specification in CafeOBJ specification language, and verify it with a proof score. In this study, we propose a test-generating method from an OTS/CafeOBJ specification together with proof scores. Our proposed method gives a suitable tests set by analyzing the proof scores. Generated tests are used to test whether an implementation satisfies the properties verified by the proof scores. |
| キーワード |
(和) |
形式仕様 / 証明譜 / テスト / OTS / CafeOBJ / / / |
| (英) |
Formal specification / Proof score / Software test / OTS / CafeOBJ / / / |
| 文献情報 |
信学技報, vol. 107, no. 392, SS2007-42, pp. 25-30, 2007年12月. |
| 資料番号 |
SS2007-42 |
| 発行日 |
2007-12-10 (SS) |
| ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
| PDFダウンロード |
SS2007-42 |