| 研究概要 |
本年度は以下の2つの成果が得られた.
(1)モデル検査手法と定理証明手法を併用した仕様の検証法を提案.組込みシステムで重要な役割を担っている部品、センサーに注目することにして、モデル検査を適用する手法について研究を行った。これまでに、センサーの仕様をSCR(Software Cost Reduction)法のモード遷移表を用いてモデル化する手法、および、それをモデル検査ツールSMVで検証する手法について提案した。モード遷移表には自然数などの変数が記述されており、SMVで検証する前に、それらを抽象化する必要がある。提案した手法では、抽象解釈法の一種であるデータマッピング法で、定理証明システムを用いながら効率的に抽象化を行う手法を提案した。今後は、検査した仕様に基づいて、センサーへのアクセスメカニズム、および、制御のためのスケジューリングを考慮に入れた設計モデルをいかに構成するかについて研究を行う予定である。
(2)定理証明手法によるオブジェクト指向分析・設計モデルの検証法の提案.分析・設計モデルでは,メソッドや制約の詳細をアクション言語や制約言語で記述する.そこで,これらの言語を用いて記述された分析・設計モデルを定理証明手法で取り扱う方法を提案した.また,これまでは,クラス図とステートチャート図を対象とした検証法を提案したきたが,UMLでは,他にもいくらかの図が存在する.それらのうちで重要な図の1つであるコラボレーション図に焦点を当てた検証法も提案した.
|
