システムレベル記述の時間制約を考慮した抽象化およびモデル検査
| Project/Area Number |
16700062
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Computer system/Network
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
中田 明夫 大阪大学, 大学院・情報科学研究科, 助教授 (60295839)
|
|---|
| Project Period (FY) |
2004 – 2005
|
| Project Status |
Completed (Fiscal Year 2005)
|
| Budget Amount *help |
¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2005: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2004: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | 実時間システム / システムレベル記述 / 組込みソフトウェア / 時間オートマトン / パラメトリックモデル検査 / 抽象化 / 時間トレース等価性 / 時間失敗等価性 / システムレベル記述言語 / 時間制約 / 時間弱トレース等価性 / 時間試験等価性 |
|---|
| Research Abstract |
本研究では、実時間制約を持つハードウェアの動作を記述したプログラム(システムレベル記述)や組込みソフトウェアプログラムが、望ましい性質(要求仕様)を満たすための、システムの時間パラメタ群に対する条件式(パラメタ条件式)を自動導出する手法(パラメトリックモデル検査)の研究を行っている。
特に本研究では、遷移条件にパラメタを記述可能な時間オートマトンの部分クラスであり、システムの各単位動作に対して、実行時間の上限と下限をパラメタを用いた線形式で指定可能なオートマトン、パラメトリック時間インターバルオートマトン(PTIA)を提案し、着目するPTIAモデルの性質を保存したまま状態数を削減(抽象化)し、従来よりも時間計算量を小さいパラメトリックモデル検査手法を開発することを目指している。
本年度は、要求仕様で着目している単位動作とその実行時間の組の系列(時間トレース)の集合が保存した抽象化操作(前年度において考案済み)を適用後のPTIAモデルが、要求仕様を満足するためのパラメタ条件式を導出するパラメトリックモデル検査アルゴリズムを考案した。理論的な成果に関する論文は、学術論文誌IEICE Trans.on Fundamentalsに採録され、本年度11月に掲載された。
また、考案したアルゴリズムをツールに実装し、ライントレースカー制御プログラムの設計に応用できることを確認した。応用結果に関しては、来年度に国内研究会で発表を予定している。
一方、提案手法を実時間並行システムに適用する場合、複数の並行コンポーネントの積状態を考える必要があり、一般に考慮すべき状態数が膨大となりパラメトリックモデル検査は困難となる。本年度はその問題の解決のため、並列コンポーネント間の時間的な通信動作に関する性質(時間失敗等価性)を保存して、各並行コンポーネントを独立に抽象化する手法を考案した。この理論的な成果に関する論文は、学術論文誌Int.Journal of Foundations of Computer Scienceへの採録が本年度中に決定しており、掲載時期は未定であるが来年度以降に掲載予定である。
|
Report
(2 results)
Research Products
(4 results)
