| 研究課題/領域番号 |
17K00089
|
|---|
| 研究機関 | 石川工業高等専門学校 |
|---|
研究代表者 |
松本 剛史 石川工業高等専門学校, その他部局等, 准教授 (40536140)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | 機能検証 / プロパティ検証 |
|---|
| 研究実績の概要 |
システム機能の検証では、与えられたテストパタンをシミュレーションし、期待値と比較することによって、機能の正しさを検証する場合が多いが、システムが満たすべき性質（プロパティ）を数学的に検証するプロパティ検証も行われている。プロパティ検証は、任意の入力パタン（シーケンス）について正しさを検証することができるため、シミュレーションで起こり得るテストパタンの不足による検証漏れのない検証方法である。本研究では、システムの機能検証において、テストパタンに依存するシミュレーションやテストではなく、システムがプロパティ（性質）を満たすかどうかを調べるプロパティ設計に注目し、プロパティの質の高さを表す指標を確立することを目的としている。
平成29年度は、プロパティ検証の対象となる設計例題の作成を主に行った。データフローが機能のメインであるシステムの例題として、自分自身と周辺8画素の平均を計算する平均化フィルタの回路を設計した。また、有限状態機械の状態遷移がメインとなって動作するシステムの例題として、ブレッドボード回路に配置されたジャンパ線をたどることによって、所望の配線が正しく行われているかどうかをチェックするシステムの設計を行った。加えて、それぞれの設計例題に対して、満たすべきプロパティを挙げて、実際にプロパティ検証を行った。次年度以降、これらの例題を用いて、プロパティの質を表すことのできる指標について研究を進めていく予定である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
今後の研究を進める上で必要となる設計例題の作成と、作成した例題で設計が満たすべきプロパティの列挙を行うことができたため、計画通りに進展していると言える。
|
| 今後の研究の推進方策 |
研究期間3年間の2年目となる次年度は、今年度の成果を用いて、プロパティの質を表すことのできる指標を検討し、提案・評価することが最も重要な研究内容となる。既に、指標の検討は始めており、あるプロパティによって網羅される状態遷移の割合や、プロパティの成立可否を変化させることができるような設計変更箇所の割合によって指標の策定を進める予定である。
|
| 次年度使用額が生じた理由 |
資料収集のための国際会議への参加を予定しており、その訪問先で当該研究分野で活躍する研究者と研究打合せを行う予定であったが、訪問先研究者と都合が合わなかったため、平成30年度に改めて国際会議参加と打合せのために米国訪問をすることにした。
|
