講演名 2009-05-22
形式的手法によるWebアプリケーションのモデル化と検証
本間 圭, 高橋 薫, 富樫 敦,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) オンライントランザクションを扱うWebアプリケーションの数は年々増加している.しかし,Webアプリケーションの設計に対する正常稼働の確認は人手で行っているのが現状である.本稿では,Webアプリケーションの設計で利用される画面遷移図とアプリケーション内部の状態を2つの有限状態オートマトンとして,Webアプリケーションをモデル化する手法を提案する.また,モデル化した設計を用いて形式的手法によるモデル検査を実施したのでその事例を合わせて報告する.
抄録(英) The number of web applications handling online transaction is increasing, but verification of the correctness of the web application design has been done manually. This paper proposes a method for modeling web applications using two finite-state automata, i.e., an automaton of screen transition and an automaton of transition describing internal state of application. An example web application is modeled by the proposed method and checked using the model checker SPIN.
キーワード(和) 形式的手法 / オートマトン / モデル検査 / SPIN
キーワード(英) formal method / automata / model checking / SPIN
資料番号 SS2009-8,KBSE2009-8
発行日

研究会情報
研究会 KBSE
開催期間 2009/5/14(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Knowledge-Based Software Engineering (KBSE)
本文の言語 JPN
タイトル(和) 形式的手法によるWebアプリケーションのモデル化と検証
サブタイトル(和)
タイトル(英) Modeling and Verification of Web Applications Using Formal Approach
サブタイトル(和)
キーワード(1)(和/英) 形式的手法 / formal method
キーワード(2)(和/英) オートマトン / automata
キーワード(3)(和/英) モデル検査 / model checking
キーワード(4)(和/英) SPIN / SPIN
第 1 著者 氏名(和/英) 本間 圭 / Kei HOMMA
第 1 著者 所属(和/英) 宮城大学大学院事業構想学研究科
Graduate School of Project Design, Miyagi University
第 2 著者 氏名(和/英) 高橋 薫 / Kaoru TAKAHASHI
第 2 著者 所属(和/英) 仙台電波工業高等専門学校
Sendai National College of Technology
第 3 著者 氏名(和/英) 富樫 敦 / Atsushi TOGASHI
第 3 著者 所属(和/英) 宮城大学大学院事業構想学研究科
Graduate School of Project Design, Miyagi University
発表年月日 2009-05-22
資料番号 SS2009-8,KBSE2009-8
巻番号(vol) vol.109
号番号(no) 41
ページ範囲 pp.-
ページ数 6
発行日