| 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
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥20,150,000 (Direct Cost: ¥15,500,000、Indirect Cost: ¥4,650,000)
Fiscal Year 2013: ¥6,370,000 (Direct Cost: ¥4,900,000、Indirect Cost: ¥1,470,000)
Fiscal Year 2012: ¥6,630,000 (Direct Cost: ¥5,100,000、Indirect Cost: ¥1,530,000)
Fiscal Year 2011: ¥7,150,000 (Direct Cost: ¥5,500,000、Indirect Cost: ¥1,650,000)
|
|---|
| 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.
|
