| 研究概要 |
本年度は以下の2つの成果を得た.
(1)モデル検査手法によるRTOSに基づいたソフトウェアの検証法の提案。
組込みソフトウェア開発ではμITRONのような優先度付きマルチタスクが扱えるRTOS(Real Time Operating System)を用いる場合が多い.この場合,並行処理を直接的にプログラムできるが,その反面,その動作の検証が困難になる.そこで,モデル検査手法を用いてRTOSに基づいたソフトウェアを検証する手法を提案した.本研究では、μITRONに基づいたソフトウェアを対象とした.モデル検査ツールはSpinを用いた.一方で,Spinではタスクのスケジューリングや優先度,その他のサービスコールを直接的には扱うことができない.そこで,それらを扱えるようにするためのライブラリを実現した.これにより,μITRONのサービスコールを直接的にSpinの入力に記述できるようになった.今後は,実際の組込みソフトウェアの検証,および,μITRONに準拠したRTOS自体の検証を行う予定である。
(2)ステートチャートに基づいた定理証明手法によるオブジェクト指向設計モデルの検証法の提案。
オブジェクト指向開発において,クラス図にアクショシ言語を用いて詳細を追加して設計モデルを作成する手法が主流になりつつある.このようなクラス図では,メソッド呼び出しの反応を見ることにより検査を行うことになる.しかしながら,通常,メソッド呼び出しの列は無限であるため,それぞれに対して検査する手法では正しさを保証できない.一方で,状態遷移モデルを用いれば,有限状態で無限の呼び出し列を表現することができる.そこで,状態遷移モデルのためのダイアグラムであるステートチャート図を用いてメソッドの呼び出し方をモデル化し,そのステートチャート図に基づいた検証法を提案した.
|
