| 研究課題/領域番号 |
17K00089
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機システム
|
|---|
| 研究機関 | 石川工業高等専門学校 |
|---|
研究代表者 |
松本 剛史 石川工業高等専門学校, 電子情報工学科, 准教授 (40536140)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2019年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2018年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2017年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | プロパティ検証 / 回路検証 / 機能検証 / 形式的検証 / 検証カバレッジ |
|---|
| 研究成果の概要 |
システム検証の一種であるプロパティ検証と呼ばれる、システムが仕様（プロパティ）を満たすかどうかを確かめる検証方法を対象として、検証がどの程度網羅的に行われているかを示す指標となる検証カバレッジを提案し、その評価を行った。検証においては、システム全体のうち、どの程度の部分が検証できているかを知ることが重要であるが、プロパティ検証ではそのような指標が存在しないため、指標の確立は重要である。本研究では、システムの状態遷移が変化することによって、検証結果がその影響によって変化した場合、検証したプロパティによってその状態遷移が網羅されていると考え、これに基づく検証カバレッジを提案し、評価結果を示した。
|
| 研究成果の学術的意義や社会的意義 |
現在、多くの電子情報機器は大規模なシステムであり、その正しさの検証を効率的に行うことが重要になっている。検証においては、検証対象システムの一部だけを検証しても誤り(バグ)を全て見つけることができないため、どの程度網羅的に検証が行われているかを把握することが必要である。本研究では、システム検証の一種であるプロパティ検証を対象として、検証がどの程度網羅的に行われているかを示す指標を提案し、いくつかの例題において評価を行った。これにより、どれ程のプロパティを検証すれば十分であるかを知る指標とすることができ、さらには、検証結果に対する信頼性・説明可能性が高まることが期待できる。
|
