| 研究課題/領域番号 |
17K17725
|
|---|
| 研究機関 | 電気通信大学 |
|---|
研究代表者 |
戸田 貴久 電気通信大学, 大学院情報理工学研究科, 助教 (50451159)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | モデル検査 / アルゴリズム / SAT / 制約 |
|---|
| 研究実績の概要 |
AllSATソルバーの高速化手法についてまとめた学術論文「Exploiting Functional Dependencies of Variables in All-Solutions SAT Solvers」が論文誌に採録された。
現在、AllSATの応用研究として有界モデル検査の拡張を進めている。有界モデル検査は（ハードウェアやソフトウェアなど）システムの誤りを発見する手法である。実用的なモデル検査器（例えば、NuSMV2）の内部処理では、SATソルバーが呼び出され、誤りの探索を行う。もし誤りが発見されたときには、モデル検査器は、システムの内部状態がどのように遷移したときに違反状態に陥るのかを表す実行シーケンスを返す。ここまではモデル検査器が自動で処理してくれるが、この実行シーケンスから誤りを引き起こした根本原因を特定する部分は通常人手が必要である。
実行シーケンスは長く複雑なので人間が理解するのは困難であり、過去の研究でその負担を軽減する仕組みが提案されてきたが、まだ十分には手が付けられていないのが現状である。そこで、本研究では、AllSATソルバーをモデル検査器のコア技術として用いて、多数の実行シーケンスを生成することができるように拡張した。さらに、特定の変数の値を固定して実行シーケンスを生成する「制約による絞り込み機能」など、人手による解析を補助する機能を開発した。現在、予定している機能実装は終了し、論文の執筆にとりかかっている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
本研究の基本アイディアを当該分野の標準的なソフトウェアを拡張する形で実装した。
このソフトウェアは３０万行程からなる巨大なものであり、その根本の部分から手を加える必要があったので、大量のコードを理解して、追加機能のコードを追加するのに想定以上に時間がかかってしまった。しかし、予定していた機能の実装はほぼ終了して、現在は論文執筆に取り掛かっている。
|
| 今後の研究の推進方策 |
まずは、これまでの研究成果を論文にまとめあげることが第一である。これで計算基盤がひとまず完成したことになる。今後はこの枠組みをネットワーク検証における問題解決につなげていくことを計画している。
|
| 次年度使用額が生じた理由 |
計算機の故障や不具合などなかったので、当該年度に新しい計算機を購入していなかったが、次年度は購入を検討している。
|
