2012 Fiscal Year Annual Research Report
高性能検証系を統合した高水準モデリング言語処理系の構築
| Project/Area Number |
23300011
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田辺 良則 国立情報学研究所, 大学共同利用機関等の部局等, 教授 (60443199)
|
|---|
| Project Period (FY) |
2011-04-01 – 2014-03-31
|
| Keywords | 高水準モデリング言語 / 言語処理系 / モデル検査 / ハイブリッドシステム / 並列処理 |
|---|
| Research Abstract |
実行系と検証系を統合した高水準モデリング言語の処理系の構築に関して，以下の二つの処理系を軸に研究開発を実施した．
1. ハイブリッドシステムモデリング言語HydLaの記号実行シミュレータHyroseの開発を進めた．Hyroseは，ハイブリッドシステムを制約によって記述する宣言型言語HydLaの実装であり，(a) 数式処理に基づく厳密な求解，(b) パラメータをもつシステムにおける自動場合分けに基づく探索，(c) 有界モデル検査機能などを大きな特徴とする．本年度は，これまでのHydLaの非決定実行アルゴリズムを実装の立場から詳細化しつつ再検討し，新たな処理系を公開した．また，Hyroseの実行において最も時間のかかっている制約の無矛盾性解析を静的解析によって最適化する方法を考案して試験実装と評価を行った．さらに，HydLaプログラムをハイブリッドオートマトンに変換する手法，数式処理で求解できないシステムの区間演算による解法，および自動場合分けに基づく探索の並列実行の基礎検討を行った．
2. 階層グラフ書換えに基づくモデリング言語LMNtalとその処理系を引き続き発展させた．言語仕様については，前年度に導入したハイパーリンクを用いたBigraphical Reactive Systems (BRS) のエンコードに必要な基本操作を設計実装することで，LMNtalの拡張であるHyperLMNtalの仕様を確立させた．また，LMNtal並列モデル検査器における状態空間構築の実行時間削減のために，on the fly性に優れるが並列効果の高くないNested DFSアルゴリズムと，その逆の特性をもつMAPアルゴリズムを組み合わせる技法を開発してその有効性を評価した．さらに，LMNtalモデル検査の状態管理において大きな役割を演ずるグラフ構造の効率的な一意エンコード手法の検討を進めた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
高水準モデリング言語の発展という観点から研究は順調に進展している．言語仕様の観点からは，HydLaは処理系開発の深化および例題の蓄積によって妥当性確認が進み，LMNtalはハイパーリンクを備えたHyperLMNtalへと発展した．それぞれの処理系の機能強化やデバッグも順調に進み，HydLaにおいてはパラメータつきシステムの自動場合分けに基づくシミュレーションや有界モデル検査，LMNtalにおいては状態空間構築の効率化やHyperLMNtalのモデル検査への対応をはじめとする多様な研究が進展した．HydLaとハイブリッドオートマトンとの関連付けをはじめ，検証系の発展のための基盤技術の整備も進んだ．一方，HydLaにおいては区間計算の導入が次の重要課題として浮上し，LMNtalにおいては状態空間爆発への対処方法の開発が課題となってきた．
|
| Strategy for Future Research Activity |
新要素技術の設計，実装，現存処理系への統合については，基本的にこれまでの体制と方法でさらに進展すると期待される．区間計算に基づくHydLaプログラムの高信頼近似計算技術については，区間計算の専門家の協力と助言をもらいつつ推進する予定である．
|
