• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2020 年度 研究成果報告書

形式的プロパティ検証の完全性指標の定義とその応用

研究課題

  • PDF
研究課題/領域番号 17K00089
研究種目

基盤研究(C)

配分区分基金
応募区分一般
研究分野 計算機システム
研究機関石川工業高等専門学校

研究代表者

松本 剛史  石川工業高等専門学校, 電子情報工学科, 准教授 (40536140)

研究期間 (年度) 2017-04-01 – 2021-03-31
キーワードプロパティ検証 / 回路検証
研究成果の概要

システム検証の一種であるプロパティ検証と呼ばれる、システムが仕様(プロパティ)を満たすかどうかを確かめる検証方法を対象として、検証がどの程度網羅的に行われているかを示す指標となる検証カバレッジを提案し、その評価を行った。検証においては、システム全体のうち、どの程度の部分が検証できているかを知ることが重要であるが、プロパティ検証ではそのような指標が存在しないため、指標の確立は重要である。本研究では、システムの状態遷移が変化することによって、検証結果がその影響によって変化した場合、検証したプロパティによってその状態遷移が網羅されていると考え、これに基づく検証カバレッジを提案し、評価結果を示した。

自由記述の分野

VLSI設計支援

研究成果の学術的意義や社会的意義

現在、多くの電子情報機器は大規模なシステムであり、その正しさの検証を効率的に行うことが重要になっている。検証においては、検証対象システムの一部だけを検証しても誤り(バグ)を全て見つけることができないため、どの程度網羅的に検証が行われているかを把握することが必要である。本研究では、システム検証の一種であるプロパティ検証を対象として、検証がどの程度網羅的に行われているかを示す指標を提案し、いくつかの例題において評価を行った。これにより、どれ程のプロパティを検証すれば十分であるかを知る指標とすることができ、さらには、検証結果に対する信頼性・説明可能性が高まることが期待できる。

URL: 

公開日: 2022-01-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi