| 研究概要 |
高性能検証のための要素技術の確立と,システム検証の基盤となるモデリング言語の整備を目指して,本年度は研究代表者のグループが開発を推進している2つのモデリング言語を核として以下の研究開発成果を得た.
階層グラフ書換え言語LMNtalについては,従来の通常の一対一接続のリンクに加えて多点接続のためのハイパーリンクの表現・操作機能を実装し,さらにそれを非決定的実行(状態空間構築)に対応させることで検証系の表現力を大幅に向上させた.また,公開中のLMNtal並列モデル検査器slimの整備を進めて版を重ねるとともに,(i)Δ-marking手法による状態空間圧縮技法,(ii)リアルタイムシステムの並列モデル検査器への拡張,(iii)組合せ最適化の並列求解系への拡張をそれぞれ試験的に実装して評価を行った.
制約に基づくハイブリッドシステムモデリング言語HydLaについては,前年度に基本設計を行った非決定実行アルゴリズムの実装を進め,初期値の一部が区間値として与えられたシステムや記号パラメタをもつシステムのシミュレーション実行を可能にした.このようなシステムは一般に複数の定性的に異なる軌道をもつが,HydLa処理系は初期値に関する場合分けを行ってその全解を求める.この機能を利用してハイブリッドシステムの解析例の蓄積を進めた.また,これまでのHydLa実行系はMathematicaを数式処理エンジンとして用いていたが,それに加えて計算機代数システムReduceも利用できるようにした.さらに,HydLa処理系の検証系への拡張の第一歩として,HydLaプログラムからのハイブリッドオートマトンの抽出に関する基礎研究を行った.
|
| 今後の研究の推進方策 |
これまで通り,高水準モデリング言語処理系の開発・使用経験を軸として,新たな要素技術の確立および応用分野・波及効果の拡大を図る.階層グラフ書換え言語LMNtalについては,ハイパーリンク機能の実装に伴い表現力が拡大したことを活かし,他の代表的計算体系のLMNtalへのエンコードを進めて,LMNtalモデル検査器がそれらの計算体系のためのモデル検査器としても利用できるようにする.またそれを可能にするための抽象化技術を確立する.ハイブリッド制約言語HydLaについては,高性能検証の実現手法を根本から検討すべく,まず現在の非決定的シミュレーションアルゴリズムの実際の挙動を深く分析し,その結果に基づいて高速化,並列化および抽象化の方向性を探求する.
|
