社団法人

電子情報通信学会

信学技報

                       を用いたウェブアプリケーションにおける階層別モデル検査支援方法
優Ý

浜口

顕Ý

吉村

岡野

浩三Ý

真二Ý

楠本

大阪大学 大学院情報科学研究科 〒   大阪府豊中市待兼山町         
あらまし ウェブアプリケーションの開発では ユーザの誤入力である二重送信やタイムアウト発生時の動作 さらにはウェブアプリケーションの内部処理におけるデッドロックを考慮する必要がある このため設計誤りはできる限り早期に検出することが望まれる 近年 ソフトウェア検証手法としてモデル検査が注目を集めている しかし モデル
検査においては 状態爆発を考慮に入れた上での検証モデルの抽出や記述の難しさが問題点になっている 本稿では

を用いたウェブアプリケーション仕様を ページ遷移を検証するモデルと内部処理を検証するモデルに階層別にモデル化するモデル検査手法を提案する 階層別に行うことにより状態爆発を回避している また提案手法をもとにした検証用モデル生成支援ツールの試作を行った この手法をある企業の新人研修で開発されたウェブアプリケー
ションをもとにした例題に適用し 手法およびツールの実用性の評価実験を行い 本手法の有効性を確かめた
キーワード モデル検査   

共有資源 状態爆発           Ý    Ý  Ý    Ý   ! " #"   !   $   %  & '  
 (     $   %     )                            

 



 

       




 

   







 

 

                         

 



 

 !     
      

 "              







# 



 



  $   



 



   





 



         

#





       $                %  





      まえがき

 

#

 

デル検査では上位仕様を基にシステムの動作を検証できるため 設計の正しさを上位工程で保証するための手段として有効であると考えられる 本稿では    を利用したウェブアプリ
 設計モデルに基づいたフレームワークを用いることが ケーションの動作を  および    から成る上位層
 設計モデルではウェブアプリケーションの構成要    と  から成る下位層 以下 ビジネスロジック多い  ビジ 層 に分けて捉え モデルチェッカ   を用いた自動検素をユーザの視点  システム制御部  の三つとして独立に捉える 開発フレー 証のためのモデルをそれぞれの層から生成する手法を提案する
ネスロジック  のモデル記述用言語   では 複数の状態遷移  と ムワークの  つである    では 主に の開発を支援する
プロセスが 通信用のチャネル キュー を通してデータを送受
ウェブアプリケーションの動作がページ遷移異常やデッド信する振る舞いを表現できる 上位層のモデルでは サーバの!" クライア
ロックを回避するように設計されていることは重要である モ
振る舞いを    設定ファイル   
ウェブアプリケーション開発は効率的なシステム開発のため

に

##



ントの振る舞いを画面設計書から生成した また下位層では処

View

Controller

Model

理の中心となるアクションおよびビジネスロジックの機能を仕

Context

様書から抽出し モデルを生成した さらにモデル化支援のたActionForm

めに これらのモデルをある程度まで自動的に生成するツール
る研究は $ % を用いたもの & ' など多い  はデッドロックの検出機能を持つ他 線形時相論
理 %(% を用いてより詳細な条件を検証する能力を持つ ただ

Business
Logic

User

も試作し その有用性を評価した 検証用言語への変換に関す

JSP
ClientActionServeletActionRequestProcessor

Database

しモデル検査では検証時の状態爆発を回避することが大きな課) のように重要な特性のみを抽出してモデル化する手法も数多く考案されている 検証コストを抑えるために非同期通信モデルを同期通信モデルに置き換える手法 *
もあり 本稿の提案モデルはこの手法を応用している その他
関連研究として文献 + , はウェブアプリケーション全般の設計を対象としている また文献 -  ではそれぞれ設定ファ題になっており 文献

イルの拡張によりアプリケーションの振る舞いを明示する手法

図                               

本稿の構成は以下の通りである

位層 下位層に対してそれぞれの提案するモデルとその検証方

  では各階層の検証用モデル生成支援ツールについて述べる  では提案手法の有用性を評価するための例題と実験結果について述べ  で本稿をまとめる

   

本章では

 

図

備

 の例（抜粋）アクションサーブレット：クライアントからのリクエス



ロセッサを選択し リクエストを渡す 以下 サーブレットと略   を構成する要素の中でもリクエストプロセッサ：



データベース：共有資源があり 処理の過程で主にビジ   ではリクエストプロセッサが中心的な役割を果たし!" にその動作を記述ていて 設定ファイル   
する 図  は  " という / 0 リクエストを受けた場合
0 /123 "2を持つ   タグで指定された  " アクショ
ンが呼び出され  " アクションは 4  と名づけられたア
クションフォーム 5  を利用し 処理が完了するとリクエス
トプロセッサに   という遷移情報を返すように定義されている 最後にリクエストプロセッサはその遷移情報に対応した
 "60 をクライアントに返す 提案手法では    が本質的に状態機械であることを利用する
ネスロジックからのアクセスを受ける

トを受信する リクエストの種類に応じて適切なリクエストプ¯



な処理を実行する データベースへのアクセスを伴うことが多¯    の概要を述べる

す場合があるく デッドロック等が発生しないように設計する必要がある

 設計モデルに基づいたウェブアプリケーション開発のためのフレームワークである    を利用したウェブアプリ
ケーションは次の要素から構成される¯ クライアント及び .：ユーザからの操作を受け サー
バにリクエストを送信する またサーバからのレスポンスを受
け 画面を切り替える¯  

法を述べる

 準



    では本研究に関係するフレームワーク    検証器  について述べる  では上 

モデル化の際に抽象化した部分をスタブで補う手法を提案している の構成

中心的な役割を果たす サーブレットから渡されたリクエストを受け リクエストの内容をコンテキストの適切なスコープにあるアクションフォームに保存する 既存のアクションフォー
ムがない場合は新たに生成し コンテキストの適切なスコープ
呼び出す  つの    アプリケーションについて  つ以上存在するモジュールである

に保存する また具体的な処理を実行するためのアクションを¯

アクションフォーム

¯

アクション

¯

コンテキスト：様々なデータを格納する¯

ビジネスロジック：アクションから呼び出され 具体的





 

 はモデル検査ツールである 検査したいシステムを検証
言語   を用いて状態遷移プロセスとしてモデル化し そのモデルと 線形時相論理 %(% で表現されたシステムが決して満たしてはいけない 7 を入力として与え システ
ムが取り得る全状態空間を自動で探索する 7 を満たす状態に到達してしまった場合は反例を出力する 7
を満たす状態がない場合 システムは 7 を満たさな 」は「 がいということが保証される 例えば式「成り立つならば いつか  が成り立つ」という意味の %(% 式
である
##

面に遷移するのを待つ（ 提案するモデル検査手法

   アプリケーションは  設計モデルに基づいて構
成されている この特徴を利用し ウェブアプリケーションの  から成る上位層    と振る舞いを  と 
 から成る下位層に分割してモデル化する手法を述べる

（ ） クライアント：）動作を繰り返す．

- 状態のプロセスである．ユーザからの入力を受け（），その内容をネットワークに送信

（）する．その後リクエストプロセッサから遷移情報を受け（ （ ），画面が遷移したことをユーザに知らせる）．各画面には複数のリクエスト候補が存在し，ユーザ

この手法により各層を独立してモデル検査することができ 状からの入力を受けた際にどのリクエストがサーバに送信される態数の軽減などが期待できるのかは非決定的に選択される．

  ページ遷移検証用モデル



上位層では基本的に 共有資源の確保は存在しない よって
またこの層では二重送信とタイムアウトが起こる可能性がある
よってこの章ではこの  つの外乱が非決定的に起こり得るモデルも提案している そのモデルを使用することで外乱が起こる
状況下での動作検証が可能になる 

シングルタスク環境を想定してモデル化しても差し支えない   基本モデル

（ ） ネットワーク： クライアントからリクエストを受け（ 

-），サーブレットへ送信する（



）．

（ ） サ ー ブ レット： ク ラ イ ア ン ト か ら 命 令 を 受 信 し（ 

） ，適 切 な リ ク エ ス ト プ ロ セッサ を 呼 び 出 す（  ）．

&（ ） リクエストプロセッサ： チャネルを つ持つ．一方はサーブレットからのリクエストを受信（ ）するためのもので，受けたリクエストは適切なアクションへと渡され'外乱が起きないと想定した基本モデルは 種類のプロセスがオートマトンとして同期したモデルで構成される

 このモ   の振デルはできるだけ忠実に かつ必要最低限の要素でる舞いをモデル化するという考えに基づいている

る（ ）．もう一方はアクションからの戻り値を受
信（ ）するためのものであり，戻り値に応じてクライ
アントに次画面への遷移を送信（
クションを呼び出す（（ ） ユーザ： 画面を通して入力を行い（ ），次の画





）するか，次のア）．他のモジュールにあるアクションを呼び出す場合もあるため，提案モデルではサーブレッ
トに命令を送信することでモジュール選択機能を持たせた．

'（ ） アクション：リクエストプロセッサからの呼び出しをModel- checking
forpage transition

User

受け（），遷移情報を返す（  ）．

 

外乱を持つモデル

二重送信やタイムアウト等の異常な振る舞いは ネットワー

View

クプロセスに図ワークプロセスはクライアントから受信したリクエストに対しController
actionaction& のような記述を加えて表現する このネット以下の動作を非決定的に選ぶ（  ） 二重化してサーブレットに送信（  ） 消失

action（ ） そのままサーブレットに送信
Modelbusinesslogicbusinesslogicbusiness
logic

ネットワークプロセスに外乱を加えた場合，クライアントおよ

Sharedresource図びリクエストプロセッサのモデルにも変更を加える必要がある．

Model- checkingforinternal
processing'

クライアントプロセスの変更（図 ）タイムアウトが発生した場合，クライアントプロセスではサーバ側から一定時間以上応答が無い場合には現在の状態を'

階層別モデル

ユーザに返すこととし，デッドロックを回避する（図 中のε遷
UserClientNetwork?input?view!input!view移）．またネットワークプロセスが二重送信を発生した場合，リクエストプロセッサプロセスから返されるレスポンスも二重!HttpReq !HttpReq?HttpReq

化されている．この場合，現実には二重の処理が実行された後に画面遷移し，ユーザは操作を続行できる場合が多い．従ってクライアントプロセスの受信も二重化する必要がある（図?HttpRes

RequestProcessor

Servelet?forward!CallRP?HttpReq!HttpRes

Action?callRP!callAction8）を 度行う遷移が該当）．

リクエストプロセッサプロセスの変更

二重送信が発生した場合，チャネルの長さが!forward?callAction!HttpReq

図

リクエスト受信（ 'で, の場合はデッドロックを発生する可能性がある．この状況に対処するため，
リクエストプロセッサが持つ二つのチャネルは命令を一つ分だ
け保持できるように変更した．

ページ遷移検証用モデルの各プロセス##?input

Business
logic1!HttpReq!view?HttpReq!HttpReq
1.

?HttpRes!HttpReq

DAOεε?HttpRes

2.
Get Data

3.

Action?HttpRes

4.

!HttpReq

図

Common lock5.

外乱を発生する  

Sharedresource

図

外乱を考慮した  
Business
logic2

Action!inputBusiness1?output
Business1!inputBusiness2?output
Business2

図?output
BusinessN

アクション単位の処理の検証用モデル例
Processing with possibility of
causing competition of resource

Processing that wants
to be verified?inputBusiness

Action1.

!output
Business

3.



2.
Writing

1.

DAO

3.

%(%
 に入力として与えることでページ遷移検証を行う
例は  の適用実験で示す


次に下位層の内部処理検証用モデルについて述べる 内部   アプリ
 アクションが複数のビジネスロジックの呼び出し順序を制御して処理を実現している よって以下ウェブアプ
処理とは意味を持つまとまりある単位の処理でケーションのリケーションの内部処理をアクション単位の処理と呼ぶことにする アクション単位の処理は論理設計書の内容を基にモデル

化する アクション単位の処理は多くの場合 共有資源にアクセスするので マルチタスクに対応する設計をする必要がある
以下のプロセスでアクション単位の処理を表現する







（ ） アクション：ビジネスロジックを呼び出すプロセス アクションは つ以上のビジネスロジックと交信を行い ビジネス

ロジックを呼び出す順番を決定している ビジネスロジックにパラメータを送信（  ）すると待機状態になり
ビジネスロジックからの戻り値を受信（ ）す

ると次に実行されるビジネスロジックを呼び出す よってビジネスロジックを増やすごとにプロセスの状態数は増加していく（ ） ビジネスロジック：アクションから呼び出しを受け（ ） ビジネスロジック内のデータアクセスオ



ブジェクトが共有資源にアクセスする 最後に適切な戻り値をアクションに返す（  ）

ActionProcessing with possibility of
causing competition of resource

図

このページ遷移検証用モデルと 検証したい項目を示す

  内部処理検証用モデル

Action3.

Business
logic

アクションプロセスとビジネスロジックプロセス

式をSharedresource
Business
logic

ページ遷移検証

2.
Writing2.
Reading

5.
accesses
the sharedresource

1.

DAO

DAO

4.

図

Business
logic

Business
logic

Businesslogic

マルチタスク環境を想定した検証用モデル例

多い ビジネスロジックプロセスが共有資源内のどの領域にア

クセスしているのかを表現する必要がある 複数のビジネスロ
ジックプロセスが共有資源にアクセスすると資源の競合が起こ
他ロックがある

る可能性がある 資源の競合を防ぐ機能として共有ロックと排¯

共有ロック：共有ロックされた領域は 別のプロセスが中身を参照することはできるが書き換えを行うことはできない
また複数のプロセスが同時に同じ領域に共有ロックできる

¯





排他ロック：排他ロックされた領域は 別のプロセスが
プロセスが同時に同じ領域に排他ロックできない¯ データアクセスオブジェクト 以下 9:; ：ビジネスロジックが共有資源を扱う場合 9:; を通してアクセスする
図 * はプロセスやデータ全体の流れを表したアクション単位の処理のモデル例である まずアクションがビジネスロジック
 にパラメータを送信し  ビジネスロジック  は共有資源に
共有ロックを掛けてデータを取得し  戻り値をアクションに返す   次にアクションはビジネスロジック  にパラメータを送信し - ビジネスロジック  は戻り値をアクションに返し
& このアクション単位の処理は終了している
中身を参照することも書き換えることもできない また複数の  内部処理検証

検証したいアクション単位の処理と資源の競合を起こす可能性のある別のアクション単位の処理が並列に実行されるような

 種類のプロセスは 互いのプロセスとの通信を  遷 モデルを作成する このモデルと検証したい項目を表現した%(% 式を合わせて  に読み込ませることで検証を行う こ
移のみで行うようにした これは必要最低限の要素でアクショ
うすることによりアクション単位の処理がマルチタスク環境でン単位の処理を表現するためである
仕様を満たす動作を行うかどうかを検証することが可能になる   モデルと共有資源
これら

ビジネスロジックプロセスは共有資源にアクセスすることが#-#  ¯           "  #    






 



*

画面遷移図には( 0 画面から購入完了（ 0 ）画面までのページ遷移情報が含まれている．支援ツールが出力したス



ケルトンコードを基にして，追加，修正を加えることで検証に  に識別子を付加する この識別子を

    #   +   ページ遷移の正当性検査

 !

      !  リクエストプロセッサ数 ，アクションフォーム数 ，ア

クション数

必要なモデルを記述している．各画面には支援ツールが自動的  
図  内部処理検証用モデル生成支援ツールの入力ファイル（抜粋）またページ遷移検証では基本モデルと外乱を持つモデルに対し 0 ）画面への遷）画面からのみである」である
移は購入確認（て検証をした 検証項目は「購入完了（

 

 検証用モデル生成支援ツール%(% 式で参照し検証する

内部処理の正当性検査

ウェブアプリケーションの個々のアクション単位の処理に対してモデル検査を行い その設計の正当性を評価している 検
上位層と下位層のそれぞれについて，提案手法に基づいたモ
デルを自動的に生成するツールを試作した．以下では各ツールについて簡単に述べる．

¯

   設定ファイル（   !"）および，各 . が呼び出すアクション名の情報を記述した $ %ツールの入力はファイルである．後者はツール利用の際，別途作成する必要が  で記述さある．ツールはこれらの入力内容を反映し，れたモデルを出力する．

¯

 つである

購入確認アクション：共有資源内の注文番号を取得し 新

規注文番号の書き込みを行う  ページ遷移検証用モデルの自動生成ツール

証を行ったアクション単位の処理は以下の

検索アクション：共有資源への検索とヒットした商品群のソートを行う



それぞれ資源の競合の可能性のあるアクション単位の処理として自分自身の処理のコピーを並列に実行させる 並列に実行させるアクション数は

 から ' までにした また様々な外的要因

で共有資源にロックが掛けられることも想定し ランダムに共内部処理検証用モデル生成支援ツール



有資源にロック 共有ロック 排他ロック を掛ける外乱プロセ

並列実行する複数のアクション単位の処理の情報を記述した
入力ファイルを生成支援ツールに入力として与え 出力される検証モデルのスケルトンにユーザが必要な情報を追加記述する , の入力用ファイルから図 ) のことでモデルは完成する 図

検証用モデルの基本形を得る． タグの   属性
では共有資源の個数を定義する．内部に複数の  タグを

持つことができ それぞれに  属性で名前が与えられる 各
アクションが持つビジネスロジックの数は  タグ内部の  タグの数で決まり，名前（ ）と呼び出される順は  タグを持ち 図 , の例では <  がリソース  に対して共有ロックした後，共有資源  に対して排他ロックする
振る舞いを表現している

序（ ）を指定する また共有資源を扱うビジネスロジック

 適 用 実 験スも並列に実行させることにした この環境で各アクション単位の処理が仕様を満たす動作を行うかどうかを検証した





実験結果

検証実験の計算機はペンティアム - >?@ メモリ ><A ; は =  $ であり  は A! 上で起動した ま
た表中に記述してある ; は ; 4  A を意味する   ページ遷移の正当性検査

モデル検査の結果 反例が出力された場合は適宜モデルを修

正し 再度モデル検査を行った 反例は例題全てにおいて一瞬で   で示す検証コストは全て 検証結果が 7
& 種類の出力された 表であった場合の数値である また検証には次のようなオプションを利用した．

¯¯

94 B オプションを与えない通常の検証 0B 94 よりメモリを効率よく利用できる全状態探索
この章では提案手法および試作したツールを実務規模のウェ
ブアプリケーションに適用し，検証実験を行う．また実験結果をまとめ，考察を与える．

¯

提案手法の有効性を確認するため，企業の新入社員研修で実際に開発された次のような験を行った（注 ½）¯

な時間を要する全状態探索¯  適 用 例 題=8 アプリケーションを対象に実=8 上でレコードを購入するためのアプリケーション:B  0 よりメモリを効率良く利用できるが多大¯?/ 0 B 迅速に検証を行う近似的探索<   B ?/ 0 よりさらに迅速に検証を行う

近似的探索

 

内部処理の正当性検査

ページ遷移検証と同様に モデル検査の結果 反例が出力され  - で示す検証コストは全て 検証結果が 7 であった場合の数値である 数値が記入されていない部分は状態爆発を起こしているた場合は適宜モデルを修正し 再度モデル検査を行った 反例
は例題全てにおいて一瞬で出力された 表（注 ）：ただし，検証実験の対象は開発で用いられた設計書等から生成されたモデルであり，研修で開発された最終成果物を直接検証したわけではない#&#  考察   ページ遷移の正当性検証について影響でアクション単位の処理が正常に動作しない可能性があることが確認できた

ウェブアプリケーションをアクション単位の処理でモデル化

二重送信とタイムアウトが両方発生する総合的なモデルでの検証では状態爆発が発生した．従ってシステムの様々な側面をせず 上位層 下位層全てをモデル化して先で述べたような並同時に検証することは困難であり，問題となる事象を個別にモ

列実行を行った場合 簡単なウェブアプリケーションでもすぐデル検査する必要があると言える．

に状態爆発を起こす 以上よりアプリケーション全体のモデル

 



内部処理の正当性検証について検査を行う場合 階層別モデル検査手法は有効であると考えら

検証の結果 共有 排他ロックのタイミングや外乱プロセスの

表

れる



 む す び

外乱のないモデルの検証コスト

   アプリケーションの動作検証を目的として，モデル化手法および   コードを自動生成するための支
本稿では，

!"  "#
探索状態数（百万）$% & '"  ( 





使用メモリ（$'）

$)









計算時間（秒）











援ツールを提案，実装した．提案手法により生成した上位層のモデルでは，外乱プロセスの導入によって二重送信やタイムア
ウトを表現した．下位層のモデルでは，仕様書の内容から情報

表を抽出し，必要最小限のモデルを記述した．これによりコード

外乱発生時モデルの検証コストの到達不能箇所を要求の漏れとみなすことができ，デッドロッ
!"  "#$%& '"







 $)

探索状態数（百万）使用メモリ（$'）

$)

$)

計算時間（秒）

















ラーニング株式会社毛利幸雄様，星野隆之様に深謝致します．

使用メモリ（$'）

$)





















$) $)



 



計算時間（秒）

使用メモリ（$'）

$)

$)

計算時間（秒）







謝辞





文

!" オプションでの検証コスト
購入確認アクション

アクション数

時間 +秒,

メモリ +$',

状態数

結果







約  万

-".

〜

$)

$)

$)

$)

検索アクション
アクション数

時間 +秒,

メモリ +$',

状態数

結果







約  万

-".

〜

$)

$)

$)

$)

表

'" オプションでの検証コスト
購入確認アクション
時間 +秒,

メモリ +$',

状態数

結果







約  万

-".







約  万

-".







約  万

-".







約  万

-".







約  万-".

アクション数 で述べた適用例題をご提供頂いた日本ユニシス・
献/ 0 %#" 1  2 3 4 1#455"#" 1  5/0 6 7 & 8" 4 9:1 $ . 1  # *; <=== :"  !" =   * > *  * ##* /0 6 7 & 8" 4 9:1 2< $ . 1  2 " .
?@  $" "*; %.. AB 2C* 
/0 加藤啓史* 結縁祥治* 阿草清滋4 9 に基づく AC %##" に対する振舞い動作記述の導入*; 日本ソフトウェア科学会第  回記念大会*  * 
/0 = $* DE"1  1* $ * 6 7 & 8" 4 9<# " 1"  2?)$=E%52<*; 2  !  .
<=== A 1 #< ."  1 F " #  " : 1 G* ##  * /0  ""3"4 9> "
! AC -  F  1$ .1 : 1 G*; F <  B#BC
A +AH,* ##* 
/0 $ &"B."*  '  ."B* % 2  * & "1" 4 92 #
 " .  #  C  . 1  *; 2  ! 1 1<===5%$ <   !% ".  !"    *##* 
/0 I F* : '" * 7 4 9% "B ! < " '2=EAC - *; 2   ! 1 <   !A . A.AC+AAA H,* ## * 
/0 崔銀惠* 河本貴則* 渡邊宏4 9画面遷移仕様のモデル検査*; 産業

上から順に 二重送信* タイムアウト* 両方の場合
表

プロセスを用いたモデルの状態爆発の克服である



探索状態数（百万）

探索状態数（百万）

ク発生時の状況の把握も容易になった 実用例題に適用した結果 提案手法の有用性が確認できた 今後の課題はより多数の技術総合研究所 システム検証研究センター テクニカルレポー
ト* 2* 
/ 0 崔銀惠* 渡邊宏4 9AC アプリケーションのクラス設計仕様に対するモデル化と検証*; 産業技術総合研究所 システム検証研究センター テクニカルレポート* 2* 

/

検索アクション
アクション数

時間 +秒,

メモリ +$',

状態数

結果







約  万

-".







約  万

-".







約  万

-".







約  万

-".







約  万-".

0 % ' " * : '" * I F 2C ""4 9 !  > "!  %B 1
B    "AC- *; 2  ! 1 <   !A . A. AC+AAA H,* ##* 
/ 0 藤原貴之* 岡野浩三* 楠本真二4 92< による  アプリケー
ションの動作検証を目的としたモデル生成手法の提案*; 信学技報* -  * * ##* 

#'#