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

2000 Fiscal Year Annual Research Report

• Project/Area Number: 11480067
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• Co-Investigator(Kenkyū-buntansha): 森 彰 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30311682)
• Keywords: 分散オブジェクト / ソフトウェア・コンポネント / 形式手法 / 詳細化検証 / 安全性検査

Research Abstract

今年度の研究の目的は,前年度に設計・開発を行った仕様リポジトリ管理システムと検証推論システムを統合することにより,1)選ばれたソフトウェア・コンポネントが求められた機能を提供するかどうか,また,2)システム統合における安全性が満たされるかどうか,をグラフィカル・ユーザーインターフェース(GUI)を通して,半自動的に検証できるようなシステムのプロトタイプを作成することであった.プロトタイプの作成においては,1)XMLによるリポジトリ表現,2)標準プロトコル(HTTP,TCP,CGI)によるユーザーおよび検証推論エンジンとの連動,3)ブラウザーで動作するWebアプリケーションとしての実装,により,各構成要素をネットワーク上の異なるサイトに配置できるようになったため,システムの修正や実験などが容易に行えるようになった.このことは今後の研究開発に役立つものと思われる.そして,このプロトタイプを用いて,簡単なコンテナー・クラスの仕様を検索する実験を行った.コンテナーはスタック,セル,バソファなど15種類を遠隔リポジトリに登録し,ユーザーがブラウザー上で要求コンポネント仕様を与え,詳細化をパスしたコンポネントについてCafeOBJサーバー経由でモデル検査を行った.コンポネント仕様やモデル検査された性質はごく簡単なものであったものの,処理は完全に自動化されており,ネットワーク上でのコンポネント仕様検証システムとしての本研究での基本設計が妥当であったことを確認することができた.最後に,より実用に近い実験を行うための準備として,実際に流通しているEJB(Enterprise JavaBeans)コンポネントのJavaDoc形式によるAPI定義をCafeOBJによるインターフェース仕様に変換するツールを作成した.これによりWeb上で公開されたJavaクラス定義を自動的に仕様化することが可能になり,将来の検証システム運用の助けになるものと思われる.

Research Products

• [Publications] 飯田周作: "振舞仕様に基づく仕様コンポーネント化技術の発展可能ソフトウェアへの応用"コンピュータソフトウェア. 18(0). 30-45 (2001)
• [Publications] Razvan Diaconescu: "CafeOBJ Jewels"CAFE : An Industiral-Strength Algebraic Formal Method. 33-60 (2000)
• [Publications] Joseph Goguen: "An Overview of Tatami Project"CAFE : An Industiral-Strength Algebraic Formal Method. 61-78 (2000)
• [Publications] Joseh Goguen: "Introducing OBJ"Software Engineering with OBJ. 3-167 (2000)
• [Publications] Masaki Nakamura: "The evaluation strategy for head normal form with and without on-demand flags"Proc of The 3rd International Workshop on Rewriting Logic and its Applications (WRLA2000). (2000)
• [Publications] Ataru Nakagawa: "Constructing a Graphics System with OBJ2 : A Practical Guide"Software Engineering with OBJ. 193-248 (2000)
• [Publications] Kazuhito Ohmaki: "A LOTOS Simulator in OBJ"Software Engineering with OBJ. 363-398 (2000)
• [Publications] Takahiro Seino: "Specification and verification of a single-track railroad signaling in CafeOBJ"Proc of International Technical Conference on Circuits/Systems,Computers and Communications (ITC-CSCC 2000). 268-273 (2000)