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上でモデル検査を行うことが可能となった。
|