2014 Fiscal Year Research-status 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年度は「形式仕様変換とモデル検査支援のツール化」に主眼を当て，以下の研究観点の成果を導き発表した．
1．情報制御システムのドメイン特化された特性に基づき開発した段階的モデル検査手法は，従来手法より検証可能範囲を広げることができた．また，システム分割によるモデル検査を可能とする分割的モデル検査手法を考案した．その結果，モデル規模が大きいと本手法の方が短時間で検証可能となることを導き，サブシステム分割で検証しても相互関係を失うことなく検証を進められ，無分割より短時間で検証できることを示した．(13.研究発表の学会発表1件目)
2．現実の情報制御システムの規模に対する段階的および分割的モデル検査手法の有用性を検討し，限界や問題点を探った．その結果，段階的モデル検査では，属性抽出の難しさが課題となり，分割的モデル検査では，サブシステム分割時に制御判断を大域ルールと局所ルールに分けるための一般的な手法が必要となることを導いた．これらの問題に対し，解決策としてモジュラ検証手法を考案した．これは，モジュラ分割を因果関係の稀薄な物理的分割，構造的対称性による分割，独立性の高い振舞いの分割という異なる3タイプの分割によるモジュラ検証を可能とする．この手法の効果は属性数比率により判断できるため，必要性を考慮して利用できる．(13.研究発表の学会発表2,3件目)
3．第３段階の予備研究として，モデル検査時に生じる反例から原因箇所を推定するために必要な情報抽出手法の検討を行った．この研究では，いくつかの問題点が認められたが，一般的な状況設定のもとでの検討であるため，段階的・分割的モデル化やモジュラ検証を考慮すれば，その特徴を効果的に利用できる見通しを得ることができた．
以上の研究より，ツール化の実装に向け設計方針を定め，以降の研究につながる成果を導くことができた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究で設定した第1段階「情報制御ドメインの形式仕様の段階的・分割的モデル化」に基づき，概ね計画どおりの段階的・分割的なモデル化を図ることができ，第２段階「形式仕様変換とモデル検査支援のツール化」に基づき，検査支援を図るなかで，ソフトウェアモデルのモジュラ検証というアプローチを導き出すことができた．具体的には，段階的手法や分割的手法の有用性を評価するために，研究協力者の院生らとソフトウェア実験を繰り返し，情報制御ドメインに適した知識の体系化および設計モデルの仕様を検討した．その後，機能安全の検証項目および形式仕様を，検証系への変換アルゴリズムを開発し，検証系を用いたモデル検査を可能とした．その上で，安全性を検証するとともに，より広範な情報制御システムのモデル検証を可能とするためのモジュラ検証アプローチを考案し，その有用性を評価するための実験を行なった．昨年度に続き，(株)日立製作所の情報提供などの協力を得て，現実的なレベルにある情報制御システム，特に社会インフラ系システムを対象として研究を進めた．モジュラ検証アプローチでは，設計モデル仕様の特性により，幾つかのモジュラ分割法を取ることができ，その選択基準を計算量から判断できるものとして示すことができた．
|
| Strategy for Future Research Activity |
本研究で設定した３段階の区切りの第３段階「設計モデルの機能安全性の評価・可視化」に進めていく．
第２段階では，機能安全性評価のための検証項目を検討するために，複数の検証項目を対象としたモデル検査を行い，設計モデルと検証項目を見直し，設計モデルから形式仕様への変換と検証支援を実用レベルに引き上げる検討に取り組んだ．その結果，ソフトウェアモデルのモジュラ検証というアプローチを考案することができた．
続く第３段階では，このモジュラ検証アプローチを情報制御ドメイン内のいくつかのシステムの設計モデルに適用し，想定ドメイン内の仕様変換とモデル検査を支援できる範囲の検討を進める．加えて，実用化検討を踏まえた検証項目に対する機能安全性のモデル検査を行い，実用レベルで検査結果を導出し，ドメイン技術者に可視化する支援ツールを構築する予定である．
|
| Causes of Carryover |
平成26年度の研究経費使用では，実用レベルのソフトウェアを対象とした品質検査や形式検証に取り組むには，仕様を整える必要があり，データ処理が必要となった．そのための作業補助を必要とした．また，品質検査や形式検証の結果を受けて，支援ツールの論理再設計を行なうにも相応の作業補助を必要とした．調査および研究協力企業との打合せ，研究成果発表のための旅費を必要とした．加えて，ソフトウェアのライセンス継続料を必要とした．しかしながら，本年度は研究の見直し部分が多いため，前年度ほどの成果発表が生じず，当初計画通りの経費使用となったため，平成25年度からの持ち越し相当額を再度，持ち越すこととなった．
|
| Expenditure Plan for Carryover Budget |
平成27年度の研究経費使用計画では，最終目標となる実用レベルの検証支援ツールを実装するには，ドメイン技術者向けの評価・可視化機能が必要となり，相当の開発作業量が必要となるので，研究協力者を増やし，数名体制でソフトウェア開発に当たってもらう予定である．また，ソフトウェアのライセンス継続料，調査および研究協力企業との打合せ，最終成果発表のための旅費が必要である．
|
Research Products
(3 results)
