| 研究概要 |
連続変化と離散変化を有するハイブリッドシステムの高信頼シミュレーション・検証・設計のための高水準モデリング言語とその実装技術の確立に向けて,以下の研究開発を行った.
1.前年度までに設計を行ったハイブリッド制約モデリング言語HydLaの基本機能を抽出した基本HydLaを定義し,その宣言的意味論を確立させた.基本HydLaは,HydLaの特徴である制約階層を,制約モジュール集合間の半順序構造の形で明示的に与えたものである.これによって,軌道の動的生成を可能にする局所変数生成機能が導入可能になり,あるイベントを検知してから新たな挙動を開始するまでの遅延の表現が可能になった.
2.HydLaは制約概念に基づく定式化を特徴としており,変数値が区間制約として与えられる系やパラメタを有する系の表現が可能であるが,そのような系に対応するシミュレーションアルゴリズムが求められていた.本年度はこれを定式化して,多数の例題の検討を通じてその妥当性を確認した.非決定アルゴリズムとして定式化することで到達可能性の探索を可能にした点や,開区間と閉区間の違いを注意深く扱う点などを特徴とする.
3.前年度開発したHydLa処理系に対して,上記アルゴリズムの機能を順次追加実装した.これによって不確定性をもつ多くの系のシミュレーションが可能になった.また制約処理エンジンとしてのREDUCEの活用可能性の検討と試作を行った.
4.HydLaの現処理系は数式処理に基づく高信頼実行に特化しているが,区間制約技術との今後の統合を目指して,非線形ハイブリッドシステムの到達可能性検証を行う有界モデル検査ツールhydlogicを試作した.hydlogicは常微分方程式の区間求解系をエンジンとするSMTソルバを要素技術としており,区間ニュートン法によって,求まった解がちょうど一つの真解を包囲することを保証している.
|
