| 講演名 | 2011-11-11 UMLモデルからの変換によるWebアプリケーションの形式検証 大須賀 隆彦, 小野 康一, 深澤 良彰, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | モデル検査法がアプリケーションソフトウェアの形式検証のために適用されつつある.ソフトウェア開発の上流工程ではモデルを開発成果物とすることが多く,その成果物としてUMLが普及している.UMLのモデルを形式検証に活用するために,モデルから検証可能なオートマトンへと変換する手法が提案されている.我々は,WebアプリケーションのUMLモデルを,検証可能なオートマトンへ変換する手法を提案する.従来手法では,オートマトン生成のための情報をモデルに付加していたが,本手法ではWebアプリケーションモデリング以外の情報をモデルの前提としない.モデリング対象は携帯電話向けのWebアプリケーションとし,検証条件はセッションに関するセキュリティ脆弱性の不存在とした. |
| 抄録(英) | Model checking techniques are being applied to application software for formal verifications. Regarded as results of development, especially UML models are spread as it. To utilize UML models for formal verification, a method for transforming UML models to automata is already proposed. We propose a method for transforming UML models of Web applications to automata. Although relevant study needs to supplement the information for generating automata, our method doesn't require any information except for that of UML modeling. We apply this method to Web applications for mobile phone, and set a verification condition as nonexistence of vulnerable security flaw concerned with session management. |
| キーワード(和) | Webアプリケーション / 形式検証 / モデル検査 / UML |
| キーワード(英) | Web Applications / Formal Methods / Model Checking Techniques / UML |
| 資料番号 | KBSE2011-49 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2011/11/3(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | UMLモデルからの変換によるWebアプリケーションの形式検証 |
| サブタイトル（和） | |
| タイトル（英） | A Formal Verification Method by Transforming UML Models of Web Applications |
| サブタイトル（和） | |
| キーワード(1)（和/英） | Webアプリケーション / Web Applications |
| キーワード(2)（和/英） | 形式検証 / Formal Methods |
| キーワード(3)（和/英） | モデル検査 / Model Checking Techniques |
| キーワード(4)（和/英） | UML / UML |
| 第 1 著者 氏名（和/英） | 大須賀 隆彦 / Takahiko OHSUGA |
| 第 1 著者 所属（和/英） | 早稲田大学大学院基幹理工学研究科情報理工学専攻 Graduate School of Fundamental Science and Engineering, Waseda University |
| 第 2 著者 氏名（和/英） | 小野 康一 / Kouichi ONO |
| 第 2 著者 所属（和/英） | 日本アイ・ビー・エム株式会社東京基礎研究所 IBM Research Tokyo, IBM Japan Ltd. |
| 第 3 著者 氏名（和/英） | 深澤 良彰 / Yoshiaki FUKAZAWA |
| 第 3 著者 所属（和/英） | 早稲田大学大学院基幹理工学研究科情報理工学専攻 Graduate School of Fundamental Science and Engineering, Waseda University |
| 発表年月日 | 2011-11-11 |
| 資料番号 | KBSE2011-49 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | 282 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |