背景と目的
WebアプリケーションのWebアプリケーションのクラス設計仕様に対するモデル化と検証

 Webアプリケーションの普及に伴ってその品質保証のための検証技術の重要性はますます高まってきた．
 本研究では，オブジェクト指向のWebアプリケーション設計におけるクラス設計仕様に注目したモデル化と検証法を提案する．
 クラス仕様： クラス図，メソッド仕様書
 クラス仕様の検証→ 実装に最も近い仕様を検査し，実装前に不具合発見
 ソフトウェアの設計段階の検証→ 実装後の不具合改修による手戻りを削減

独立行政法人 産業技術総合研究所
システム検証研究センター

崔 銀惠

渡邊 宏

http://unit.aist.go.jp/cvs/
JaSST’05 2005.1.24
2

1

設計仕様間の整合性

クラス仕様と画面遷移仕様の整合性とは

Webアプリケーションの設計仕様
上位仕様
下位仕様

 クラス仕様と画面遷移仕様が整合しているとは，

動作仕様：
アクティビティ図，フローチャートなど...

画面遷移仕様 条件1. 画面遷移仕様の画面遷移がクラス仕様にある．
 条件2. クラス仕様の画面遷移が画面遷移仕様にある．

ActionAB+a()+b( )クラス仕様:
クラス図，メソッド仕様

問題点
9 クラス仕様が画面遷移仕様や動作仕様を満たしていない．
9 クラス仕様の変更を画面遷移仕様や動作仕様へフィードバックしていない．

クラス仕様

画面遷移仕様

画面a

画面a

画面b

画面b

クラス仕様と他の設計仕様間の整合性検査が必要
3

クラス仕様と動作仕様の整合性とは

4

研究の概要
 クラス仕様に対する2つの検証法を提案

 クラス仕様と動作仕様が整合しているとは，

 検証1: クラス仕様 vs. 画面遷移仕様 の整合性検査

 条件1. 動作仕様の処理の流れがクラス仕様にある．

 検証2: クラス仕様 vs. 動作仕様 の整合性検査

 条件2. クラス仕様の処理の流れが動作仕様にある．
 ある企業のWebアプリケーション設計開発で用いられた設計仕様に

クラス仕様

動作仕様

処理a

処理a

処理b

処理b

処理c

処理c

提案法を適用 Java+Strutsで開発した業務処理アプリケーション
 数十個のモジュールの内の1つに関する設計仕様を検査
 上位仕様： 画面遷移図，UMLアクティビティ図 下位仕様： クラス図，メソッド仕様書
画面遷移図

アクティビティ図
クラス仕様

561

実験結果1
実験結果1 - クラス仕様と画面遷移図の整合性

実験結果2
実験結果2 - クラス仕様とアクティビティ図の整合性

クラス仕様
クラス数5
メソッド数
17

クラス仕様
画面遷移図

：
：

クラス数5
メソッド数
17

画面数4
遷移数9アクティビティ図
状態数66
遷移数83

：
：

クラス図 メソッド仕様書

クラス図 メソッド仕様書

提案検証法1

提案検証法2

検査結果 : 画面遷移に関する不整合を発見
9 画面遷移図の画面Aから画面Bへの遷移がクラス仕様にない．
9 クラス仕様の画面Cから画面Dへの遷移が画面遷移図にない．

検査結果 : 両仕様間の不整合を発見
9 クラス仕様にだけエラー画面へ遷移するところがある．
9 両仕様でボタン押下時の処理が異なる．
7

8

Webアプリケーションの例
Webアプリケーションの例

発表のながれ Webアプリケーションと設計仕様の例

予約画面

エラー画面

確認画面

完了画面

 検証法1: クラス仕様 vs. 画面遷移仕様 の整合性検査
 検証法2: クラス仕様 vs. 動作仕様 の整合性検査
 まとめ

9

画面遷移図，アクティビティ図
画面遷移図

予約画面

10

クラス仕様

アクティビティ図

クラス図

エラー画面

メソッド仕様書

Action

予約画面

確認画面

エラー
画面

クラス名

メソッド名

ReservAction

clickReserv

1. 利用者IDのチェックを行う．
1.1. 誤りがあればエラー画面へ転送する．
2. 確認画面へ転送する．

ErrorAction

clickBack

1. 予約画面へ転送する．

ConfirmAction

clickSubmit

1. 予約処理を行う．
2. 完了画面へ転送する．

clickCancel

1. 予約画面へ転送する．

FinishAction

clickBack

1. 確認画面へ転送する．

完了画面
ReservAction+clickBack( )ConfirmAction

FinishAction+clickSubmit( )+clickCancel( )

確認画面
11

ErrorAction+clickReserv( )予約ボタン押下時の処理+clickBack( )

処理内容

完了画面

122

整合性検査モデル検査

Actionクラス仕様

ReservAction

ErrorAction+clickReserv( )+clickBack( )ConfirmAction

エラー画面

確認画面

完了画面

画面
遷移図

システム
（設計仕様）

モデル

検査項目• 常に．．．である• いずれ．．．である

検査式• AG ．．．
• EF ．．．

FinishAction+clickBack( )+clickSubmit( )+clickCancel( )
クラス名

メソッド名

処理内容

ReservAction

clickReserv

1. 利用者IDのチェック．
1.1. 誤りがあればエラー画面へ転送する．
2. 確認画面へ転送する．

ErrorAction

clickBack

1. 予約画面へ転送する．

ConfirmAction

clickSubmit

1. 予約処理を行う．
2. 完了画面へ転送する．

clickCancel

1. 予約画面へ転送する．

clickBack

1. 確認画面へ転送する．

FinishAction

予約画面

アクティビティ図

モデル検査器• True• False (反例) 有限状態遷移系としてモデル化したシステムが時相論理の検査式を満たすかを全状態探索で網羅的に検査 既存のモデル検査器(UPPAAL, SMV, SPIN...)を使用して全自動的な検査が可能
 クラス仕様と画面遷移仕様，動作仕様の整合性を網羅的に検査す

 本研究では，UPPAALを使用ることは難しい．(人手によるレビューでは見落としやすい．)

 モデル：オートマトンの集まり，検査式：CTLの一部

 本研究では，モデル検査を用いた検証法を提案する．
13

14

発表のながれモデル作成： クラス仕様のモデル化

 Webアプリケーションと設計仕様の例

 クラス図とメソッド仕様書から，クラスの動的な振舞いを表すモデル（クラスモデル）を次の手順で作成する．

 検証法1: クラス仕様 vs. 画面遷移仕様 の整合性検査
 検証法2: クラス仕様 vs. 動作仕様 の整合性検査

Step 1. 個々のクラスのモデル化
 各クラスに対して，メソッド仕様書に記述された処理の流れを遷移システムとしてモデル化
Step 2. モデルの合成
 Step1で作成した遷移システムのクラス連携部分の遷移に同期のラベルをつけて並列合成
クラス呼び出し関係

 まとめ クラスモデルはクラス全体の振舞いを模擬する．

15

モデル作成例 – 1.個々のクラスのモデル化
1.個々のクラスのモデル化

16

モデル作成例 – 2.モデルの合成
2.モデルの合成
クラス全体のモデル C = C1 || C2 || C3 || C4

 例： ReservActionクラスのモデル

C1: ReservAction
C2: ErrorAction

初期状態

インスタンスが作成された状態

ReservAction+clickReserv( )確認画面へ!と?は同期して遷移する

メソッドが呼ばれた状態

メソッドclickReservの仕様書
C3: ConfirmAction

1. 利用者IDのチェックを行う．
1.1. 誤りがあればエラー画面へ転送する．
2. 確認画面へ転送する．

C4: FinishAction

確認画面のインスタンス
作成

2.
1.

1.1.
17

183

検査式作成モデル検査結果の例

 画面遷移仕様から検査式を作成する．

検査式の作成例

予約画面

 クラスモデルで作成した検査式が成り立つことを検査する．

エラー画面

6

検査式
EF (完了画面 ∨ EX 予約画面)

検査結果
False

10AG (完了画面 → AX (完了画面 ∨ 予約画面))

False

画面遷移図
確認画面

検査項目

完了画面

クラス仕様と画面遷移図の不整合発見

検査式

画面遷移図の画面 1. EF (予約画面 ∨ EX エラー画面)...
遷移がクラスモデルにある
6. EF (完了画面 ∨ EX 予約画面)

予約画面

検査式6がFalse

エラー画面

Ｘ
確認画面

クラスモデルの画 7. AG (予約画面 → AX (予約画面 ∨ エラー画面 ∨ 確認画面))...
面遷移が画面遷移
図にある
10. AG (完了画面 → AX (完了画面 ∨ 予約画面))

完了画面

検査式10がFalse + 反例

1920

発表のながれクラス仕様と動作仕様の整合性検査法
クラス仕様と動作仕様の整合性検査法

 Webアプリケーションと設計仕様の例

 検証法1: クラス仕様 vs. 画面遷移仕様 の整合性検査

 検証法2: クラス仕様 vs. 動作仕様 の整合性検査

クラスモデルCと動作仕様のモデルAを合成してモデルC||Aを作る．
モデルC||Aでデッドロック検査を行う．
 もしデッドロックがあれば不整合が見つかる．

 まとめ

C: 初期状態 → 処理1 → 処理2 → 処理1
A: 初期状態 → 処理1 → 処理2 → 初期状態

例

C: クラスモデル

A: 動作仕様のモデル

a!

a?

1b!

c!

●は現在の状態

1b?

c?

2

2

21

モデル作成例
22

モデル検査例

クラスモデルCとアクティビティ図のモデルAの合成 C || A


C1: ReservAction
A: Activity

C2: ErrorAction

入力 モデル：

A: Activity

C1: ReservAction
C2: ErrorAction

C3: ConfirmAction

C3: ConfirmAction

C4: FinishAction

23

C4: FinishAction

検査式： AG( not deadlock ) --- デッドロックがない

検査結果： False ＋ 反例

24

4

反例の具体例
クラスモデル

発表のながれアクティビティ図のモデル

 Webアプリケーションと設計仕様の例
 反例分析

 検証法1: クラス仕様 vs. 画面遷移仕様 の整合性検査→ 不整合部分特定

 検証法2: クラス仕様 vs. 動作仕様 の整合性検査

完了画面で戻るボタン押下時，アクティビティ図：予約画面を表示
クラス仕様：確認画面へ転送

 まとめ

完了画面表示

完了画面

戻るボタン押下

戻るボタン押下

予約画面表示
確認画面

デッドロック25

まとめ26

システム検証研究センターの研究活動
システム検証研究センターの研究活動

 Webアプリケーションのクラス設計仕様に対するモデル化と検証法① システム検証技術の基礎研究
 抽象化技法
 モデル検査技法 定理証明技法を提案した．
 クラス図とメソッド仕様書からクラスモデルを作成し，
 クラスモデルとモデル検査法を用いて，1) クラス仕様と画面遷移
仕様の整合性検査，2) クラス仕様と動作仕様の整合性検査を行う．

パートナー
募集中！

② システム検証の「フィールドワーク」
 企業との共同による事例研究 技術者向けモデル検査研修コースの開発・実施

 実際のWebアプリケーションの設計仕様に対して適用実験を行い，いくつかの不具合を発見した．

受講者
募集中♪

 今後の課題 データフローを考慮した整合性検査
 ソースコードの検証27

28

システム検証研究センター
 ホームページ

http://unit.aist.go.jp/cvs/

 Eメイルinformatics-inquiry@m.aist.go.jp

 活動拠点 千里中央（大阪府豊中市）
 尼崎（兵庫県尼崎市）
 つくば
 臨海副都心（お台場）29

5