分散オブジェクト環境におけるコンポネント仕様の検証に関する研究

1999 Fiscal Year Annual Research Report

• Project/Area Number: 11480067
• 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): 森 彰 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30311682)
• Keywords: ソフトウェア・コンポネント / 形式仕様 / 仕様リポジトリ / シグネチャ・マッチング / 振舞詳細化 / モデル検査

Research Abstract

今年度の研究の目的は,1.ネットワーク上でソフトウェア・コンポネントのサービス仕様を形式的に記述・登録するための仕様リポジトリ管理法の確立と,2.コンポネントが求められた機能を提供するかどうかの検証,及びシステム統合における安全性の検査を自動的に行うための推論系の開発であった。仕様リポジトリ管理については,XMLを用いた代数仕様のための文書スキーマを定義することで,コンポネント仕様の可用性が高まることが確認できた。CafeOBJによる仕様や実装オブジェクトの識別子を含ませておくことで,コンポネントの検索・検証や遠隔実行などが特定の処理方式に依存せずに実現できるものと思われる。仕様検証については,1.コンポネントのインターフェースを対象をしたシグネチャ・マッチング,2.得られたシグネチャ射に対する振舞詳細化検証,3.コンポネント結合におけるモデル検査,の三つの部分に分けて設計・開発を行った。シグネチャ・マッチングについては,隠蔽ソートのみ置き換えを許し,可視ソートについてはその名前が同一かだけでマッチングを行うことにより,実用性を損なうことなく高速にシグネチャ射を生成することが可能となった。詳細化検証では,振舞等式の詳細化検証に必要な双対帰納法を状態の対に対する安全性モデル検査とみなし,モデル検査エンジンを用いて処理する方法を提案した。モデル検査については,振舞仕様を(無限)状態遷移機械の定義とみなし,システムの状態を隠蔽ソート上の述語として表現することで,不動点の繰り返し計算として自動化できることを示した。検査するシステムの時相的性質は,状態遷移の次状態,前状態,不動点のそれぞれの演算子によって記述され,これに対応する遷移述語間の包含関係が,等号を含む一階述語論理を対象とした導出法に基づく定理自動証明によって判定される。CafeOBJ処理系の上に試作システムを作成しその有効性を確認した。

Research Products

• [Publications] Akira Mori: "Verifying Behavioural Specifications in CafeOBJ Environment"Lecture Notes in Computer Science. 1709. 1625-1643 (1999)
• [Publications] Razvan Diaconescu: "Component-based Algebraic Specification and Verification in CafeOBJ"Lecture Notes in Computer Science. 1709. 1644-1663 (1999)
• [Publications] Kazuhiro Ogata: "Formal Verification of the MCS List-Based Queuing Lock"Lecture Notes in Computer Science. 1742. 281-293 (1999)