2013 Fiscal Year Research-status Report
| Project/Area Number |
25330075
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Ibaraki University |
|---|
Principal Investigator |
上田 賀一 茨城大学, 工学部, 教授 (00213372)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | モデル検査 / モデル駆動開発 / ソフトウェア安全性検証 / 情報制御システム / 機能安全 |
|---|
| Research Abstract |
平成25年度は「情報制御ドメインの形式仕様の段階的・分割的モデル化」に主眼を当て，以下の研究観点の成果を導き発表した．
1．情報制御システムのドメイン特化された特性に基づき，段階的なモデル検査手法を開発し，有効性を評価した．その結果，従来手法より少ないメモリで検証可能であり，従来手法では検証可能範囲を広げた．また，モデル規模が大きくなると，本手法の方が短時間で検証可能となることを導いた．次に，システム分割によるモデル検査を可能とする分割的モデル検査手法を考案し，有効性を評価した．その結果，サブシステム分割して検証を行っても相互関係を失うことなく検証を進められ，無分割より短時間で検証できることを示した．
2．現実の情報制御システムの規模に対する段階的および分割的モデル検査手法の有用性に関する検討を行い，現状の限界や問題点を探った．その結果，段階的モデル検査では，属性抽出の難しさが課題となることが分かった．また，分割的モデル検査では，サブシステム分割時に，制御判断を大域ルールと局所ルールに分けるための一般的な手法が必要となることを導いた．これらの問題に対し解決策を検討しており，第２段階で合わせて対応する．
3．情報制御システム向け設計モデリング言語のメタモデル化を図り，検証系Alloyによる正当性検証を行い，言語としての問題がないことを確認した．加えて，第３段階の予備研究として，モデル検査時に生じる反例（正常の終了状態に至らない事例）を容易に取り扱うための視覚化のあり方と原因箇所を推定するために必要な情報の検討を行った．この予備研究では，いくつかの限界点や問題点が認められたが，一般的な状況設定のもとでの検討であるため，段階的・分割的モデル化を考慮すれば，その特徴を効果的に解決できる見通しを得ることができた．
|
| 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段階「情報制御ドメインの形式仕様の段階的・分割的モデル化」に基づき，概ね計画どおりの段階的・分割的なモデル化を図ることができたと考える．具体的には，段階的手法や分割的手法の有用性を評価するために，研究協力者の院生らとソフトウェア実験を繰り返し，情報制御ドメインに適した知識の体系化および設計モデルの仕様を検討した．その結果として，機能安全の検証項目を仮設定し，検証系への変換アルゴリズムを開発し，検証系を用いたモデル検査を可能とした．その上で，安全性を検証するとともに，段階的手法と分割的手法の有用性を評価するための実験を行なった．この際，(株)日立製作所の情報提供などの協力を得て，現実的なレベルにある情報制御システム，特に社会インフラ系システムを対象として研究を進めた．また，設計モデル仕様そのものの形式仕様への変換についても検討を進め，検証系SPINに適用する方法の開発を進めることができた．
|
| Strategy for Future Research Activity |
本研究で設定した３段階の区切りの第２段階「形式仕様変換とモデル検査支援のツール化」，第３段階「設計モデルの機能安全性の評価・可視化」に進めていく．
第２段階では，機能安全性評価のための検証項目を検討するために，多くの検証項目を対象としたモデル検査を行う予定である．その上で，設計モデルと検証項目の見直しを行い，設計モデルから形式仕様への変換と検証支援を実用レベルに引き上げる検討に取り組む．また，この見直しを試作ツールにも反映する．情報制御ドメイン内のいくつかのシステムの設計モデルに適用を広げ，想定ドメイン内の仕様変換とモデル検査を支援できる範囲の検討を進める．
続く第３段階では，実用化検討を踏まえた検証項目に対する機能安全性のモデル検査を行い，評価をドメイン技術者に可視化する支援ツールを構築する予定である．
|
| Expenditure Plans for the Next FY Research Funding |
平成25年度の研究経費使用では，予定されたPCの価格変更や性能変更に伴い，選定品を変更したことと，開発用・モデル設計用に選定したソフトウェアのライセンス形態により当初予定ほどの費用がかからなかった．一方で，当初予定より研究成果発表機会が増え，旅費は予定以上に必要となった．以上のことから10万円程の差額残が生じた．次年度以降も，基本的な使用計画に変更はないが，今後も発表機会が増えることも考えられ，旅費に充当することが必要となる．
平成26年度の研究経費使用計画では，実用レベルのソフトウェアを対象とした品質検査や形式検証に取り組むには，設計仕様書を整える必要があり，そのための作業補助を必要とする．また，品質検査や形式検証の結果を受けて，支援ツールの論理再設計を行なうにもかなりの作業補助を必要とする．調査および研究協力企業との打合せ，研究成果発表のための旅費を必要とする．加えて，ソフトウェアのライセンス継続料が必要である．
平成27年度の研究経費使用計画では，最終目標となる実用レベルの検証支援ツールを実装するには，ドメイン技術者向けの評価・可視化機能が必要となり，相当の開発作業量が必要となるので，研究協力者を増やし，数名体制でソフトウェア開発に当たってもらう予定である．また，ソフトウェアのライセンス継続料，調査および研究協力企業との打合せ，最終成果発表のための旅費が必要である．
|
