2008 Fiscal Year Annual Research Report
高水準ハイブリッド制約モデリング言語とその高信頼実装
| Project/Area Number |
20300013
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 Waseda University, 理工学術院, 教授 (10257206)
|
|---|
| Keywords | ハイブリッドシステム / モデリング言語 / 高信頼計算 / 制約 / システム検証 |
|---|
| Research Abstract |
連続変化と離散変化の両方を有するハイブリッドシステムのシミュレーション・検証・設計のための高水準モデリング言語の確立に向けて,本年度は以下の項目について研究開発を行った.
1.ハイブリッドオートマトンと比べて格段に高い記述能力を持つ高水準モデリング言語が備えるべき要件を詳細に検討し,それに基づいてハイブリッド制約モデリング言語HydLaの基本設計を行った. HydLaは以下の点を特徴とする.
(a)微分方程式をはじめとする制約式を用いて「時刻の関数」を定義してその初期値問題を解くことを,言語および計算の基本としている.
(b)数学と論理学の周知の記法を最大限利用した宣言型記述を可能にしている.
(c)制約概念を基本に据えることで,シミュレーションや検証における不確定情報を的確に扱うことができる.
(d)制約の階層化機能を備えることで,システムの挙動に関する制約条件を過不足なくかつ簡潔に与えることができる.
(e)複雑な系の記述に必要な部品化やパラメタ化の機能を備えている.
本年度は上記の特徴をもつHydLaの構文および宜言的意味論を設計し,記述実験を通じて言語の記述能力および意味論の妥当性を確認した.
2. HydLaの仕様の妥当性確認および実装方式の基礎検討のために, HydLaの基本機能の試験実装を行った.実装はMathematicaで行い,制限されたクラスのHydLaモデルに対して,制約階層の求解が記号的に実装できることを確かめた.
3.観測誤差や計算誤差などに起因する不確定情報の存在下でのシミュレーションや検証の正当性を確保するために,離散変化の発生時刻やそのときの状態を区間求解するための体系とアルゴリズムを開発した.またその実装に利用する既存の求解系(VNODE-LPおよびElisa)の機能や構造の解析および改良を行った.
|
