2013 Fiscal Year Final Research Report
Implementations of high-level modeling languages that integrate high-performance verifiers
| Project/Area Number |
23300011
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
UEDA Kazunori 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TANABE Yoshinori 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60443199)
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
HOSOBE Hiroshi 法政大学, 情報科学部, 教授 (60321577)
ISHII Daisuke 東京工業大学, 情報理工学研究科, 助教 (00454025)
|
|---|
| Project Period (FY) |
2011-04-01 – 2014-03-31
|
| Keywords | 高水準モデリング言語 / 言語処理系 / モデル検査 / ハイブリッドシステム / 並列処理 |
|---|
| Research Abstract |
Modeling and verification technologies of natural, symbolic and cyber-physical systems are becoming increasingly important. The aim of this research was to demonstrate the viability of high-level modeling languages based on mathematical notions such as graphs, sets, equations and inequations whose generality goes far beyond Computer Science. To achieve this goal, we constructed two publicly available language implementations that integrate runtime systems and verifiers. One of them is an implementation of the graph rewriting language LMNtal, which has now evolved into a parallel model checker with hypergraph rewriting capabilities; the other is an implementation of the hybrid constraint language HydLa, which has evolved into a non-deterministic symbolic execution system for hybrid systems with uncertainties.
|
