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

浜口, 優; 吉村, 顕; 岡野, 浩三 他

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

Number of Access:451（2025-09-04 16:35 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27418

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr106_202_029 pdf None 660 KB 110 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
Hierarchical Model-checking for Web Application with SPIN
SPIN　ヲ　モチイタ　ウェブ　アプリケーション　ニ　オケル　カイソウベツ　モデル　ケンサ　シエン　ホウホウ
Creator
CreatorName
浜口, 優 ; ハマグチ, ユウ ; Hamaguchi, Yuu
CreatorName
吉村, 顕 ; ヨシムラ, アキラ ; Yoshimura, Akira
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Subject
モデル検査
Struts
共有資源
状態爆発
Model-checking
Shared resource
State explosion
Promela
SPIN
Abstract
ウェブアプリケーションの開発では,ユーザの誤入力である二重送信やタイムアウト発生時の動作,さらにはウェブアプリケーションの内部処理におけるデッドロックを考慮する必要がある.このため設計誤りはできる限り早期に検出することが望まれる.近年,ソフトウェア検証手法としてモデル検査が注目を集めている.しかし,モデル検査においては,状態爆発を考慮に入れた上での検証モデルの抽出や記述の難しさが問題点になっている.本稿ではStrutsを用いたウェブアプリケーション仕様を,ページ遷移を検証するモデルと内部処理を検証するモデルに階層別にモデル化するモデル検査手法を提案する.階層別に行うことにより状態爆発を回避している.また提案手法をもとにした検証用モデル生成支援ツールの試作を行った.この手法をある企業の新人研修で開発されたウェブアプリケーションをもとにした例題に適用し,手法およびツールの実用性の評価実験を行い,本手法の有効性を確かめた.
In the development of the web application, double-click actions of users, time-out and deadlock should be considered. Therefore, such design faults should be found as early as possible. Recently, the model-checking attracts attention as the effective software verification technology. However, to create effective models and describing properties have become main issues of model-checking. This paper proposes a hierarchical model-checking for the web application implemented in framework Struts. The method, thus, avoids state explosion. The method is applied to a web application developed as an exercise of an enterprise's new comers' training. The result shows that the proposed method is useful.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
106(202)
Page
29-34
Date of Issued
2006-07-28
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27418
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2006 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article