CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 3: Webアプリケーションの画面遷移仕様のモデル検査


実施年度2004
概要 Webアプリケーションの基本設計にある画面遷移仕様とプログラム処理の流れ を表わすフローチャート間の整合性をモデル検査で検証する方法を提案し、実 際の事務処理アプリケーションの仕様書に対して適用実験を行った。
担当者 崔銀惠、河本貴則、渡邊宏
班名 数理的手法研究班
寄与 企業A社との共同研究、文科省科振費
関連する事例 事例 4:Webアプリケーションのクラス設計仕様に対するモデル化と検証

題材

領域 Webアプリケーション、業務システム
題材の詳細
約100の機能を持つ業務系Webアプリケーションの基本設計仕様と詳細設計仕様。
基本設計仕様に含まれていた画面遷移図、詳細設計仕様に含まれていたUMLの
活動図(Activity Diagram)。
形態 仕様書
言語 日本語
規模 2モジュール/数10モジュール。 モジュール1は画面遷移図で9状態、UML活動図で66状態。 モジュール2は画面遷移図で9状態、UML活動図で56状態。
題材の情報源 企業A社の業務系Webアプリケーションの仕様書

検証のデータ

目的
仕様書の不備を発見する方法の適用実験を行う。
検証内容
画面遷移図の遷移関係をもとに次の二種類の論理式だけ作成して検査する。
1. EF (x ∧ EX y)
2. AG (x → AX (x∨y1∨...∨yn))
ただしy,y1,..,yn はxの次のノード
結果
二つのモジュールへの適用実験では、合計19件の不具合を発見できた。
不具合内容は、画面遷移の欠落や遷移先の誤りなど。
検証手法 モデル検査
モデル化法 手動
使用ツール NuSMV
スケジュール、
労力、時間など
1モジュールあたり3時間程度。
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS-2005-002, 画面遷移仕様のモデル検査, 崔銀惠、河本貴則、渡邊宏, http://unit.aist.go.jp/cvs/tr-data/ps05-002.pdf
論文発表 画面遷移仕様のモデル検査,崔 銀恵、河本 貴則、渡邊 宏,日本ソフトウェ ア科学会論文誌「コンピュータソフトウェア」,22-3,pp.146-153、2005/07
口頭発表 画面遷移仕様のモデル検査,渡邊 宏、崔 銀恵、河本 貴則, 第十五回 ALGI (代数,論理,幾何と情報科学研究集会),兵庫県神戸市 神戸大学、 2004/09/15
知的財産
その他

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