CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 4: Webアプリケーションのクラス設計仕様に対するモデル化と検証


実施年度2004
概要 Webアプリケーションのクラス設計仕様に対するモデル化と検証手法を提案し、 実際の事務処理アプリケーションの仕様書に対して適用実験を行った。
担当者 崔銀惠、渡邊宏
班名 数理的手法研究班
寄与 企業A社との共同研究、文科省科振費
関連する事例 事例 3:Webアプリケーションの画面遷移仕様のモデル検査

題材

領域 Webアプリケーション、業務システム
題材の詳細
詳細設計仕様に含まれるクラス図とメソッド定義書からなるクラス設計仕様、
詳細設計仕様に含まれるUMLのアクテビティ図
基本設計仕様に含まれる画面遷移図

適用実験を行なったのは、約100の機能を持つ業務系Webアプリケーションの基
本設計仕様と詳細設計仕様。
(実装はStrutsのフレームワークを用いてJava言語で開発されていた。)
形態 仕様書
言語 日本語
規模 1モジュール/数10モジュールで、5つのクラスからなる部分。 モジュール1は画面遷移図で9状態、UML活動図で66状態。
題材の情報源 企業A社の業務系Webアプリケーションの仕様書

検証のデータ

目的
仕様書の不備を見つける方法の適用実験を行う。
検証内容
クラス仕様(クラス図とメソッド定義書)から作成するクラスの振舞いを表わす
状態遷移系であるクラスモデルを作成し、次の二種類の検証をおこなった。
・ クラスモデルと画面遷移仕様との整合性検査。
・ クラスモデルとアクテビティ図の間の整合性検査。
結果
クラス仕様と画面遷移仕様との間の不整合、クラス仕様とアクテビティ図の間
の不整合が見つかった。例えば、クラス仕様と活動図で画面遷移先が一致して
いない、アクテビティ図の記述漏れなど。
検証手法 モデル検査、モデル作成
モデル化法 手動
使用ツール UPPAAL
スケジュール、
労力、時間など
1モジュールあたり1日程度。
備考 クラスモデルと画面遷移図との整合性検査は、「画面遷移仕様のモデル検査」 を適用した。

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS-2005-003, Web アプリケーションのクラス設計仕様に対するモデル化と検 証, 崔銀惠、渡邊宏, http://unit.aist.go.jp/cvs/tr-data/ps05-003.pdf
論文発表 Webアプリケーションのクラス設計仕様に対するモデル化と検証, 崔 銀惠、渡邊 宏, ソフトウェアテストシンポジウム2005予稿集,1-1,pp.90-97、2005/01
Model Checking Class Specifications for Web Applications, 崔 銀惠、渡邊 宏, Proc. of the twelfth Asia-Pacific Software Engineering Conference, IEEE,pp.67-75、2005/12
口頭発表 Webアプリケーションのクラス設計仕様に対するモデル化と検証, 崔 銀惠、渡邊 宏, ソフトウェアテストシンポジウム,東京コンファレンスセンター品川、 2005/01/24
Model Checking Class Specifications for Web Applications, 崔 銀惠、渡邊 宏, The twelfth Asia-Pacific Software Engineering Conference,TAIPEI, TAIWAN、2005/12/15
知的財産
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.