2011 Fiscal Year Annual Research Report
高性能検証系を統合した高水準モデリング言語処理系の構築
| Project/Area Number |
23300011
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
|
|---|
| Keywords | 高水準モデリング言語 / 言語処理系 / モデル検査 / ハイプリッドシステム / 並列処理 |
|---|
| Research Abstract |
高性能検証のための要素技術の確立と,システム検証の基盤となるモデリング言語の整備を目指して,本年度は研究代表者のグループが開発を推進している2つのモデリング言語を核として以下の研究開発成果を得た.
階層グラフ書換え言語LMNtalについては,従来の通常の一対一接続のリンクに加えて多点接続のためのハイパーリンクの表現・操作機能を実装し,さらにそれを非決定的実行(状態空間構築)に対応させることで検証系の表現力を大幅に向上させた.また,公開中のLMNtal並列モデル検査器slimの整備を進めて版を重ねるとともに,(i)Δ-marking手法による状態空間圧縮技法,(ii)リアルタイムシステムの並列モデル検査器への拡張,(iii)組合せ最適化の並列求解系への拡張をそれぞれ試験的に実装して評価を行った.
制約に基づくハイブリッドシステムモデリング言語HydLaについては,前年度に基本設計を行った非決定実行アルゴリズムの実装を進め,初期値の一部が区間値として与えられたシステムや記号パラメタをもつシステムのシミュレーション実行を可能にした.このようなシステムは一般に複数の定性的に異なる軌道をもつが,HydLa処理系は初期値に関する場合分けを行ってその全解を求める.この機能を利用してハイブリッドシステムの解析例の蓄積を進めた.また,これまでのHydLa実行系はMathematicaを数式処理エンジンとして用いていたが,それに加えて計算機代数システムReduceも利用できるようにした.さらに,HydLa処理系の検証系への拡張の第一歩として,HydLaプログラムからのハイブリッドオートマトンの抽出に関する基礎研究を行った.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の中心をなす高水準モデリング言語LMNtalおよびHydLaの処理系および検証系の開発と機能拡張は順調に進展し、LMNtalに続きHydLa処理系も公開するに至った。一方、当初予定の研究項目の一部(抽象化、高信頼近似計算)についてはその難度が予想以上であったため、実装を急がず基礎に立ち返り研究を続けることとした。
|
| Strategy for Future Research Activity |
これまで通り,高水準モデリング言語処理系の開発・使用経験を軸として,新たな要素技術の確立および応用分野・波及効果の拡大を図る.階層グラフ書換え言語LMNtalについては,ハイパーリンク機能の実装に伴い表現力が拡大したことを活かし,他の代表的計算体系のLMNtalへのエンコードを進めて,LMNtalモデル検査器がそれらの計算体系のためのモデル検査器としても利用できるようにする.またそれを可能にするための抽象化技術を確立する.ハイブリッド制約言語HydLaについては,高性能検証の実現手法を根本から検討すべく,まず現在の非決定的シミュレーションアルゴリズムの実際の挙動を深く分析し,その結果に基づいて高速化,並列化および抽象化の方向性を探求する.
|
