産業応用を目指したオブジェクト指向モデルの検証手法の提案

点击翻译按钮获取中文摘要

本年度は以下の成果を得た.・周期イベントに基づいたマルチタスクの振る舞いの検証法の提案.μITRONやOSEKに基づいたリアルタイムOS(RTOS)では,並行動作するマルチタスクを用いてソフトウェアを構成する.この場合,並行処理を直接的にプログラムできるが,その反面,並行動作に起因する問題の検出が困難になる.そこで昨年度までに,モデル検査ツールSpinを用いて,μITRONに基づいたRTOS上で動作するタスクの振る舞いを検証する手法などを提案してきた.この手法では,優先度,sleep/wakeupなどのスケジューリングの取り扱いを目的としている.一方で,マルチタスクソフトウェアでは周期やデッドラインといった時間に関する性質が重要であり,これまでに提案した手法では扱えなかった.そこで,今年度は,周期に基づいて動作するマルチタスクソフトウェアの検証法を提案した.まず,実際のCDプレーヤやDVDプレーヤを開発してきたエンジニアが,これまでの経験に基づいて,CDプレーヤの典型的な設計モデルになるようUMLで作成した.このようなソフトウェアでは,タスク間の状態に不整合が生じる状態不一致問題が典型的な問題として挙げられ,それは,周期実行やそれに関連する処理の実行タイミングが原因で発生していることがわかった.そこで,それらをモデル検査ツールSpinを用いて検証する手法,および,周期に関してより詳細な解析が行える手法を提案した.本研究では,これまでにモデル検査手法や定理証明手法を用いた現実的な検証手法を提案してきた.そして,焦点を当てたいくらかの問題について,提案手法が有効であることを示すことができた.このような問題は他にも様々なものがあることが容易に想像されるが,すべて統一的に扱える普遍的な検証手法は存在しないはずである.よって,典型的な問題を洗い出し,それら一つ一つについて解決する検証手法を今後も提案する必要がある.