信頼性の高いソフトウェア開発に向けた「モデル-プログラム協調環境」の構築

2009 Fiscal Year Annual Research Report

• Project/Area Number: 19700016
• Research Institution: Ube National College of Technology
• Principal Investigator: 田辺 誠 Ube National College of Technology, 制御情報工学科, 准教授 (00353318)
• Keywords: 形式検証 / プログラム意味論 / モデル検査 / 時相論理 / CTL / UPPAAL / JML / UML

Research Abstract

平成20年度での二年間の研究で、UPPAAL(モデル)からJAVAプロクラムへの変換システムを構築した。平成21年度は三年間の研究のまとめとして、変換システムの有用性を検証するためのケースワークを行った。ケースワークの題材としてチケット予約システムの設計を採り上げ、以下の順で検証を行った。
1. UPPAALモデルによる形式設計および検証
WEB上のチケット予約システムの要求仕様からソフトウェアの動作モデルをUPPAAL上で作成した。動作モデルは先行研究を参考とし、形式仕様を満足するような改良を行った。また、作成されたモデルが仕様を満たすことをモデル検査によって確認した。
2. UPPAALモデルからJAVAプログラムへの変換
本研究によって作成した変換システムを用い、モデルをプログラムに変換した。これによって、モデルに記述された通りのシステム遷移を行うプログラムが得られた。
3. プログラムの完成
2. で得られたプログラムはモデルと同等の詳細度しかないため、実際の入出力等の詳細を実装し、チケット予約システムのプロトタイプを作成した。このプロトタイプは1.で検証済みの仕様を満たすことが保証されているため、高い安全性を持つことができる。
以上のケースワークを通じ、本研究で作成された変換システムの有用性を確認した。