オブジェクト指向型ソフトウェアの仕様記述と検証及び実行プログラム導出

2002 Fiscal Year Annual Research Report

• Project/Area Number: 13680414
• Research Institution: Osaka University
• Principal Investigator: 谷口 健一 大阪大学, 大学院・情報科学研究科, 教授 (00029513)
• Co-Investigator(Kenkyū-buntansha): 安本 慶一 奈良先端科学技術大学院大学, 情報科学研究科, 助教授 (40273396) ; 山口 弘純 大阪大学, 大学院・情報科学研究科, 助手 (80314409) ; 岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632)
• Keywords: 分散オブジェクト / プログラム自動導出 / Java / カラーペトリネット

Research Abstract

本研究では,分散オブジェクトプログラムの仕様を抽象度の高い記述モデルで記述し,その動的性質や機能の正しさを検証した上でプログラムコードを自動導出することで,設計・実装時の誤りを削減し,信頼性の高い分散オブジェクトプログラムを少ない設計コストで実現するための方法論に関する研究を行っている.今年度は,カラーペトリネット仕様からのJavaプログラムコード自動導出アルゴリズムについて検討し,それに基づく自動導出系のプロトタイプ実装を行った.自動導出アルゴリズムでは,近年の携帯端末クライアントの普及を考慮し,クライアントメモリ制約下においても与えられた仕様を満たしてプログラムが実行されていくようにした.このため,導出アルゴリズムは,サーバ及びクライアントへの適切な機能分担及びプログラムデータの配置を行い,クライアント側でインタプリタ方式で実行するコードを導出する.なお,実行時にはサーバ・クライアント間の通信量がなるべく少なくなるように工夫している.複数人によるコラボレーションフロー管理の例題記述を行い,作成した自動導出系を用いて対応するJavaコードを導出し,Java携帯端末を含む分散環境上で実行実行を行った.その結果,そのようなクライアントを含む環境においても導出したコードは問題なく実行できることが確認できた.これらの中間成果は電子情報通信学会の研究会等で発表した.今後はカラーペトリネットで記述された仕様の性質検証について,オブジェクト指向プログラムに適した方法論の検討を行う予定である.

Research Products

• [Publications] 坂上 弘祐 他: "ペトリネットで記述された簡易ブラウザ型の組込みJavaプログラム動作仕様に対する実行方式の提案"電子情報通信倍学会技術研究報告(信学技報). 102・246. 1-6 (2002)
• [Publications] 坂上 弘祐 他: "端末間通信可能なJ2MEアプリケーションプログラムのペトリネット動作仕様からの自動導出"情報処理学会第65回全国大会予稿集. (発表予定). (2003)