2004 Fiscal Year Annual Research Report
オブジェクト指向型ソフトウェアの仕様記述と検証及び実行プログラム導出
| Project/Area Number |
13680414
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
谷口 健一 大阪大学, 大学院・情報科学研究科, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632)
安本 慶一 奈良先端科学技術大学院大学, 情報科学研究科, 助教授 (40273396)
山口 弘純 大阪大学, 大学院・情報科学研究科, 助手 (80314409)
|
|---|
| Keywords | オブジェクト指向 / 分散実時間システム / ステートチャート / UML / OCL / 時間オートマトン / プログラム導出 |
|---|
| Research Abstract |
本研究はオブジェクト指向ソフトウェアの高品質設計方法,高信頼性ソフトウェア導出のための仕様記述方法,および,効率のよい実行プログラム導出方法の確立をその目標にしている.昨年度からは,時間制約を満たすプログラムの設計方法を提案し,その有用性を調べている.今年度は昨年度の研究を踏まえ,上位記述にUML/OCLを用いて設計記述を行い,コンポーネントベースの設計と検証作業を二段階に分けることにより,システム全体に課せられたQoS制約が満たされることを保障し,さらに制御コードを導出する方法を考案した.上位設計においては,各コンポーネントの接続関係と各コンポーネントの提供時間QoS制約(スループット,ジッター,遅延),及び,システム全体の要求QoS制約をUMLクラス図とUMLの拡張用言語として提案されているOCL (Object Constraint Language)記述で与える.システムの要求QoSがこれらの提供QoSとコンポーネント接続関係のもとで満たされるかを線形計画問題に帰着して判定する.さらに各コンポーネントの振る舞いを時間制約を持つ拡張ステートチャート記述により設計記述する.そして各コンポーネントごとに提供QoS制約を満たすことの検証を2ステップで行う.先ず,拡張ステートチャートから時間オートマトンネットワークへ変換する.そして,昨年度提案した方法により時間QoSを満たすことの検証を行う拡張ステートチャートから時間オートマトンネットワークへの変換においいては,ステートチャートの階層構造を活かしながら,フラットな時間オートマトンに変換している.また,試作した変換系を用いて例題に適用し,段階的設計を行うことにより,検証時に状態爆発を起こすことなく,提案したQoS検証方法が適用可能であること,及び,時間制御コードが生成できることを確認し,研究会で発表した.
|
