2015 Fiscal Year Annual Research Report
| Project/Area Number |
25330075
|
|---|
| Research Institution | Ibaraki University |
|---|
Principal Investigator |
上田 賀一 茨城大学, 工学部, 教授 (00213372)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | モデル検査 / モジュラ検証 / ソフトウェア安全性検証 / 情報制御システム / 機能安全 |
|---|
| Outline of Annual Research Achievements |
平成25年度，26年度の研究を受け，平成27年度は，それらの研究結果を見直しつつ，「設計モデルの機能安全性の評価・可視化」に着目し，検証項目に対する機能安全性のモデル検査手法の実用化を踏まえた検討を行い，問題点となる反例とその原因の抽出や可視化について検討した．
1．ドメイン特化された特性に基づき開発した段階的モデル検査手法，および本研究で考案した分割的モデル検査手法により情報制御システムの分割によるモデル検査を行い，サブシステム分割で検証しても相互関係を失うことなく検証を進められ，無分割より短時間で検証できることを確認した．しかし，現実の情報制御システムの規模や複雑さに対する段階的および分割的モデル検査手法を探った結果，モデル検証を一般化する際の問題点が見出された．
２．段階的モデル検査では属性抽出が難しいこと，分割的モデル検査ではサブシステム分割時に制御判断を大域ルールと局所ルールに分けるための汎用手法が必要となる問題に対する解決策のひとつとして，モジュラ検証アプローチを考案し，因果関係の稀薄な物理的分割，構造的対称性による分割，独立性の高い振舞いの分割という異なる3タイプの分割によるモジュラ検証を可能とした．このアプローチを支援するモデル検証ツール群を試作し，の効果は属性数比率により判断できるため，必要性を考慮して利用できる．この成果を学会発表した(2)．
3．モデル検査時に生じる複数の反例から原因箇所を推定するために，適用ルールの順序や組合せの問題を発見するための手法を探り，推定アルゴリズムを検討した．段階的・分割的モデル化やモジュラ検証を考慮した上で，原因推定を支援するソフトウェアの試作を行った．この成果を学会発表した(1)．
以上の研究より，ツールの実用性の観点では充分とは言えないが，本研究の主目的につながる成果を導くことができた．
|
Research Products
(2 results)
