Construction of "Model program cooperation environment" for reliable software development

构建可靠软件开发的“模范程序协作环境”

• 批准号: 19700016
• 负责人: TANABE Makoto
• 金额: $ 1.91万
• 依托单位: Ube National College of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2007
• 资助国家: 日本
• 起止时间: 2007 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19700016/
• 关键词: プログラム理論; ソフトウェア検証; モデル検査; UPPAAL; Java Modeling Language,Stateパターン; 形式検証; プログラム意味論; 時相論理; CTL; JML; UML

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.

提出了一种将模型检测工具UPPAAL的模型转换为JAVA程序源代码的转换技术，并开发了两种转换工具。一种是用JML（Java Modeling Language）描述生成JAVA源代码，另一种是用相应的状态模式描述再现给定模型上的状态转换生成JAVA源代码，并将转换技术应用于一个订票系统的设计与开发中，验证了该技术的有效性。