2014 Fiscal Year Annual Research Report
検証系を備えた高水準モデリング言語処理系の実装技術の深化
| Project/Area Number |
26280024
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
石井 大輔 東京工業大学, 情報理工学(系)研究科, 助教 (00454025)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 高水準モデリング言語 / 言語処理系 / モデル検査 / ハイブリッドシステム / 並列処理 |
|---|
| Outline of Annual Research Achievements |
ハイブリッドシステムモデリング言語HydLaの実行系HyLaGIおよびグラフ書換え言語LMNtalのモデル検査系SLIMの発展に向けて，以下の研究を推進した．
1. 属性つきハイパーリンク機能をもつ拡張言語HyperLMNtalの実用性評価のために，高階単一化機能をもつ高階論理型言語のHyperLMNtalへのエンコーディングを行い動作確認を行った．
2. HyLaGIは記号実行に基づく無誤差計算やパラメタを含むモデルのシミュレーションを特徴としているが，離散変化フェーズと連続変化フェーズの繰返し実行において直前のフェーズの情報が利用されておらず，不要な再計算を繰り返すという問題があった．そこで，離散変化の原因，フェーズ間の制約の差分，変数の連続性の3種類の情報を活用したインクリメンタルな実行方式を考案し，制約の依存関係グラフを用いた実装を行った．プログラム中の制約数の増大に対するスケーラビリティがおよそ1次分向上したことを実験により確認した．
3. グラフ書換え系は情報構造の表現力が高い半面，時間空間の両面で効率のよい状態空間圧縮が難しい．そこで状態空間圧縮手法Tree Compressionのグラフデータ構造への適用を試みた．Tree Compressionは各状態ベクトルの共通部分を木構造で管理することで状態空間を圧縮する．これをSLIMに導入する方法を検討し，実装・評価を行った．その結果，メモリ使用量を最高約11%に圧縮することに成功し，空間効率向上に伴い実行時間も短縮された．従来実行不能であった20億状態規模の例題の実行が可能となった．
4. 区間計算を拡張した平行体計算に基づく非線形ハイブリッドシステムのシミュレーション手法を利用し，有界線形時相論理式で記述した非線形ハイブリッドオートマトンの性質を精度保証つきで検証する手法を開発した．さらにこの手法を用いて統計的モデル検査を行う実験を行い，平行体計算に基づく手法の有用性を示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の研究実施計画の中で，属性つきハイパーリンク操作のための言語機能については，高階単一化という複雑な操作を含む計算体系のエンコードを通じてその有効性と処理系の動作確認ができ，今後の研究展開の方針を得ることができた．グラフの高速パターンマッチングについては，スペースの都合で研究実績概要には記載していないが，探索の高速化に有効なデータ構造と並列探索アルゴリズムを設計・実装し，その効果を確認した．高度な索引構造については今後の課題である．ハイブリッド制約言語処理系のための高信頼近似計算については，本年度は離散変化を起こす時刻の精度保証求解というもっとも必要度の高い場面について，区間ニュートン法に基づくアルゴリズムの検討と実験を進めた．それと並行して平行体計算に基づく非線形ハイブリッドシステムの精度保証シミュレーション・検証手法を開発したが，HyLaGI処理系への統合は今後の課題である．HydLaプログラムからのハイブリッドオートマトン抽出については，公開中のHyLaGI処理系に組み込むことができ，次のステップとしてHyLaGI処理系のモデル検査系への発展に向けた検討に着手した．
平成26年度の計画に明記した項目に加えて，SLIM並列モデル検査系における状態圧縮機能が実現され，グラフというデータ構造を用いながら20億状態規模のモデル検査が可能になったことは大きな成果である．また，平成27年度の実施計画の中のハイブリッド制約プログラムのスケーラビリティ改善に関して，複雑な系を簡潔に表現するためのリスト内包記法の設計・実装や，制約のインクリメンタルな求解に基づく計算量削減が前倒しで達成できたことも成果である．同じく平成27年度計画の中の多数のグラフのための一意バイト列表現についても，概念整理と実験を前倒しで進めることができた．
|
| Strategy for Future Research Activity |
二つの高水準モデリング言語処理系の実装技術の深化については，多くの大学院生との共同作業の中から多くの新たな着想が生まれてきている．個々の着想は要素技術としての検討を経て，各技術の研究のフェーズに応じて処理系への組み込みが進みつつある．
現時点で特に難度が高いと認識している問題は，大規模グラフの書換え系における相互排他のオーバーヘッドを抑えたスケーラブルな並列化，およびハイブリッドシステムの精度保証シミュレーションにおける記号実行と高信頼近似計算との融合とスケーラビリティの確保である．どちらもさらに基礎検討や予備実験を重ねながら方針を固めてゆきたいと考えている．
|
| Causes of Carryover |
予定していた国際会議参加に関して，別予算から旅費参加費を手当てすることがてきたため．
|
| Expenditure Plan for Carryover Budget |
フランスの区間制約プログラミング研究者を招聘して共同研究を行う費用に充てる予定である．
|
