• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2012 年度 実績報告書

高性能検証系を統合した高水準モデリング言語処理系の構築

研究課題

研究課題/領域番号 23300011
研究機関早稲田大学

研究代表者

上田 和紀  早稲田大学, 理工学術院, 教授 (10257206)

研究分担者 田辺 良則  国立情報学研究所, 大学共同利用機関等の部局等, 教授 (60443199)
研究期間 (年度) 2011-04-01 – 2014-03-31
キーワード高水準モデリング言語 / 言語処理系 / モデル検査 / ハイブリッドシステム / 並列処理
研究概要

実行系と検証系を統合した高水準モデリング言語の処理系の構築に関して,以下の二つの処理系を軸に研究開発を実施した.
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モデル検査の状態管理において大きな役割を演ずるグラフ構造の効率的な一意エンコード手法の検討を進めた.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

高水準モデリング言語の発展という観点から研究は順調に進展している.言語仕様の観点からは,HydLaは処理系開発の深化および例題の蓄積によって妥当性確認が進み,LMNtalはハイパーリンクを備えたHyperLMNtalへと発展した.それぞれの処理系の機能強化やデバッグも順調に進み,HydLaにおいてはパラメータつきシステムの自動場合分けに基づくシミュレーションや有界モデル検査,LMNtalにおいては状態空間構築の効率化やHyperLMNtalのモデル検査への対応をはじめとする多様な研究が進展した.HydLaとハイブリッドオートマトンとの関連付けをはじめ,検証系の発展のための基盤技術の整備も進んだ.一方,HydLaにおいては区間計算の導入が次の重要課題として浮上し,LMNtalにおいては状態空間爆発への対処方法の開発が課題となってきた.

今後の研究の推進方策

新要素技術の設計,実装,現存処理系への統合については,基本的にこれまでの体制と方法でさらに進展すると期待される.区間計算に基づくHydLaプログラムの高信頼近似計算技術については,区間計算の専門家の協力と助言をもらいつつ推進する予定である.

  • 研究成果

    (14件)

すべて 2013 その他

すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (10件) 図書 (1件) 備考 (2件)

  • [雑誌論文] ハイブリッド制約言語HydLaの記号実行シミュレータHyrose2013

    • 著者名/発表者名
      松本翔太, 上田和紀
    • 雑誌名

      コンピュータソフトウェア

      巻: Vol. 30, No. 4 ページ: 18-35

    • DOI

      10.11309/jssst.30.4_18

    • 査読あり
  • [学会発表] HydLa: A High-Level Language for Hybrid Systems

    • 著者名/発表者名
      Kazunori Ueda, Shota Matsumoto, Akira Takeguchi, Hiroshi Hosobe, Daisuke Ishii
    • 学会等名
      Second Workshop on Logics for System Analysis (LfSA 2012)(査読有)
    • 発表場所
      Berkeley, CA, USA
  • [学会発表] Hybrid Constraint Language HydLa and Its Implementation

    • 著者名/発表者名
      Shota Matsumoto, Akira Takeguchi, Kazunori Ueda, Hiroshi Hosobe
    • 学会等名
      15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012)(査読有)
    • 発表場所
      北京、中国
  • [学会発表] ハイブリッド制約言語プログラムのハイブリッドオートマトンへの変換アルゴリズム

    • 著者名/発表者名
      竹口 輝,和田 亮,松本 翔太,細部 博史,上田 和紀
    • 学会等名
      日本ソフトウェア科学会第29回大会
    • 発表場所
      東京
  • [学会発表] ハイブリッド制約言語HydLaの記号実行シミュレータHyrose

    • 著者名/発表者名
      松本 翔太,上田 和紀
    • 学会等名
      日本ソフトウェア科学会第29回大会
    • 発表場所
      東京
  • [学会発表] 複数の計算モデルをサポートするモデル検査器の実現

    • 著者名/発表者名
      目黒 学,谷口 直輝,上田 和紀
    • 学会等名
      日本ソフトウェア科学会第29回大会
    • 発表場所
      東京
  • [学会発表] LMNtalによるBigraphのエンコードおよびモデル検査の実現

    • 著者名/発表者名
      目黒 学, 宮原 和大, 上田 和紀
    • 学会等名
      第10回 ディペンダブルシステムワークショップ (DSW 2012)
    • 発表場所
      神戸
  • [学会発表] 動的に変化するグラフのための効率的な一意エンコード生成手法

    • 著者名/発表者名
      宮原 和大, 上田 和紀
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
    • 発表場所
      会津若松
  • [学会発表] LMNtal処理系SLIMのマルチスレッド化による最短経路問題のデータ並列求解

    • 著者名/発表者名
      青山 龍一, 上田 和紀
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
    • 発表場所
      会津若松
  • [学会発表] SLIMの階層グラフのためのキャッシュコンシャスかつ効率的なデータ構造

    • 著者名/発表者名
      吉田 健人, 上田 和紀
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
    • 発表場所
      会津若松
  • [学会発表] LMNtal並列モデル検査における状態生成数削減及び高速化

    • 著者名/発表者名
      安田 竜, 上田 和紀
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
    • 発表場所
      会津若松
  • [図書] Concurrent Objects and Beyond (COB 2012), G. Agha et al. (eds.) (査読有)2013

    • 著者名/発表者名
      Kazunori Ueda
    • 総ページ数
      26
    • 出版者
      Towards a Substrate Framework of Computation
  • [備考] LMNtal, a unifying language and tool

    • URL

      http://www.ueda.info.waseda.ac.jp/lmntal/

  • [備考] 制約概念に基づくハイブリッドシステムモデリング言語HydLa

    • URL

      http://www.ueda.info.waseda.ac.jp/hydla/

URL: 

公開日: 2014-07-24  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi