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

2007 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

Research Abstract

本研究は、モデル検査とプログラミング言語との融合をはかることを目的とする。平成19年度は、モデル検査ツールUPPAALからオブジェクト指向言語へ対応付けた。
UPPAALのモデル要素からオブジェクト指向言語要素への対応付けの概略は以下のとおりである。テンプレート(状態遷移図のひな形)をクラスに、状態遷移図をインスタンスに、状態遷移をメソッド呼び出しに、状態遷移図の状態をインスタンス変数に対応付ける。共有変数は、UPPAALクラスの静的変数(あるいはシングルトンのインスタンス変数)に対応付ける。
UPPAALの遷移にはGuardと呼ばれる前提条件が付加されており、遷移が行われるためにはこの条件が満たされることが必要である。このGuard要素の対応付けに注意を要した。対応付けの指針として以下の二種類が考えられた。一つは言語要素内に明示的に取り入れる方法である。この場合、取り入れる仕組みによって実装方法が制約を受けてしまう。もう一つはコメント文に変換する方法である。しかしこの方法ではモデルによって記述された仕様を守ることが実装者にゆだねられてしまい、安全な実装が保障されない。そこで本研究では、変換の対象言語をJAVA言語に固定し、遷移の前提条件をJML(Javaモデリング言語)に変換することにより、上述の二種類の変換方法の利点を採り入れた。JMLは、「契約による設計」(DBC: Design by Contract)の概念に基づきJava言語のモデリングを行うための言語である。Javaのコメント文としてJML形式でモデル記述を行い、JML専用のチェッカーにより、Javaプログラムがモデル記述に整合的に動作するかどうか確認することができる。これを用い、UPPAALの遷移に付加された制約条件をJMLに対応付けることにより、実装とUPPAALモデルとの整合性を確認することができる。また、JML記述は通常のコンパイル時にはコメントとして扱われるため、効率性を損なうことなくこの方式を導入できる。