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

• 浜口, 優

• 吉村, 顕

• 岡野, 浩三

• 楠本, 真二

書誌事項

タイトル別名

• Hierarchical Model-checking for Web Application with SPIN
• SPIN　ヲ　モチイタ　ウェブ　アプリケーション　ニ　オケル　カイソウベツ　モデル　ケンサ　シエン　ホウホウ

抄録

ウェブアプリケーションの開発では,ユーザの誤入力である二重送信やタイムアウト発生時の動作,さらにはウェブアプリケーションの内部処理におけるデッドロックを考慮する必要がある.このため設計誤りはできる限り早期に検出することが望まれる.近年,ソフトウェア検証手法としてモデル検査が注目を集めている.しかし,モデル検査においては,状態爆発を考慮に入れた上での検証モデルの抽出や記述の難しさが問題点になっている.本稿ではStrutsを用いたウェブアプリケーション仕様を,ページ遷移を検証するモデルと内部処理を検証するモデルに階層別にモデル化するモデル検査手法を提案する.階層別に行うことにより状態爆発を回避している.また提案手法をもとにした検証用モデル生成支援ツールの試作を行った.この手法をある企業の新人研修で開発されたウェブアプリケーションをもとにした例題に適用し,手法およびツールの実用性の評価実験を行い,本手法の有効性を確かめた.

収録刊行物

• 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス

  電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 106 (202), 29-34, 2006-07-28

  電子情報通信学会

キーワード

• モデル検査
• Struts
• 共有資源
• 状態爆発
• Model-checking
• Shared resource
• State explosion
• Promela
• SPIN

詳細情報

• CRID: 1050018218951060608
• NII論文ID: 110004824065
• NII論文ID: 10031116752
• NII書誌ID: AN10013287
• HANDLE: 11094/27418
• NDL書誌ID: 8047779
• ISSN: 09135685
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I8047779
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN