2009 Fiscal Year Final Research Report
Construction of "Model program cooperation environment" for reliable software development
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
|
Keywords | プログラム理論 / ソフトウェア検証 / モデル検査 / UPPAAL / Java Modeling Language,Stateパターン |
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.
|