講演抄録/キーワード |
講演名 |
2009-05-22 10:00
形式的手法によるWebアプリケーションのモデル化と検証 ○本間 圭(宮城大)・高橋 薫(仙台電波高専)・富樫 敦(宮城大) SS2009-8 KBSE2009-8 |
抄録 |
(和) |
オンライントランザクションを扱う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 / / / / |
文献情報 |
信学技報, vol. 109, no. 40, SS2009-8, pp. 43-48, 2009年5月. |
資料番号 |
SS2009-8 |
発行日 |
2009-05-14 (SS, KBSE) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2009-8 KBSE2009-8 |