SPINを用いたウェブアプリケーションにおける 階層別モデル検査支援方法 大阪大学 大学院情報科学研究科 コンピュータサイエンス専攻 浜口 優 吉村 顕 岡野 浩三 楠本 真二 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 研究の背景と目的 研究の背景 Webアプリケーションの大規模複雑化 設計誤りを早期に漏れなく検出するのはますます困難 従来のソフトウェア開発における確認作業の問題点 人間の手作業による抜け落ちを完全に排除することは難しい – レビュー：担当者による仕様の確認作業 – 受け入れテスト：テストチームによるテストケースの設定 ソフトウェア設計の確認作業で求められること 設計誤りを迅速に検出すること – 上位仕様を対象とした検査手法の確立 モデル検査 上 位 仕 様 実装 設計誤りを漏れなく検出すること – 論理的な確認手法の確立 研究の目的 Webアプリケーション仕様を対象としたモデル検査手法の提案と評価 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 2 モデル検査 検査対象の動作が仕様通りであることを検証 デッドロック，到達不能状態の検出機能 ユーザが定義した制約（LTL等）の真偽判定 利用手順 検査対象を有限状態機械としてモデル化 検査ツールで全状態空間を迅速に探索 問題点 検証用モデル記述言語の習得が必要 状態爆発回避を考慮した抽象化には経験が必要 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 3 提案手法 問題点 システム全体をモデル化 状態爆発 提案手法 Webアプリケーションを階層別にモデル化 階層 – 画面遷移の検証 – 内部処理の検証 藤原貴之 他, ”SPINによるStrutsアプリケーションの 動作検証を目的としたモデル生成手法の提案” 利点 – 状態爆発の軽減 – モデル別に独立した検証 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 4 対象Webアプリケーションの概要 ページ遷移検証用モデル View １ User Controller ＊ １ Action MVCアーキテクチャ Model 具体的な処理 View ユーザの視点，画面 Controller ModelとViewの制御 内部処理検証用モデル ＊ Model １ ＊ Business Logic １ １ Temporary Data Database 各部の主な働き User アプリケーションの利用者 Business Logic 具体的な処理の最小単位 Action まとまりのある処理単位を構成 – Business Logicの制御 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 5 検証用モデル生成の流れ 検証用モデル生成支援ツールの作成 検証用モデルのスケルトンを出力 モデル抽出の手間を削減 抽出モデルの記述にかかる手間を緩和 支援ツールの入力 仕様の情報を含むXMLファイル Struts設定ファイル 画面定義ファイル （画面設計書等の情報から作成可能） 内部処理定義ファイル （論理設計書から作成可能） 仕様書等 （XML） 支援ツール 検証者 検証用 モデル （Promela） 制約 （LTL） ページ遷移検証用モデル 内部処理検証用モデル 検証器 （SPIN） 検証結果 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 6 検証用モデル生成の基本方針 各機能ごとに状態遷移プロセスを作成 プロセスどうしが同期することでシステムを表現 ページ遷移検証用モデル 内部処理検証用モデル ページ遷移検証用モデル Server Client User Business Logic Action Context Form JSP Client 内部処理検証用モデル Action Servlet Action Request Processor Database 図：Strutsアプリケーションの概要 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 7 ページ遷移検証用モデル 入力ファイル 画面定義ファイル 画面内にどのアクションがある のかを記述 呼び出すアクション名 – パラメータ 画面ID 画面に含まれるJSP Struts設定ファイル アクション実行後どの画面に 遷移するのかを記述 アクションの総数 各アクションの名称 処理後の遷移先 ページの枚数と名前 <screens> <screen id=“初期画面"> <jsps> <jsp file="index.jsp" /> </jsps> <actions> <action name="/menu" parameter="action=init" /> <action name="/menu" parameter="action=top" /> </actions> </screen> <screen> ･・・・・・・・・・・・・ </screen> </screens> そのページから呼び出される アクション <struts-config> <form-beans> <form-bean name=“form” type=“Form” /> </form-beans> <action-mappings> <action path=“/index" type=“Index" name=“form” scope=“request” > <forward name=“init" path=“index.jsp" /> </action> </aciton-mappings> </struts-config> アクションの名前 アクション実行後の遷移先 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 8 ページ遷移検証用モデル 出力となるモデル クライアントプロセス ユーザからの入力 ? input Viewの情報より生成 画面定義ファイル （画面設計書） – 表示画面の総数 ! view !HttpReq ユーザへ表示中画面の送信 アクションプロセス ?HttpRes サーバからの受信 Controllerの情報より生成 Struts設定ファイル – アクションの総数 – 各アクションの名称 – 処理後の遷移先 全体で６個のプロセスが同期 して実現 サーバへリクエスト送信 呼び出しを受信 ! forward ? callAction 遷移先を送信 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 9 ページ遷移検証用モデル 工夫点：特殊な状況とそのモデル表現（外乱プロセス） 購入確認画面 Submitボタン押下ミス 購入完了処理 （支払い等）の二重化 二重送信 リクエスト送信 ユーザ サーバ タイムアウト リクエスト情報の消失 参照例外発生 購入確認画面 放置 → Submit 二重送信発生時 タイムアウト発生時 !HttpReq e !HttpReq 通常時 通常時 !HttpReq ?HttpReq ?HttpReq リクエスト横取り リクエスト横取り !HttpReq 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 10 目次 研究の背景と目的 モデル検査 提案手法 対象Webアプリケーションの概要 検証用モデル生成の流れ 検証用モデル生成の基本方針 ページ遷移検証用モデル 内部処理検証用モデル 評価実験 適用実験 実験結果と考察 まとめ 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 11 内部処理検証用モデル 概要 内部処理 Model層における意味を持つまとまりある単位の処理 Actionが複数のBusiness logicの呼び出し順序を制御して処理を実現 ビジネスロジック１ 呼び出し ビジネスロジック１ 処理終了受信 !call Business１ ビジネスロジック２ 呼び出し ?return Action１ !call Business2 ?return Action2 アクション アクションから 呼び出し受信 ビジネス ロジック１ ビジネス ロジック２ ?call Business１ ?call Business２ 処理終了 送信 … … !return Action１ ?return Action2 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 12 内部処理検証用モデル 工夫点：マルチタスク環境に対応したモデル表現 内部処理は共有資源を扱うことが多い マルチタスク環境での動作検証が必要 検証したい内部処理 並列に実行させる 検証したい内部処理 資源の競合を起こす可能性のある内部処理 ビジネス ロジック 共有ロック 読み込み ロック開始と解除 タイミングのミス 資源の競合の可能性 のある内部処理 排他ロック 書き込み 資源の競合が起きるかどうかを検証できるモデル を作成可能（デッドロックを早期に発見可） ビジネス ロジック デッドロック 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 13 内部処理検証用モデル 生成支援ツールの入出力 入力：内部処理定義ファイル 内部処理内のAction Actionの呼び出すBusiness logic Business logic のアクセスする共有資源 出力：検証モデル 追加記述 共有資源を設定 呼び出すビジネス <actions resource=“1"> <action name=“ActionA"> ロジックを定義 アクションを定義 <business-objects> <business name="businessA" order="0"> <dao name="daoA" resource=“1" order="0" type=“read" /> </business> </business-objects> ビジネスロジックの <action name=“ActionB”> 行う処理を定義 <business-objects> <business name="businessB" order="0"> <dao name="daoB" resource=“1" order="0" type=“write" /> </business> 並列に実行する </business-objects> </action> 内部処理を定義 </actions> 共有ロック 読み込み 追加記述 共有資源 排他ロック 書き込み 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 14 評価実験 実際のWebアプリケーションに適用 企業の新人研修で開発されたWebアプリケーション ショッピングサイト Webアプリケーションのページ遷移 二重送信 タイムアウト Webアプリケーション内の一部の内部処理 購入確認処理 検索処理 調べたいこと 動作誤りの検証が可能かどうか？ まとまった処理の検証が可能かどうか？ 評価項目 検証コスト（検証時間，メモリ使用量） 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 15 適用実験：ページ遷移 新人研修で開発されたWebアプリケーション ショッピングサイト 画面遷移書，画面設計書がある 黄色ノードへはメニューフレームより全画面から遷移可能 カート詳細 商品詳細 商品リスト トップ 購入 購入確認 購入完了 検証例としてここに着目 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 16 実験結果と考察：ページ遷移 実験環境 CPU : 3GHz，メモリ: 2GByte，検証器 : SPIN OS : Windows XP Professional Edition 外乱なし 二重送信 タイムアウト 二重送信と タイムアウト 状態数 約600万 約2億 約2700万 状態爆発 メモリ（MB） 781 1989 1046 - 検証時間 30分 15時間 2時間 - 検証結果 Valid Valid Valid - 動作誤りが存在する場合の検証時間は数秒 問題となる事象を個別に検証することで状態爆発を回避 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 17 適用実験：購入確認処理 処理内容 共有資源内の注文番号を取得し、新規注文番号の書き込みを行う ２～６個の購入確処理を並列に実行 検査項目 全ての購入確認処理が正常に終了し、共有資源に値を書き込んでいる 共有ロック掛けて 読み込み 購入確認処理A ビジネスロジック排他ロック掛けて 呼び出し 書き込み 図：作成した検証モデル 購入確認処理Aと 同じ処理 共有資源 購入確認処理B ランダムに共有ロック、 排他ロックを掛ける 外乱プロセス （外部から管理者の 共有資源へのアクセスを想定） 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 18 実験結果と考察：内部処理 実験環境 CPU : 3GHz，メモリ: 2GByte，検証器 : SPIN OS : Windows XP Professional Edition 購入確認処理 アクション数 ２ アクション数 ３～６ 状態数 約120万 状態爆発 メモリ（MB） 705 検証時間 検証結果 検索処理 アクション数 ２ アクション数 ３～６ 状態数 約200万 状態爆発 - メモリ（MB） 957 - 10秒 - 検証時間 24秒 - Valid - 検証結果 Valid - 動作誤りが存在する場合の検証時間は数秒 同時に実行できるアクション数は２つのみ 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 19 実験結果と考察：内部処理（外乱プロセスなし） 実験環境 CPU : 1.69GHz，メモリ: 512MByte，検証器 : SPIN OS : Windows XP Home Edition 検索処理 購入確認処理 アクション数 ２ アクション数 ３ アクション数 ４～６ アクション数 ２ アクション数 ３～６ 状態数 約1万 約180万 状態爆発 状態数 約1万5千 状態爆発 メモリ（MB） 160 160 - メモリ（MB） 160 - 検証時間 約1秒 25秒 - 検証時間 約1秒 - 検証結果 Valid Valid - 検証結果 Valid - 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 20 モデル生成と検証の手間 ページ遷移検証：約３日 モデル作成 画面定義ファイル記述 追加記述 検証式（LTL式） 内部処理検証：約１日 モデル作成 内部処理定義ファイル記述 – 購入確認処理 – 検索処理 追加記述 モデル内の詳細記述 検証式（LTL式） 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 21 まとめ Webアプリケーション検証用モデル生成支援手法 外乱の導入によって異常発生時の動作設計支援 並列実行によるマルチタスク環境での内部処理動作設計支援 検証用コードの自動生成ツール試作 モデル検査利用者の利便性向上 提案したモデルはある程度状態爆発を回避 今後の課題 より多数のプロセスを用いたモデルの状態爆発の克服 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 22 2006/8/4 Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University 23
© Copyright 2024 ExpyDoc
