講演名 2002/10/4
WSFLの記述パターンとデザインチェッカ
中島 震,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) インターネットの本格化と,共に登場したWebサービスは他と独立に自律並行実行する実体である.利用者は既存のWebサービスを連携させることで所望の機能を得ることができる.Webサービスを組み上げるサービス・アグリゲーションに関心が集まり,Webサービスフロー記述言語が提案・公開されている.その代表例であるWSFL(Web Services Flow Language)はネット指向ワークフロー言語であり,構文的に正しくても大域的な不具合を生じる可能性を排除できない.モデル検査検証技法によってWSFL記述の大域的な振舞いを検証することができる.一方,データリンクの取り扱いや検証という観点から見た場合にWSFLの操作的な意味には問題点がある.本稿では,WSFLの仕様を分析し不具合が発生する原因を探る.WSFLの考え方にしたがった範囲内で"保守的な"拡張を検討し,WSFL記述の検証を可能にする操作的な意味を提案する.また,モデル検査検証ツールSPINについて,WSFL仕様の分析作業の中での使い方ならびに,WSFL記述チェッカのエンジンとしての利用方法を紹介する.
抄録(英) Web service is an emerging software technology to use remote services in the Internet. Each Web service is an autonomous server ready to use. As the technology becomes pervasive, some "language" to describe Web service flows is needed to combine existing services flexibly. WSFL(Web Services Flow Language), one of the languages proposed for a standard, is a net-oriented flow language. This paper proposes to use the the SPIN model-checker for the verification of descriptions written in WSFL. Since WSFL is a net-oriented specification language, any WSFL descriptions, though syntactically correct, sometimes show faulty global behaviours. Such faulty descriptions can be detected by means of the proposed method. Further, the paper reports some anomaly in the definition of the WSFL operational semantics in regard to the handling of dataflows, which was identified during the experiments on using the model-checker. The paper presents a remedy to the anomaly as well as discussions on the role of the model-checking technology for use in the behavioural analysis of Web service flows.
キーワード(和) Webサービス / ワークフロースキーマ / デッドロック解析 / モデルチェッキング
キーワード(英) Web Service / Workflow Schema / Deadlock Analysis / Model-Checking
資料番号 KBSE2002-10
発行日

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

講演論文情報詳細
申込み研究会 Knowledge-Based Software Engineering (KBSE)
本文の言語 JPN
タイトル(和) WSFLの記述パターンとデザインチェッカ
サブタイトル(和)
タイトル(英) Patterns in WSFL Descriptions and Validation Checker
サブタイトル(和)
キーワード(1)(和/英) Webサービス / Web Service
キーワード(2)(和/英) ワークフロースキーマ / Workflow Schema
キーワード(3)(和/英) デッドロック解析 / Deadlock Analysis
キーワード(4)(和/英) モデルチェッキング / Model-Checking
第 1 著者 氏名(和/英) 中島 震 / Shin NAKAJIMA
第 1 著者 所属(和/英) 法政大学:科技団さきがけ21
Hosei University:PRESTO, JST
発表年月日 2002/10/4
資料番号 KBSE2002-10
巻番号(vol) vol.102
号番号(no) 371
ページ範囲 pp.-
ページ数 6
発行日