| 研究課題/領域番号 |
17K17725
|
|---|
| 研究機関 | 電気通信大学 |
|---|
研究代表者 |
戸田 貴久 電気通信大学, 大学院情報理工学研究科, 准教授 (50451159)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | モデル検査 / アルゴリズム / SAT / 制約 |
|---|
| 研究実績の概要 |
まずは、本研究の背景（SATに基づく有界モデル検査）とその問題点について述べる。モデル検査はハードウェアやソフトウェアなど情報システムの検証を行うための技術である。もしシステムの設計に何らかの不具合があった場合、モデル検査をおこなうことにより、不具合に至るシステムの状態遷移列（反例）を自動的に計算できる。これは強力な技術であるが、反例の計算と不具合の特定の間には隔たりがあり、不具合特定のためには反例をもとに人手の検査が必要となる。これは属人的な作業であり、多くの変数値やその時間的変化を観察することが求められ煩雑で気が滅入る作業である。
本研究では、不具合の特定作業を支援することを目的にして、モデル検査に対して以下の機能を追加し、既存の枠組みを拡張する：これまでのように１つの反例だけを計算するのでなく、複数の反例を生成する；生成された反例は莫大な数になりうるので、結果をデータ構造BDDを用いてコンパクトに表現する（これを反例データベースと呼ぶ）；反例データベースを解析することにより、”抽象化された情報”を獲得する。
これまでの研究で、この新しい枠組みを立案し、既存のモデル検査ソフトウェアNuSMV2を土台に実装した。解析操作としては、さまざまな操作を後から容易に拡張できるように、解析操作を他のコンポーネントから独立になるように設計した。
実現した解析操作の例としては、特定の整数変数xに着目して、xの値が区間をなす反例集合（のうち区間の長さが最大のもの）を求めることが挙げられる。この操作により、（他の変数の値を固定した下で）xの値がある区間[a,b]に属するならばすべて反例になる、ということがわかる。特にxの値がaあるいはbとなる反例に関しては、不具合になるか否かの境目をなすことから、（他のxの値に関する単一の反例を提示する場合に比べ）不具合特定により近い有用な情報になりうる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
これまでの研究活動により、当初構想した研究計画の核となる基本部分を実現することができた。具体的には、既存のモデル検査の枠組みに対する拡張機能の追加と、それらを連携させて抽象的な解析を実現させる枠組みの開発である。
これをモデル検査ソフトウェアNuSMV2を土台にして実装した。NuSMV2は巨大なソフトウェアライブラリであり、今回の拡張作業はソフトウェアコードの深くまで手を加える必要があったため、（既存のコードを理解することも含め）開発作業は難航したが、何とか計画したとおりの機能拡張を実現することができ、動作の確認もできた。また、モデル検査の過去の研究を丹念に調査し、本研究と関連する研究を整理し、本研究の位置づけを明らかにした。以上の結果をまとめ、国内の研究会で報告した。
|
| 今後の研究の推進方策 |
これまでの研究の完成度を上げるために、十分な計算機実験を行いたい。また提案手法の応用として、具体的にどのような場合に本手法を活用できて、その結果、どのような効果が得られるのかについて具体的な例を検討する。これらの結果を論文にまとめ、国際会議や学術雑誌に投稿する。また、開発したソフトウェアを誰でも利用できるように一般に公開することの可能性について検討する（既存のソフトウェアを土台にしているので、著作権の問題が生じない範囲で公開できるか否か）。公開する際には、説明の文書やホームページの作成、そしてコードの整理などを行う。
|
| 次年度使用額が生じた理由 |
厳密に０ではないが、残額は少なく、ほぼ予定通りに使用している。
次年度の旅費あるいは物品費の一部として使用する予定である。
|
