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