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

2008 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年度は以下の研究を行った。
1. UPPAAL(モデル)からJML(プログラム)への変換システムを構築した。
モデル検査ツールUPPAALによって作成されたモデルを読み込み、JML記述の付加されたJAVAソースコードを生成する変換システムを構築した。構築にあたっては、UPPAALのテンプレート記述をJAVAのクラス定義に、UPPAALのプロセス記述をJAVAのインスタンス生成に対応付け、UPPAALのチャネルによる同期通信をJAVAのメソッド呼び出しに対応づけた。また、変換システムはコンパイラ・コンパイラの一種であるJavaCCを用いて実装を行った。これにより、変換による対応付けの定義と、変換操作の詳細をある程度分けて記述することが可能となり、今後の機能追加や、UPPAALLの仕様変更への対応に柔軟に対応できることとなった。
2. UMLモデルからUPPAALモデルへの変換システムを試作した。
UML(Unified Modeling Lanuage : 統一モデリング言語)はソフトウェアを中心とするシステムの仕様を記述し、視覚化し、構築し、文書化するために設計されたモデリングの規約であり、近年のオブジェクト指向開発における設計段階で用いられている。平成20年度は、UMLモデルの一つであるステートチャート図からUPPAALモデルへの変換システムを試作した。具体的には、UMLの標準的な保存形式であるXMIからUPPAALモデル記述のXMLへのファイル変換システムを作成した。これにより、UMLツールを用いて作成したモデルをXMI形式で保存し、UPPAALで読み込み可能なXML形式のモデル記述ファイルに変換することにより、UPPAAL上でモデル検査を行うことが可能となった。