2019 Fiscal Year Research-status Report
| Project/Area Number |
17K00089
|
|---|
| Research Institution | Ishikawa National College of Technology |
|---|
Principal Investigator |
松本 剛史 石川工業高等専門学校, 電子情報工学科, 准教授 (40536140)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 機能検証 / プロパティ検証 |
|---|
| Outline of Annual Research Achievements |
本研究では、回路が満たすべき性質（プロパティ）をどのような入力パタン（または、シーケンス）に対しても満たしているかどうかを調べるプロパティ検証における検証の網羅性を定義し、算出することを目的としている。与えられたテストパターン（または、シーケンス）によって回路やプログラムの検証を行う場合、様々なカバレッジ指標が実用されているが、プロパティ検証ではそのような指標が存在していないため、有効な指標を開発することは重要である。
令和元年度の成果としては、状態遷移システムにおいて、システムが持つ状態遷移のうち、その有無がプロパティ検証の検証結果に影響を与える割合をプロパティ網羅性の指標として提案し、評価結果を得た。もし、検証対象の状態遷移システムに対してあるプロパティを検証した結果と、検証対象のシステムからある状態遷移を削除して得られるシステムで同じプロパティを検証した結果が異なるのであれば、削除された状態遷移はプロパティの検証でチェックされていると考えられる。そのため、そのプロパティの検証において、削除された状態遷移を網羅していると言ってよいと考えられる。このように定義されたプロパティの網羅性を評価するために、車感応式信号機の例題において、いくつかのプロパティの網羅性を計算したところ、一部のプロパティが非常に小数の状態遷移しか網羅していないのに対し、全ての状態遷移を網羅するプロパティもあるなど、プロパティによって大きなばらつきがあることが分かった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
例題を通したプロパティ網羅性の評価が実際にできており、おおむね順調に進展していると考える。現在は、個々の状態遷移に対して網羅性の計算を行っているが、研究期間の延長申請で述べた通り、今後は、複数の状態遷移の網羅性をまとめて計算する効率的な手法について研究開発を行う予定である。
|
| Strategy for Future Research Activity |
より効率的にプロパティ網羅性の計算を行うためには、複数の状態遷移の網羅性をまとめて計算することによる効率化が必要である。今年度の研究において、論理式の充足可能性判定問題や論理回路の自動デバッグ手法を応用した効率化手法の基本的なアイデアが得られており、研究期間の延長申請で述べた通り、今後は、この効率的な手法について研究開発を行う予定である。
|
| Causes of Carryover |
計画していた国際会議発表が実現しなかったため、旅費やその他に含まれる会議参加費に計画との差額が生じることとなった。研究を発展させるために研究期間を延長したので、見込まれる発展内容を改めて国際会議や論文誌で対外発表を行うために研究費を使用する予定である。
|
