2005 Fiscal Year Annual Research Report
産業応用を目指したオブジェクト指向モデルの検証手法の提案
| Project/Area Number |
16700028
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
青木 利晃 北陸先端科学技術大学院大学, 安心電子社会研究センター, 特任助教授 (20313702)
|
|---|
| Keywords | オブジェクト指向 / モデル検査 / 定理証明 / 検証 / 形式的手法 |
|---|
| Research Abstract |
本年度は以下の2つの成果を得た.
(1)モデル検査手法によるRTOSに基づいたソフトウェアの検証法の提案。
組込みソフトウェア開発ではμITRONのような優先度付きマルチタスクが扱えるRTOS(Real Time Operating System)を用いる場合が多い.この場合,並行処理を直接的にプログラムできるが,その反面,その動作の検証が困難になる.そこで,モデル検査手法を用いてRTOSに基づいたソフトウェアを検証する手法を提案した.本研究では、μITRONに基づいたソフトウェアを対象とした.モデル検査ツールはSpinを用いた.一方で,Spinではタスクのスケジューリングや優先度,その他のサービスコールを直接的には扱うことができない.そこで,それらを扱えるようにするためのライブラリを実現した.これにより,μITRONのサービスコールを直接的にSpinの入力に記述できるようになった.今後は,実際の組込みソフトウェアの検証,および,μITRONに準拠したRTOS自体の検証を行う予定である。
(2)ステートチャートに基づいた定理証明手法によるオブジェクト指向設計モデルの検証法の提案。
オブジェクト指向開発において,クラス図にアクショシ言語を用いて詳細を追加して設計モデルを作成する手法が主流になりつつある.このようなクラス図では,メソッド呼び出しの反応を見ることにより検査を行うことになる.しかしながら,通常,メソッド呼び出しの列は無限であるため,それぞれに対して検査する手法では正しさを保証できない.一方で,状態遷移モデルを用いれば,有限状態で無限の呼び出し列を表現することができる.そこで,状態遷移モデルのためのダイアグラムであるステートチャート図を用いてメソッドの呼び出し方をモデル化し,そのステートチャート図に基づいた検証法を提案した.
|
