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