2009 Fiscal Year Annual Research Report
高水準ハイブリッド制約モデリング言語とその高信頼実装
| Project/Area Number |
20300013
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 Waseda University, 理工学術院, 教授 (10257206)
|
|---|
| Keywords | ハイブリッドシステム / モデリング言語 / 高信頼計算 / 制約 / システム検証 |
|---|
| Research Abstract |
連続変化と離散変化の両方を有するハイブリッドシステムのシミュレーション・検証・設計のための高水準モデリング言語とその実装技術の確立に向けて,以下の研究開発を行った.
1.前年度に基本設計を行ったハイブリッド制約モデリング言語HydLaについて,意味論と記述能力の検討を引き続き行った。HydLaは,数学および論理学の記法を利用した宣言的記述,制約概念を活用した不確定情報の扱い,制約の階層化機能などを特徴とする.制約の階層化は簡潔なモデリングに不可欠な機能であるが,制約発行と無矛盾極大な制約集合の求解タイミングとの関係をはじめとする言語設計上の要検討点がいくつか見つかり,制約階層の意味論の再検討を詳細に行った.
2.HydLaの主要機能を備えた統合試作処理系を構築した.構文解析,制約階層ソルバ,前向きシミュレータをそれぞれ再利用可能な形でモジュール化し,仮想制約ソルバをインタフェースとして数式処理による制約ソルバと区間演算による制約ソルバの双方が利用できるようにした.
3.観測や計算の誤差に起因する不確定情報の存在下でのシミュレーションや検証の正当性を確保するために,離散変化の発生時刻やそのときの状態を区間求解する体系とアルゴリズムの改良拡張を行った.離散変化条件をみたす時点と状態を求める問題をHCS(ハイブリッド制約システム)として定式化し,区間解析に基づく実装を整備するとともに,区間解中に理論解が唯一含まれることを保証する機能を実装した.
4.HydLaの検証機能の構築に向けて,HCSの求解機能を利用してハイブリッドオートマトンの到達性検証を行う手法を開発した.到達性問題を一階述語論理式の充足可能性問題に変換し,3.の実装とSATソルバとを接続したSMTソルバによって求解する有界モデル検査法を開発し,既存のソルバで解けなかった問題の解を存在保証付きで求めることに成功した.
|
