振舞仕様に基づく問題モデルの構築と検証

2003 Fiscal Year Annual Research Report

• Project/Area Number: 15300007
• Research Category: Grant-in-Aid for Scientific Research (B)
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• Co-Investigator(Kenkyū-buntansha): 中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (40345658)
• Keywords: 問題モデル / システム検証 / システム安全性 / フォーマルメソッド / 振舞仕様 / 要求仕様 / CafeOBJ

Research Abstract

平行分散アルゴリズム,認証プロトコルなどの問題領域において蓄積してきた振舞仕様の検証事例を,「適切な抽象度を持った振舞仕様の作成」ならびに「探索型と推論型の検証法の融合」の観点から分析し,以下の成果を得た.
1.適切な抽象度を持った振舞仕様の作成に関しては,どのような性質を解析・検証したいのかが仕様の抽象度の決定に大きく影響する点に着目し,以下の成果を得た.
(1)ブール代数や自然数などの,基本データ型は,いかなる抽象度の振舞仕様においても,特にその解析・検証において重要な役割を演ずることが明らかになった.これを受け,ブール代数や自然数を,その検証法(具体的にはCafeOBJの証明譜)と共に,基本ライブラリとして整理した.
(2)振舞仕様の安全性の検証が,状態遷移の回数に関する帰納法で行える事は,今までに蓄積した例題から実証されていた.これを発展させ,典型的な帰納法の検証パターンを整理体系化し,それに基づき帰納法の検証をモジュール化する技術を開発した.
2.探索型検証と推論方検証の融合に関しては,CafeOBJで書かれた振舞仕様をSMVまたはMaudeなどのモデルチェック器に変換する方法に焦点を当て.以下の成果を得た.
(1)SMVモデルチェッカに変換可能な観測遷移機械(OTS)のクラスを同定し,CafeOBJで記述されたOTS仕様からSMVへの変換プログラムを開発した.将来的には,この変換プログラムを使って,検証しようとしている命題が成立しないことを端的に示す反例の発見に役立てる計画である.
(2)cafeOBJで記述されたOTS仕様を,Maude言語のモデルチェッカに変換する変換システムの検討を行い,SMVへの変換に比べより効果的な検証補助になりうる可能性が高いとの知見を得た.

Research Products

• [Publications] Kazuhiro OGATA, Kokichi FUTATSUGI: "Flaw and Modification of the iKP Electronic Payment Protocols"Information Processing Letters. 86(2). 57-62 (2003)
• [Publications] Kazuhiro OGATA, Kokichi FUTATSUGI: "Proof Scores In the OTS/CafeOBJ Method"Springer LNCS (FMOODS 2003, Formal Methods for Open Object-Based Distributed Systems). 2884. 170-184 (2003)
• [Publications] Razvan DIACONESCU, Kokichi FUTATSUGI, Kazuhiro OGATA: "CafeOBJ : Logical Foundation and Methodologies"Computing and Informatics. 22. 257-283 (2003)
• [Publications] Kazuhiro OGATA, Kokichi FUTATSUGI: "Formal analysis of the NetBill electronic commerce protocol"International Symposium on Software Security, LNCS. (To appera). (2004)
• [Publications] 緒方和博, 二木厚吉: "書き換えによるセキュリティプロトコルの帰納的検証"コンピュータソフトウェア. 20. 54-72 (2003)
• [Publications] 清野貴博, 緒方和博, 二木厚吉: "項書換えを用いた安全性検証の組織化"コンピュータソフトウェア. 20. 32-45 (2003)