システムレベル記述の時間制約を考慮した抽象化およびモデル検査

本研究では、実時間制約を持つハードウェアの動作を記述したプログラム(システムレベル記述)や組込みソフトウェアプログラムが、望ましい性質(要求仕様)を満たすための、システムの時間パラメタ群に対する条件式(パラメタ条件式)を自動導出する手法(パラメトリックモデル検査)の研究を行っている。特に本研究では、遷移条件にパラメタを記述可能な時間オートマトンの部分クラスであり、システムの各単位動作に対して、実行時間の上限と下限をパラメタを用いた線形式で指定可能なオートマトン、パラメトリック時間インターバルオートマトン(PTIA)を提案し、着目するPTIAモデルの性質を保存したまま状態数を削減(抽象化)し、従来よりも時間計算量を小さいパラメトリックモデル検査手法を開発することを目指している。本年度は、要求仕様で着目している単位動作とその実行時間の組の系列(時間トレース)の集合が保存した抽象化操作(前年度において考案済み)を適用後のPTIAモデルが、要求仕様を満足するためのパラメタ条件式を導出するパラメトリックモデル検査アルゴリズムを考案した。理論的な成果に関する論文は、学術論文誌IEICE Trans.on Fundamentalsに採録され、本年度11月に掲載された。また、考案したアルゴリズムをツールに実装し、ライントレースカー制御プログラムの設計に応用できることを確認した。応用結果に関しては、来年度に国内研究会で発表を予定している。一方、提案手法を実時間並行システムに適用する場合、複数の並行コンポーネントの積状態を考える必要があり、一般に考慮すべき状態数が膨大となりパラメトリックモデル検査は困難となる。本年度はその問題の解決のため、並列コンポーネント間の時間的な通信動作に関する性質(時間失敗等価性)を保存して、各並行コンポーネントを独立に抽象化する手法を考案した。この理論的な成果に関する論文は、学術論文誌Int.Journal of Foundations of Computer Scienceへの採録が本年度中に決定しており、掲載時期は未定であるが来年度以降に掲載予定である。

本研究では、実時間制約を持つハードウェアの動作を記述したプログラム(システムレベル記述)や組込みソフトウェアプログラムが、望ましい性質(要求仕様)を満たすための、システムの時間パラメタ群に対する条件式(パラメタ条件式)を自動導出する手法(パラメトリックモデル検査)の研究を行っている。特に本研究では、遷移条件にパラメタを記述可能な時間オートマトンの部分クラスであり、システムの各単位動作に対して、実行時間の上限と下限をパラメタを用いた線形式で指定可能なオートマトン、パラメトリック時間インターバルオートマトン(PTIA)を提案し、着目するPTIAモデルの性質を保存したまま状態数を削減(抽象化)し、従来よりも時間計算量を小さいパラメトリックモデル検査手法を開発することを目指している。本年度は、要求仕様で着目している単位動作とその実行時間の組の系列(時間トレース)の集合が保存した抽象化操作(前年度において考案済み)を適用後のPTIAモデルが、要求仕様を満足するためのパラメタ条件式を導出するパラメトリックモデル検査アルゴリズムを考案した。理論的な成果に関する論文は、学術論文誌IEICE Trans.on Fundamentalsに採録され、本年度11月に掲載された。また、考案したアルゴリズムをツールに実装し、ライントレースカー制御プログラムの設計に応用できることを確認した。応用結果に関しては、来年度に国内研究会で発表を予定している。一方、提案手法を実時間並行システムに適用する場合、複数の並行コンポーネントの積状態を考える必要があり、一般に考慮すべき状態数が膨大となりパラメトリックモデル検査は困難となる。本年度はその問題の解決のため、並列コンポーネント間の時間的な通信動作に関する性質(時間失敗等価性)を保存して、各並行コンポーネントを独立に抽象化する手法を考案した。この理論的な成果に関する論文は、学術論文誌Int.Journal of Foundations of Computer Scienceへの採録が本年度中に決定しており、掲載時期は未定であるが来年度以降に掲載予定である。