SPINを用いたウェブアプリケーションにおける 階層別モデル検査支援方法 大阪大学　大学院情報科学研究科 コンピュータサイエンス専攻 浜口 優　吉村 顕　岡野 浩三　楠本 真二

研究の背景と目的 研究の背景 研究の目的 Webアプリケーションの大規模複雑化 従来のソフトウェア開発における確認作業の問題点 設計誤りを早期に漏れなく検出するのはますます困難 従来のソフトウェア開発における確認作業の問題点 人間の手作業による抜け落ちを完全に排除することは難しい レビュー：担当者による仕様の確認作業 受け入れテスト：テストチームによるテストケースの設定 ソフトウェア設計の確認作業で求められること 設計誤りを迅速に検出すること 上位仕様を対象とした検査手法の確立 設計誤りを漏れなく検出すること 論理的な確認手法の確立 研究の目的 Webアプリケーション仕様を対象としたモデル検査手法の提案と評価 モデル検査 上位仕様 実装 現在、ウェブアプリケーションは大規模複雑化しています。設計誤りを早期に 漏れなく検出するのはますます困難になってきています。また、従来のソフトウェア 開発の確認作業であるレビューや、受け入れテストは人間の手作業であり、 設計誤りを漏れなく完全に見つけることは難しいです。ソフトウェア設計の 確認作業に求められることは設計誤りを迅速に漏れなく検出することで、 上位仕様を対象とした論理的な検査手法の確立が必要だと考えます。 よって我々はモデル検査に着目しました。研究の目的は ウェブアプリケーション仕様を対象としたモデル検査手法 の提案と評価です。 2006/8/4

モデル検査 問題点 検査対象の動作が仕様通りであることを検証 利用手順 デッドロック，到達不能状態の検出機能 ユーザが定義した制約（LTL等）の真偽判定 利用手順 検査対象を有限状態機械としてモデル化 検査ツールで全状態空間を迅速に探索 問題点 検証用モデル記述言語の習得が必要 状態爆発回避を考慮した抽象化には経験が必要 モデル検査について簡単に説明します。モデル検査とは検査対象の動作 が仕様通りであることを検証することで、デッドロックの検出やユーザが 定義した制約の真偽判定を行うことができます。 検査対象を有限状態機械にモデル化し、検査ツールで全状態空間を迅速に 探索します。問題点は検証用モデル記述言語の習得や状態爆発回避を考慮 した抽象化の困難さです。 2006/8/4

提案手法 問題点 提案手法 システム全体をモデル化 状態爆発 Webアプリケーションを階層別にモデル化 階層 利点 画面遷移の検証 内部処理の検証 利点 状態爆発の軽減 モデル別に独立した検証 藤原貴之 他, ”SPINによるStrutsアプリケーションの 動作検証を目的としたモデル生成手法の提案” 今回検証の対象とするウェブアプリケーション仕様をモデル化する際、 先程の状態爆発が問題になります。システム全体をモデル化すると 簡単に状態爆発になることが予想されます。 今回我々はこれを解決できないかと考えました。そして ウェブアプリケーションを階層別にモデル化することを 考案しました。画面遷移用、内部処理用と分けることで 状態爆発の軽減やモデル別に独立した検証が可能になります。 画面遷移検証に関しては以前この学会で発表された藤原さん の研究を利用しています。 2006/8/4

対象Webアプリケーションの概要 MVCアーキテクチャ 各部の主な働き User Business Logic Action User ページ遷移検証用モデル 内部処理検証用モデル View Controller Model ＊ Temporary Data １ １ ＊ １ ＊ User Action Business　Logic Database １ １ MVCアーキテクチャ Model 具体的な処理 View ユーザの視点，画面 Controller ModelとViewの制御 各部の主な働き User アプリケーションの利用者 Business Logic 具体的な処理の最小単位 Action まとまりのある処理単位を構成 Business Logicの制御 検査の対象とするウェブアプリケーションはフレームワークStrutsを利用し、 MVCアーキテクチャに基づくものとします。MVCアーキテクチャには ユーザの視点、画面を扱うView、具体的な処理を扱うModel、 ModelとViewを制御するControllerがあります。図は各部の主な働きを 表しています。Userはアプリケーションの利用者を表しています。 Business Logicは具体的な処理の最小単位を表していて、 データベースなどにアクセスします。Actionはまとまりのある処理単位を Business Logicの制御を行うことで構成します。今回我々はこのMVCを ２つの階層、ページ遷移検証用モデルと内部処理検証用モデル に分けてモデル化することにしました。 2006/8/4

検証用モデル生成の流れ 検証用モデル生成支援ツールの作成 支援ツールの入力 仕様書等 （XML） 検証用 モデル （Promela） 検証用モデルのスケルトンを出力 モデル抽出の手間を削減 抽出モデルの記述にかかる手間を緩和 支援ツールの入力 仕様の情報を含むXMLファイル Struts設定ファイル 画面定義ファイル　（画面設計書等の情報から作成可能） 内部処理定義ファイル　（論理設計書から作成可能） ページ遷移検証用モデル 内部処理検証用モデル 仕様書等 （XML） 検証用 モデル （Promela） 支援ツール 検証器 （SPIN） 検証には著名なモデル検査ツールSPINを使用しました。検証の流れは、 検証者が検証用モデルと検証したい項目を記述し、SPINに読む込むこと で検証結果を得ます。今回我々はこの検証用モデル記述を支援するツール を試作しました。検証用モデルのスケルトンを出力することで、 モデルの抽出や抽出モデルの記述に掛かる手間を緩和します。 支援ツールの入力は仕様の情報を含むXMLファイルで、 ページ遷移検証用モデルの入力はStruts設定ファイルと画面設計書等 の情報から作成可能な画面定義ファイルとし、 内部処理検証用モデルは論理設計書から作成可能な内部処理定義ファイルと しました。 制約 （LTL） 検証者 検証結果 2006/8/4

検証用モデル生成の基本方針 各機能ごとに状態遷移プロセスを作成 プロセスどうしが同期することでシステムを表現 Client Server ページ遷移検証用モデル 内部処理検証用モデル ページ遷移検証用モデル 内部処理検証用モデル Client Server Context Business Logic Action Form User Action 検証用モデルはページ遷移検証用モデルも内部処理検証用モデルも状態遷移 プロセスで表現します。下の図は先程のMVCモデルをより詳細にしたものですが、 これらの機能ごとに状態遷移プロセスを作成します。プロセスどうしが同期する ことで各モデルが実現されています。 JSP Client Action Servlet Request Processor Database 図：Strutsアプリケーションの概要 2006/8/4

ページ遷移検証用モデル 入力ファイル 画面定義ファイル Struts設定ファイル 画面内にどのアクションがあるのかを記述 呼び出すアクション名 パラメータ 画面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> ･・・・・・・・・・・・・ </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> アクションの名前 ページ遷移検証用モデルについて紹介していきます。ページ遷移検証用モデルの 入力ファイルは以下の２つを用います。画面定義ファイルは画面設計書から作成し、 次のような仕様になっています。このファイルには画面内にどのアクションが あるのかという情報が含まれます。呼び出すアクションプロセスや パラメータ、画面IDなどを入力とします。 Struts設定ファイルにはアクション実行後にどの画面に遷移するのかという情報 が含まれます。呼び出すアクションの総数やアクションの名称、 アクションの処理後の遷移先などの情報を入力とします。 アクション実行後の遷移先 2006/8/4

ページ遷移検証用モデル 出力となるモデル クライアントプロセス アクションプロセス 全体で６個のプロセスが同期して実現 Viewの情報より生成 画面定義ファイル （画面設計書） 表示画面の総数 ユーザからの入力 サーバへリクエスト送信 ? input ! view !HttpReq ユーザへ表示中画面の送信 アクションプロセス Controllerの情報より生成 Struts設定ファイル アクションの総数 各アクションの名称 処理後の遷移先 ?HttpRes サーバからの受信 呼び出しを受信 ページ遷移検証用モデルの概要を説明します。先程の画面定義ファイルやStruts 設定ファイルから全体で６種類のオートマトンが同期してページ遷移検証用 モデルは表現されます。例えばクライアントプロセスは４つの状態を持ち、 ユーザプロセスから入力を受信すると別のプロセスにリクエストを送信します。 アクションプロセスはリクエストから適切な遷移情報を返し、クライアント プロセスに遷移情報を送信します。クライアントプロセスは遷移画面情報を 受け取り表示画面の変更を行うという仕組みになっています。 ! forward ? callAction 全体で６個のプロセスが同期して実現 遷移先を送信 2006/8/4

ページ遷移検証用モデル 工夫点：特殊な状況とそのモデル表現（外乱プロセス） 購入確認画面 Submitボタン押下ミス 購入完了処理 （支払い等）の二重化 二重送信 リクエスト送信 ユーザ サーバ タイムアウト リクエスト情報の消失 参照例外発生 購入確認画面 放置 → Submit 二重送信発生時 タイムアウト発生時 !HttpReq また実際のウェブアプリケーションには二重送信やタイムアウトなどの外乱も 発生します。よってこのページ遷移検証用モデルでは外乱プロセスを導入する ことにより、これらの外乱が起こりうる状況での画面遷移検証を可能にしました。 外乱プロセスは先程のクライアントプロセスがサーバに送るリクエストを横取りし、 非決定的に二重送信やタイムアウトを発生します。二重送信の場合はサーバに リクエストを２度送るようにしています。タイムアウトのときはリクエストを 消失させています。 !HttpReq 通常時 通常時 e !HttpReq ?HttpReq ?HttpReq リクエスト横取り リクエスト横取り !HttpReq 2006/8/4

目次 研究の背景と目的 モデル検査 提案手法 対象Webアプリケーションの概要 検証用モデル生成の流れ 検証用モデル生成の基本方針 ページ遷移検証用モデル 内部処理検証用モデル 評価実験 適用実験 実験結果と考察 まとめ ここまではページ遷移検証用モデルについて述べてきましたので、 続いて内部処理検証用モデルについて紹介します。 2006/8/4

内部処理検証用モデル 概要 内部処理 … … Model層における意味を持つまとまりある単位の処理 Actionが複数のBusiness logicの呼び出し順序を制御して処理を実現 ビジネスロジック１呼び出し ビジネスロジック１ 処理終了受信 ビジネスロジック２呼び出し !call Business１ ?return Action１ !call Business2 ?return Action2 アクション アクションから 呼び出し受信 処理終了 送信 !return Action１ ?call Business１ ビジネス ロジック１ 入出力関係は後程説明します。 内部処理とはModel層における意味を持つまとまりある単位の処理のことです。 ここではアクションプロセスが複数のビジネスロジックプロセスの呼び出し 順序を制御して処理を実現します。図は１つの内部処理モデルの例です、 アクションプロセスがビジネスロジックプロセス１を呼び出します。 ビジネスロジックプロセス１はアクションプロセスからの呼び出しを受信し、 共有資源にアクセスするなどの適切な処理を行い、戻り値をアクションに 返します。ビジネスロジック１からの処理終了を受信するとアクション プロセスはビジネスロジック２を呼び出しています。アクションプロセスは 呼び出すビジネスロジックの数によって状態数が変化します。 … ?return Action2 ?call Business２ ビジネス ロジック２ … 2006/8/4

内部処理検証用モデル 工夫点：マルチタスク環境に対応したモデル表現 内部処理は共有資源を扱うことが多い マルチタスク環境での動作検証が必要 並列に実行させる 検証したい内部処理 資源の競合を起こす可能性のある内部処理 資源の競合が起きるかどうかを検証できるモデルを作成可能（デッドロックを早期に発見可） 検証したい内部処理 共有ロック 読み込み ビジネスロジック ロック開始と解除 タイミングのミス 資源の競合の可能性 のある内部処理 排他ロック 書き込み また内部処理は共有資源を扱うことが多く、マルチタスク環境での動作検証 が必要です。各ビジネスロジックの共有資源に対するロックの開始と解除の タイミングのミスなどでデッドロックの可能性があります。 このモデルでは検証したい内部処理と資源の競合を起こす可能性のある 内部処理を並列に実行することで資源の競合が起きるかどうかを検証 できるモデルを作成可能です、これによりデッドロックを早期に 発見できます。 デッドロック ビジネスロジック 2006/8/4

内部処理検証用モデル 生成支援ツールの入出力 入力：内部処理定義ファイル 内部処理内の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" /> </action> </actions> 共有ロック アクションを定義 読み込み ビジネスロジックの行う処理を定義 追加記述 共有資源 排他ロック 書き込み 内部処理検証用モデル生成支援ツールの入出力について説明します。 論理設計書から作成した内部処理定義ファイルにより、 内部処理検証用モデルのスケルトンを作成します。 内部処理定義ファイルには内部処理内のアクション、 アクションの呼び出すビジネスロジック、ビジネスロジック のアクセスする共有資源についての情報を記述します。 以下はスケルトン作成の流れを示す例です。共有資源、アクション、 呼び出すビジネスロジック、ビジネスロジックの行う簡単な処理、 アクションと並列に実行させたいアクションを定義した ファイルから以下のスケルトンが作成されます。ユーザはこの スケルトンに追加記述することになります。内部処理のモデル は自由度が高いので、ビジネスロジック内の制御文など定義 ファイルで自動生成できない部分を記述する必要があります。 共有ロックや排他ロックなども機能は提供しますが、掛ける タイミングに関してはユーザが決める必要があるようにしました。 並列に実行する 内部処理を定義 2006/8/4

評価実験 実際のWebアプリケーションに適用 調べたいこと 評価項目 企業の新人研修で開発されたWebアプリケーション ショッピングサイト Webアプリケーションのページ遷移 二重送信 タイムアウト Webアプリケーション内の一部の内部処理 購入確認処理 検索処理 調べたいこと 動作誤りの検証が可能かどうか？ まとまった処理の検証が可能かどうか？ 評価項目 検証コスト（検証時間，メモリ使用量） 実際に企業の新人研修で開発されたウェブアプリケーションの仕様に対して 評価実験を行いました。ページ遷移に関しては二重送信、タイムアウトの 起こる状況での検証も行っています。内部処理に関しては論理設計書の先頭に 記述してあった購入確認処理と検索処理に対して検証をおこなっています。 検証コストを基に動作誤りの検証が可能かどうかを調べます。 2006/8/4

適用実験：ページ遷移 新人研修で開発されたWebアプリケーション ショッピングサイト 画面遷移書，画面設計書がある 黄色ノードへはメニューフレームより全画面から遷移可能 トップ 商品リスト 商品詳細 カート詳細 購入 購入確認 購入完了 ページ遷移で検証した項目について具体的にのべます。この ウェブアプリケーションの画面遷移は次のようになっていて 今回は購入確認画面から購入完了画面への遷移が本当に行われているか どうかについて検証しました。 検証例としてここに着目 2006/8/4

実験結果と考察：ページ遷移 実験環境 動作誤りが存在する場合の検証時間は数秒 問題となる事象を個別に検証することで状態爆発を回避 CPU : 3GHz，メモリ: 2GByte，検証器 : SPIN OS : Windows XP Professional Edition 外乱なし 二重送信 タイムアウト 二重送信とタイムアウト 状態数 約600万 約2億 約2700万 状態爆発 メモリ（MB） 781 1989 1046 - 検証時間 30分 15時間 2時間 検証結果 Valid ページ遷移の実験結果は次のようになります。すべての状況において 動作誤りが存在する場合は一瞬で反例を出力しました。図の結果は動作誤り などを修正して検査項目が保証された状況での結果です。 図から二重送信とタイムアウトの両方が起こる状況では状態爆発が起こっている ことが分かります。両方の外乱が起こる状況では検証できませんでしたが、 個別に検証を行うことはできました。 動作誤りが存在する場合の検証時間は数秒 問題となる事象を個別に検証することで状態爆発を回避 2006/8/4

ランダムに共有ロック、排他ロックを掛ける 適用実験：購入確認処理 処理内容 共有資源内の注文番号を取得し、新規注文番号の書き込みを行う ２～６個の購入確処理を並列に実行 検査項目 全ての購入確認処理が正常に終了し、共有資源に値を書き込んでいる 共有ロック掛けて 読み込み 購入確認処理Aと同じ処理 購入確認処理A 共有資源 購入確認処理B ランダムに共有ロック、排他ロックを掛ける 内部処理の例についても詳しく述べます。ここでは購入確認処理 について説明します。処理内容は共有資源内の注文番号を取得し、 新規注文番号の書き込みを行うというものです。 資源の競合を起こす可能性のある処理として購入確認処理のコピー を並列に実行させます。購入確認処理の並列に実行する 個数は２から６個にしました。作成したモデルは以下のようになります。 ビジネスロジックを呼び出して、共有ロックを掛けて読み込み、 排他ロックを掛けて書き込みを行います。これと同じ処理を他のコピー は行います。またランダムに共有ロック、排他ロックを掛ける 外部からの管理者の共有資源へのアクセスを想定した 外乱プロセスも並列に実行させました。検査項目は 全ての購入確認処理が正常に終了し、共有資源に値を書き込んでいるか どうかです。検索処理の検証も同様に行いました。 ビジネスロジック 呼び出し 排他ロック掛けて 書き込み 外乱プロセス （外部から管理者の 共有資源へのアクセスを想定） 図：作成した検証モデル 2006/8/4

実験結果と考察：内部処理 実験環境 動作誤りが存在する場合の検証時間は数秒 同時に実行できるアクション数は２つのみ CPU : 3GHz，メモリ: 2GByte，検証器 : SPIN OS : Windows XP Professional Edition 購入確認処理 検索処理 アクション数 ２ ３～６ 状態数 約120万 状態爆発 メモリ（MB） 705 - 検証時間 10秒 検証結果 Valid アクション数 ２ ３～６ 状態数 約200万 状態爆発 メモリ（MB） 957 - 検証時間 24秒 検証結果 Valid 内部処理の実験結果は次のようになりました。内部処理も同様にすべての状況 において、動作誤りが存在する場合は一瞬で反例を出力しました。 図の結果は動作誤りなどを修正して検査項目が保証された状況での結果です。 図から並列に実行するアクションの数を３つ以上にすると状態爆発が起こった ことが分かります。 動作誤りが存在する場合の検証時間は数秒 同時に実行できるアクション数は２つのみ 2006/8/4

実験結果と考察：内部処理（外乱プロセスなし） 実験環境 CPU : 1.69GHz，メモリ: 512MByte，検証器 : SPIN OS : Windows XP Home Edition 検索処理 購入確認処理 アクション数 ２ ３ ４～６ 状態数 約1万 約180万 状態爆発 メモリ（MB） 160 - 検証時間 約1秒 25秒 検証結果 Valid アクション数 ２ ３～６ 状態数 約1万5千 状態爆発 メモリ（MB） 160 - 検証時間 約1秒 検証結果 Valid 外乱プロセスなしの場合の実験 も行いました。購入確認処理に関しては３つまで並列実行しても結果を 得ることができました。ただ、検索処理の方はこれでも状態爆発に なってしまいました。最初の約５千の差が響いていると考えられます。 結果から３つ以上の並列実行は困難ですが、最低２つのプロセスの 並列実行でデッドロックは検出できるので資源の競合の起こる状況での 検証で状態爆発を回避することはできました。 2006/8/4

モデル生成と検証の手間 ページ遷移検証：約３日 内部処理検証：約１日 モデル作成 追加記述 画面定義ファイル記述 検証式（LTL式） 内部処理定義ファイル記述 購入確認処理 検索処理 モデル内の詳細記述 最後にこの実験の手間について述べます。画面設計書や 論理設計書、Struts設定ファイルは事前に用意されていました。 画面定義ファイルをモデルのために記述し、検証式を追加記述 しました。個人差はありますが論理設計書の把握などで全体で ３日ほど掛かったと思います。 内部処理検証は内部処理定義ファイルをモデルのために記述し、 モデルの詳細と検証式を追加記述しました。購入確認処理と 検索処理を合わせて１日ほど掛かりました。 2006/8/4

まとめ 今後の課題 Webアプリケーション検証用モデル生成支援手法 検証用コードの自動生成ツール試作 提案したモデルはある程度状態爆発を回避 外乱の導入によって異常発生時の動作設計支援 並列実行によるマルチタスク環境での内部処理動作設計支援 検証用コードの自動生成ツール試作 モデル検査利用者の利便性向上 提案したモデルはある程度状態爆発を回避 　今後の課題 より多数のプロセスを用いたモデルの状態爆発の克服 まとめです。ウェブアプリケーション検証用モデル生成支援手法を 提案しました。外乱の導入によって異常発生時の動作設計や並列実行 によるマルチタスク環境での内部処理動作設計を支援することができます。 検証用コードのスケルトンを自動生成するツールを試作しました。 これによりモデル検査利用者の利便性を向上することができました。 評価実験から提案したモデルは状態爆発をある程度は回避することが できました。 今後の課題はより多数のプロセスを用いたモデルの状態爆発の克服だと考えます。 以上です。 2006/8/4

2006/8/4