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

2003 Fiscal Year Annual Research Report

• Project/Area Number: 13680414
• Research Institution: Osaka University
• Principal Investigator: 谷口 健一 大阪大学, 大学院・情報科学研究科, 教授 (00029513)
• Co-Investigator(Kenkyū-buntansha): 山口 弘純 大阪大学, 大学院・情報科学研究科, 助手 (80314409) ; 安本 慶一 奈良先端科学技術大学院大学, 情報科学研究科, 助教授 (40273396) ; 岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632)
• Keywords: 時間オートマトン / Quality of Services / 線形計画法 / 分散マルチメディアシステム / コンポーネントベースシステム / プログラム導出 / Java

Research Abstract

本研究ではカラーペトリネットなどの高水準の形式的モデルから,Javaで記述された分散プログラムを自動導出する方法論を目指して研究してきている.時間的要素を考慮にいれるとカラーペトリネットモデルの他に時間オートマトンネットワークも記述モデルとして表現能力がある.そこで,本年度は,特に,時間オートマトンネットワークモデルによるコンポーネントベースの実時間システム設計に着目し,マルチメディアシステムの時間QoS(スループット,ジッタ,遅延)の検証について研究を行ってきた.
提案手法では,時間オートマトンネットワークとして記述されたシステムの各コンポーネントに対して,要求される時間QoSが守れるかどうかの検証をUPPAAL等を用いて行う.システム全体を同様の方法で行うと状態爆発によるメモリ空間の圧迫が問題となるので,各コンポーネントに課された提供時間QoSとコンポーネントの接続関係の2つを入力とし,それらがシステム全体への要求時間QoSを満たすかどうかの判定問題を定式化し,その問題を線形制約の非可解性問題に帰着した.この方法論の正しさを京都大学で行われた計算機科学基礎理論の研究会で発表した.
上記の方法論を元にコンポーネントベースのマルチメディアシステムの総合的な開発方法を定め,電子情報通信学会のソフトウェアサイエンス研究会で発表した.提案方法論では提供QoSに対する要求QoSの一貫性を線形制約の非可解性判定問題として高速に解いた後,各コンポーネントの時間的動作を時間オートマトンで記述し,確かめる.その後,時間制約を満たすように動作するJavaコードを自動導出する
この導出系のプロトタイプをすでに開発している.導出法については電子情報通信学会の春季総合大会で発表予定である.今後は例題などに適用し,導出されるJavaコードの改善など行う予定である.

Research Products

• [Publications] 森 一夫: "マルチメディアシステムにおけるTimeliness QoS一貫性検証と時間制御コード導出"電子情報通信学会技術報告. Vol.103, No.583. 13-18 (2004)
• [Publications] 岡野 浩三: "線形制約を用いた時間QoS一貫性の検証法"京都大学数理解析研究所考究録 計算機科学基礎理論の新展開. (To appear). 22-1-22-6 (2004)
• [Publications] 牧寺 彩: "分散環境における実時間アプリケーション動作仕様記述からのJavaコード自動導出手法の提案"電子情報通信学会春季総合大会. (To appear). (2004)