| Project/Area Number |
19700016
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Ube National College of Technology |
|---|
Principal Investigator |
TANABE Makoto Ube National College of Technology, 制御情報工学科, 准教授 (00353318)
|
|---|
| Project Period (FY) |
2007 – 2009
|
| Project Status |
Completed (Fiscal Year 2009)
|
| Budget Amount *help |
¥2,980,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥480,000)
Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2007: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | プログラム理論 / ソフトウェア検証 / モデル検査 / UPPAAL / Java Modeling Language,Stateパターン / 形式検証 / プログラム意味論 / 時相論理 / CTL / JML / UML |
|---|
| Research Abstract |
A transformational technology is developed from models of a model-checking tool UPPAAL to JAVA program source codes that keep the properties guaranteed by model-checking process.
Two kinds of translation tools are developed. One generates JAVA source codes with JML (Java Modeling Language) description, and the other generates JAVA source codes where the state transition on the given model is reproduced by the corresponding state pattern description.
The effectiveness of this technology is verified by applying the transformational technology to the design and development of a ticket reservation system.
|
