• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2013 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 23300011
Research InstitutionWaseda University

Principal Investigator

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

Co-Investigator(Kenkyū-buntansha) 田辺 良則  国立情報学研究所, 大学共同利用機関等の部局等, 教授 (60443199)
Project Period (FY) 2011-04-01 – 2014-03-31
Keywords高水準モデリング言語 / 言語処理系 / モデル検査 / ハイブリッドシステム / 並列処理
Research Abstract

実行系と検証系を統合した高水準モデリング言語の構築に関して,以下の二つの処理系を軸に研究開発を実施した.
1. ハイブリッドシステムモデリング言語HydLaの記号実行シミュレータHyroseについて以下の開発を進めた.(a) 無限時間モデル検査への発展を視野に入れて,前年度検討したHydLaからハイブリッドオートマトンへの変換技法を改良して実装した.(b) 記号的に解けない問題の解の存在範囲を正しく計算するために,記号実行処理系にアフィン演算を統合的に導入する方法の基礎検討を行った.(c) 制約が矛盾する原因をunsat coreを用いて説明するための機能をインタラクティブ実行系に組み込んだ.(d) Hyroseの基本演算である制約求解について,求解結果の再利用や制約間の依存関係解析に基づく最適化アルゴリズムを開発し実装を行った.(e) 求解エンジンとしてMathematicaに加えてREDUCEを使えるように拡張を行った.
2. 階層グラフ書換えに基づくモデリング言語LMNtalとその処理系について以下の研究開発を進めた.(a) 並列モデル検査機能について,MAPとNested DFSの複合によって効率とスケーラビリティを改善する方法を実装し評価を行った.(b) モデル検査における状態空間構築で重要な多数のグラフ構造間の同型性判定を効率化するために,グラフ間の差分情報に着目してグラフ正規化のコストを削減する手法を開発して試験実装と評価を行った.(c) 大規模グラフ書換えの並列処理を可能にする抽象機械命令を導入して評価を行った.(d) ハイパーグラフ書換え系への拡張について,多相型推論や論理型言語の実装実験を通じて有効性評価と処理系の保守改良を進めた.(e) LMNtalの文脈機能の拡張に向けて,ユーザ定義文脈機能の試験実装および例題記述実験を行った.(f) 汎用性の高い新たな実行可視化環境Grapheneの設計と実装を行った.

Current Status of Research Progress
Reason

25年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

25年度が最終年度であるため、記入しない。

  • Research Products

    (22 results)

All 2014 2013 Other

All Journal Article (4 results) (of which Peer Reviewed: 4 results) Presentation (15 results) (of which Invited: 1 results) Book (1 results) Remarks (2 results)

  • [Journal Article] LMNtal並列モデル検査における状態生成数削減及び高速化2014

    • Author(s)
      安田竜, 吉田健人, 上田和紀
    • Journal Title

      人工知能学会論文誌

      Volume: Vol. 29, No. 1 Pages: 182-187

    • DOI

      10.1527/tjsai.29.182

    • Peer Reviewed
  • [Journal Article] Coqを使用したMapReduceアプリケーションの検証とScalaコード2014

    • Author(s)
      姜 帆, 田辺 良則, 本位田 真一
    • Journal Title

      電子情報通信学会論文誌

      Volume: J97-D(3) Pages: 625-634

    • Peer Reviewed
  • [Journal Article] ハイブリッド制約言語HydLaの記号実行シミュレータHyrose2013

    • Author(s)
      松本翔太, 上田和紀
    • Journal Title

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

      Volume: Vol. 30, No. 4 Pages: 18-35

    • DOI

      10.11309/jssst.30.4_18

    • Peer Reviewed
  • [Journal Article] Java PathFinderにおける探索打ち切りポリシーを用いたヒューリスティック探索2013

    • Author(s)
      前岡 淳, 田辺 良則, 石川 冬樹
    • Journal Title

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

      Volume: 30(3) Pages: 109-122

    • DOI

      10.11309/jssst.30.3_109

    • Peer Reviewed
  • [Presentation] LMNtal処理系SLIMのマルチスレッド化による最短経路問題のデータ並列求解

    • Author(s)
      青山 龍一,上田 和紀
    • Organizer
      先進的計算基盤システムシンポジウム SACSIS2013
    • Place of Presentation
      仙台
  • [Presentation] LMNtal 並列モデル検査における 状態生成数削減及び高速化

    • Author(s)
      安田 竜,上田 和紀,吉田 健人
    • Organizer
      2013年度人工知能学会全国大会
    • Place of Presentation
      富山
  • [Presentation] Literal Block Distanceに基づく学習節共有を行う並列SATソルバGlucans

    • Author(s)
      徐 暁雋,松本 翔太,上田 和紀
    • Organizer
      2013年度人工知能学会全国大会
    • Place of Presentation
      富山
  • [Presentation] 制約の静的解析を用いたHydLa処理系の最適化

    • Author(s)
      河野 文彦,松本 翔太,上田 和紀
    • Organizer
      2013年度人工知能学会全国大会
    • Place of Presentation
      富山
  • [Presentation] Encoding type systems into HyperLMNtal

    • Author(s)
      Alimujiang Yasen, Kazunori Ueda
    • Organizer
      日本ソフトウェア科学会第30回大会(JSSST2013)
    • Place of Presentation
      東京
  • [Presentation] ハイブリッドシステム制約言語HydLaの数式処理実行系へのアフィン演算の導入

    • Author(s)
      松本翔太,上田和紀
    • Organizer
      日本ソフトウェア科学会第30回大会(JSSST2013)
    • Place of Presentation
      東京
  • [Presentation] グラフ書換え系におけるグラフ構造の効率的な一意バイト列生成手法

    • Author(s)
      宮原和大,上田和紀
    • Organizer
      日本ソフトウェア科学会第30回大会(JSSST2013)
    • Place of Presentation
      東京
  • [Presentation] LMNtalにおけるグラフ書換え操作のCoqによる形式化

    • Author(s)
      信夫裕貴,田辺良則,上田和紀
    • Organizer
      日本ソフトウェア科学会第30回大会(JSSST2013)
    • Place of Presentation
      東京
  • [Presentation] Software model checking for distributed systems with selector-based, non-blocking communication

    • Author(s)
      Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
    • Organizer
      ASE 2013
    • Place of Presentation
      Palo Alto, USA
  • [Presentation] Formalization of the Graph Rewriting Operations of LMNtal by Coq

    • Author(s)
      Yuuki Shinobu, Yoshinori Tanabe, Kazunori Ueda
    • Organizer
      11th Asian Symposium on Programming Languages and Systems (APLAS 2013)
    • Place of Presentation
      Melbourne, Australia
  • [Presentation] Optimized Canonical Graph Labeling Algorithm for Graph Rewriting Systems

    • Author(s)
      Kazuhiro Miyahara and Kazunori Ueda
    • Organizer
      11th Asian Symposium on Programming Languages and Systems (APLAS 2013)
    • Place of Presentation
      Melbourne, Australia
  • [Presentation] ハイブリッド制約言語HydLaの対話的な実行方式の実装

    • Author(s)
      和田亮,松本翔太,上田和紀
    • Organizer
      第11回 ディペンダブルシステムワークショップ (DSW 2013)
    • Place of Presentation
      熱海
  • [Presentation] 文脈に依存したグラフ書き換え系の設計と実装

    • Author(s)
      奈良 耕太,上田 和紀
    • Organizer
      第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014
    • Place of Presentation
      阿蘇
  • [Presentation] LMNtal実行時処理系SLIMにおけるグラフ構造探索の計算量改善

    • Author(s)
      青山 龍一,上田 和紀
    • Organizer
      第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014
    • Place of Presentation
      阿蘇
  • [Presentation] A Hybrid Constraint Language HydLa and Its Implementation

    • Author(s)
      Kazunori Ueda
    • Organizer
      Halmstad Colloquium
    • Place of Presentation
      Halmstad, Sweden
    • Invited
  • [Book] Towards a Substrate Framework of Computation, in Concurrent Objects and Beyond (COB 2012)2014

    • Author(s)
      Kazunori Ueda
    • Total Pages
      26
    • Publisher
      Springer-Verlag
  • [Remarks] LMNtal: A Unifying Language and Tool

    • URL

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

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

    • URL

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

URL: 

Published: 2015-05-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi