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

浜口, 優; 吉村, 顕; 岡野, 浩三; 楠本, 真二

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

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

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

アクセス数:462件（2025-10-24 14:07 集計）

固定URL: https://hdl.handle.net/11094/27418

閲覧可能ファイル

ファイル	フォーマット	利用条件	サイズ	閲覧回数	利用開始日	説明	information
itr106_202_029	pdf	なし	660 KB	114	2014.04.11

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル	SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
	Hierarchical Model-checking for Web Application with SPIN
	SPIN　ヲ　モチイタ　ウェブ　アプリケーション　ニ　オケル　カイソウベツ　モデル　ケンサ　シエン　ホウホウ
著者	著者名浜口, 優 ; ハマグチ, ユウ ; Hamaguchi, Yuu
	著者名吉村, 顕 ; ヨシムラ, アキラ ; Yoshimura, Akira
	NRID 1000070252632 1000070252632 著者名岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
	NRID 1000030234438 1000030234438 researchmap permalink read0013799 read0013799 Scopus Author ID 7102741360 7102741360 著者名楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
キーワード等	モデル検査
	Struts
	共有資源
	状態爆発
	Model-checking
	Shared resource
	State explosion
	Promela
	SPIN
抄録	ウェブアプリケーションの開発では,ユーザの誤入力である二重送信やタイムアウト発生時の動作,さらにはウェブアプリケーションの内部処理におけるデッドロックを考慮する必要がある.このため設計誤りはできる限り早期に検出することが望まれる.近年,ソフトウェア検証手法としてモデル検査が注目を集めている.しかし,モデル検査においては,状態爆発を考慮に入れた上での検証モデルの抽出や記述の難しさが問題点になっている.本稿では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.
出版者	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻(号)	106(202)
ページ	29-34
刊行年月	2006-07-28
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27418
PISSN	09135685
NCID	AN10013287
アクセス権	open access
権利情報	Copyright © 2006 IEICE
権利情報	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
DCMI資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス. 2006, 106(202), p. 29-34
DC.title	SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
	Hierarchical Model-checking for Web Application with SPIN
	SPIN　ヲ　モチイタ　ウェブ　アプリケーション　ニ　オケル　カイソウベツ　モデル　ケンサ　シエン　ホウホウ
DC.creator	浜口, 優
	ハマグチ, ユウ
	Hamaguchi, Yuu
	吉村, 顕
	ヨシムラ, アキラ
	Yoshimura, Akira
	岡野, 浩三
	オカノ, コウゾウ
	Okano, Kozo
	楠本, 真二
	クスモト, シンジ
	Kusumoto, Shinji
DC.publisher	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
DC.language' scheme='DCTERMS.RFC1766	日本語
DC.type' scheme='DCTERMS.DCMIType	text
DCTERMS.issued' scheme='DCTERMS.W3CDTF	2006-07-28
DC.subject	モデル検査
	Struts
	共有資源
	状態爆発
	Model-checking
	Shared resource
	State explosion
	Promela
	SPIN
DCTERMS.abstract	ウェブアプリケーションの開発では,ユーザの誤入力である二重送信やタイムアウト発生時の動作,さらにはウェブアプリケーションの内部処理におけるデッドロックを考慮する必要がある.このため設計誤りはできる限り早期に検出することが望まれる.近年,ソフトウェア検証手法としてモデル検査が注目を集めている.しかし,モデル検査においては,状態爆発を考慮に入れた上での検証モデルの抽出や記述の難しさが問題点になっている.本稿ではStrutsを用いたウェブアプリケーション仕様を,ページ遷移を検証するモデルと内部処理を検証するモデルに階層別にモデル化するモデル検査手法を提案する.階層別に行うことにより状態爆発を回避している.また提案手法をもとにした検証用モデル生成支援ツールの試作を行った.この手法をある企業の新人研修で開発されたウェブアプリケーションをもとにした例題に適用し,手法およびツールの実用性の評価実験を行い,本手法の有効性を確かめた.
DCTERMS.abstract	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.
DC.rights	Copyright © 2006 IEICE
DC.rights	本文データはCiNiiから複製したものである
DC.format	27418
citation_title	SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
citation_author	浜口, 優
	吉村, 顕
	岡野, 浩三
	楠本, 真二
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2006-07-28
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	106
citation_issue	202
citation_firstpage	29
citation_lastpage	34
citation_public_url	https://hdl.handle.net/11094/27418

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

閲覧可能ファイル

論文情報

論文詳細を表示