多値モデル検査法を用いたモデリング・エラーの発見

本研究は、モデル検査法を用いたシステム設計検証において、しばしば問題となる「モデル化の誤り(モデリング・エラー)」を発見する手法の研究を行うものである。モデル化に誤りがあるときは、仮にモデル検査器が「検証成功」という結果を出力をしても、システム設計が正しいことは保証されないため、これは深刻な問題である。本研究の中心となるアイディアは、「検証成功」という結果になったときに、モデルの一部を意図的に変更し、「検証失敗」となる限界モデルを探索することにより、モデリング・エラーの原因を探るというものである。今年度の研究では、昨年度の研究で構築した多値モデル検査のアルゴリズムを改良し、Quasi-Boolean Algebraに適用できるようにした。また、多値モデル検査の理論的基礎について、従来手法を一般化した定式化とそれに対するシミュレーション定理を証明し、多値モデル検査の効率化に対して理論的根拠を与えることに成功した。さらに、昨年度のアルゴリズムに対して実装上の改良をおこない、いくつかの具体例に対して、モデリング・エラーの発見を行う実験を行い、一定の条件のもとでは、本研究の手法で効率的なモデリング・エラー発見が可能であることがわかった。これらについては、後日、成果をまとめた論文を発表する予定である。関連研究として、「検証失敗からの情報の取得」という点で類似している型推論アルゴリズムにおける型エラーについての考察を行い、より良い失敗情報の取得を行うためのアルゴリズムの設計、開発を行った。

本研究は、モデル検査法を用いたシステム設計検証において、しばしば問題となる「モデル化の誤り(モデリング・エラー)」を発見する手法の研究を行うものである。モデル化に誤りがあるときは、仮にモデル検査器が「検証成功」という結果を出力をしても、システム設計が正しいことは保証されないため、これは深刻な問題である。本研究の中心となるアイディアは、「検証成功」という結果になったときに、モデルの一部を意図的に変更し、「検証失敗」となる限界モデルを探索することにより、モデリング・エラーの原因を探るというものである。今年度の研究では、昨年度の研究で構築した多値モデル検査のアルゴリズムを改良し、Quasi-Boolean Algebraに適用できるようにした。また、多値モデル検査の理論的基礎について、従来手法を一般化した定式化とそれに対するシミュレーション定理を証明し、多値モデル検査の効率化に対して理論的根拠を与えることに成功した。さらに、昨年度のアルゴリズムに対して実装上の改良をおこない、いくつかの具体例に対して、モデリング・エラーの発見を行う実験を行い、一定の条件のもとでは、本研究の手法で効率的なモデリング・エラー発見が可能であることがわかった。これらについては、後日、成果をまとめた論文を発表する予定である。関連研究として、「検証失敗からの情報の取得」という点で類似している型推論アルゴリズムにおける型エラーについての考察を行い、より良い失敗情報の取得を行うためのアルゴリズムの設計、開発を行った。