| 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 *help |
¥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.
|
