• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

状態爆発するWEBアプリケーションに対するソフトウェアモデル検査

研究課題

研究課題/領域番号 18049054
研究種目

特定領域研究

配分区分補助金
審査区分 理工系
研究機関大阪大学

研究代表者

岡野 浩三  大阪大学, 大学院情報科学研究科, 助教授 (70252632)

研究分担者 谷口 健一  大阪大学, 名誉教授 (00029513)
楠本 真二  大阪大学, 大学院情報科学研究科, 教授 (30234438)
山口 弘純  大阪大学, 大学院情報科学研究科, 助手 (80314409)
研究期間 (年度) 2006
研究課題ステータス 完了 (2006年度)
配分額 *注記
1,600千円 (直接経費: 1,600千円)
2006年度: 1,600千円 (直接経費: 1,600千円)
キーワードSPIN / UML / OCL / WEB / Struts / UPPAAL / timelines QoS
研究概要

ソフトウェアの安全性妥当性を論理的数学的な手段で保証することは情報爆発する情報社会にとってますます重要である.その手段の1つとしてソフトウェアモデル検査が近年注目を浴びている.本研究は,ソフトウェアモデル検査の有用性適用限界を規模に対するスケーラビリティの観点から調べることをその目的とする.具体的には(1)実時間システムのコンポーネントベースの時間性質の設計検証と(2)Strutsを用いて作成されたコンポーネントベースのWEBアプリケーションの各種例題に対して,ソフトウェアモデル検査を適用し,規模の観点から有用性を調べていく.また,状態爆発などによって生じる適用限界の壁をブレークスルーするための方法論をコンポーネントの分割を用いた一般性のある形で考案していく.状態爆発を克服する1つの方法はシステムを複数のサブシステムからなるコンポーネントベースシステムとしてとらえ,各コンポーネントの検証とシステム全体の検証に問題を分割することである.一般にソフトウェアシステムを設計する際,そのようなコンポーネントに分割して設計を行うことは自然なことである.本手法はそのことに着目し,設計段階の途中生産物(UML記述,WEB遷移図)を有効利用し,モデル検査する方法を提案し,実際に検査ツールを作成し,その有効性を調べた.ここでの課題は,システム全体の検証を行う際,コンポーネント分割したメリットを失うことなく,スケーラビリティを維持する方法を考案することや,計算機支援を通じて,適切なモデル化を効率良く行うことである.これまでのこの研究プロジェクトでは,UML記述されたコンポーネントベースの実時間システムに対して,効率よく時間QoS性質を検証する方法論とStrutsで記述されたWEBアプリケーションに対するページ遷移や内部動作のモデル検査を行う方法について研究成果を挙げてきた.実時間システムのコンポーネントベースの時間性質の設計検証においては,Bang&Olulfsenのプロトコル例題に対して,検証可能なことを示した.WEBアプリケーションについては企業新人研修で作成したオンラインショップの設計に対して適用可能であることを示した.このことはこのアプローチが有効であることを示していると考える.また後者についてはEclipse上のプラグインを開発した.

報告書

(1件)
  • 2006 実績報告書
  • 研究成果

    (2件)

すべて 2006

すべて 雑誌論文 (2件)

  • [雑誌論文] SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法2006

    • 著者名/発表者名
      浜口優, 吉村顕, 岡野浩三, 楠本真二
    • 雑誌名

      電子情報通信学会 技術研究報告 Vol. 106,No. 202

      ページ: 29-34

    • NAID

      110004824065

    • 関連する報告書
      2006 実績報告書
  • [雑誌論文] UML/OCLに記述された時間QoSの階層的検証手法の提案2006

    • 著者名/発表者名
      長井栄吾, 岡野浩三, 楠本真二
    • 雑誌名

      電子情報通信学会 技術研究報告 Vol. 106,No. 202

      ページ: 13-18

    • NAID

      110004824062

    • 関連する報告書
      2006 実績報告書

URL: 

公開日: 2006-04-01   更新日: 2018-03-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi