Towards Model Transformation Validation from Model Validation

• Project/Area Number: 22650007
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: National Institute of Informatics
• Principal Investigator: HU Zhenjiang 国立情報学研究所, アーキテクチャ科学研究系, 教授 (50292769)
• Co-Investigator(Kenkyū-buntansha): INABA Kazuhiro 国立情報学研究所, アーキテクチャ科学研究系, 研究員 (30570311)
• Co-Investigator(Renkei-kenkyūsha): HIDAKA Soichiro 国立情報学研究所, アーキテクチャ科学研究系, 助教 (70321578) ; KATO Hiroyuki 国立情報学研究所, コンテンツ科学研究系, 助教 (10321580)
• Project Period (FY): 2010 – 2011
• Project Status: Completed (Fiscal Year 2011)
• Budget Amount: ¥2,470,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥270,000); Fiscal Year 2011: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2010: ¥1,300,000 (Direct Cost: ¥1,300,000)
• Keywords: モデル変換 / モデル駆動ソフトウェア / 検証 / グラフ変換 / 双方向変換 / プログラム言語論 / プログラミングパラダイム

Research Abstract

In this research, we succeeded in designing a static verification algorithm for validating transformations in UnQL(UnCAL), a known graph(model) querying language. Our new approach to the verification problem is based on the two important characteristics of UnCAL, bisimulation-equivalence of graphs and structured recursion, and we show that a graph transformation in the Core UnCAL can be automatically checked with the MONA system against a schema specified in the powerful monadic second order logic(MSO). Moreover, we show that ranges of transformations can be statically computed, which can be used to exclude invalid updates on the resulting graph of a transformation.

Research Products

• [Journal Article] 模倣に基づくグラフスキーマを利用したビュー更新可能性判定 (2012)
  • Author(s): 中野圭介、日高宗一郎、胡振江、稲葉一浩、加藤弘之
  • Journal Title: コンピュータソフトウェア Volume: 29巻2号 Pages: 174-191
  • NAID: 130004549266
  • URL: https://www.jstage.jst.go.jp/article/jssst/29/2/29_2_174/_pdf
  • Peer Reviewed
• [Journal Article] Sound and Complete Validation of Graph Transformations (2010)
  • Author(s): Kazuhiro Inaba, Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano
  • Journal Title: Technical Report Volume: 04 Pages: 1-27
  • URL: http://grace-center.jp/downloads/GRACE-TR-2010-04.pdf
• [Journal Article] Sound and Complete Validation of Graph Transformations (2010)
  • Author(s): Kazuhiro Inaba, Soichiro Hidaka, Zehnjiang Hu, Hiroyuki Kato, Keisuke Nakano
  • Journal Title: Technical Report GRACE-TR-2010-04 Volume: 2010-04 Pages: 1-27
• [Presentation] Graph-Transformation Verification using Monadic Second-Order Logic (2011)
  • Author(s): Kazuhiro Inaba, Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano
  • Organizer: 13^<th> International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming(PPDP 2011)
  • Place of Presentation: University of Southern Denmark, Odense, Denmark
  • Year and Date: 2011-07-20
• [Presentation] Graph-Transformation Verification using Monadic Second-Order Logic (2011)
  • Author(s): Kazuhiro Inaba, Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano
  • Organizer: 13^<th> International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011)
  • Place of Presentation: University of Southern Denmark, Odense, Denmark
  • Year and Date: 2011-07-20
• [Presentation] 模倣に基づくグラフスキーマを利用したビュー更新可能性判定 (2011)
  • Author(s): 中野圭介、日高宗一郎、胡振江、稲葉一浩、加藤弘之
  • Organizer: 第13回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 定山渓ビューホテル、北海道
  • Year and Date: 2011-03-10
• [Presentation] 模倣に基づくグラグスキーマを利用したビュー更新可能製判定 (2011)
  • Author(s): 中野圭介、日高宗一郎、胡振江、稲葉一浩、加藤弘之
  • Organizer: 第13回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 定山渓ビューホテル、北海道
  • Year and Date: 2011-03-10
• [Presentation] Range Analysis of Graph Transformation for Simulation-based Schema(poster) (2010)
  • Author(s): Keisuke Nakano, Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato
  • Organizer: 8^<th> Asian Symposium on Programming Languages and Systems(APLAS 2010)
  • Place of Presentation: Hengshan Hotel, Shanghai, China
  • Year and Date: 2010-11-30
• [Presentation] Range Analysis of Graph Transformation for Simulation-based Schema (2010)
  • Author(s): Keisuke Nakano, Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato
  • Organizer: 8^<th> Asian Symposium on Programming Languages and Systems (APLAS 2010)
  • Place of Presentation: Hengshan Hotel, Shanghai, China(poster)
  • Year and Date: 2010-11-30
• [Presentation] Bidirectionalizing Graph Transformations (2010)
  • Author(s): Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Keisuke Nakano, Kazutaka Matsuda
  • Organizer: 15^<th> ACM SIGPLAN International Conference on Functional Programming(ICFP 2010)
  • Place of Presentation: Hyatt Regency Inner Harbor, Baltimore, America
  • Year and Date: 2010-09-28
• [Presentation] Bidirectionalizing Graph Transformations (2010)
  • Author(s): Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Keisuke Nakano, Kazutaka Matsuda
  • Organizer: 15^<th> ACM SIGPLAN International Conference on Functional Programming (ICFP 2010)
  • Place of Presentation: Hyatt Regency Inner Harbor, Baltimore, America
  • Year and Date: 2010-09-28
• [Remarks] 発表論文、開発したシステムのソースなどを下記のプロジェクトのページからご覧いただける
  • URL: http://www.biglab.org/