Verification of BPEL Workflows Design using Model Checking

スポンサーリンク

概要

• 論文の詳細を見る

• The goal of this paper is to verify the behavioral specification of the Web service workflows described by BPEL (Business Process Execution Language) using SPIN model checker. Therefore, this paper introduces patterns to map from the specification to Promela (Process or Protocol Meta Language), which is a verification modeling language in SPIN model checker. The result of our case study using a parking navigation service shows that our approach can automatically verify the specification.

• 2011-06-23

著者

• NAKAJIMA Shin

  National Institute of Informatics

• UBAYASHI NAOYASU

  Kyushu Institute of Technology

• Ubayashi Naoyasu

  Kyushu University

• Nakajima Shin

  National Inst. Informatics Tokyo Jpn

• NAKASHIRO Ryosuke

  Kyushu University

• KAMEI Yasutaka

  Kyushu University

• IWAI Akihito

  DENSO CORPORATION

関連論文

• Highly Reliable Embedded Software Development Using Advanced Software Technologies(Software Engineering for Embedded Systems)
• Rodin plugin to link Event-B and SPIN (ソフトウェアサイエンス)
• ASB : A Framework for Implementing Extensible Aspect-oriented Programming Languages
• Project Management Patterns to Prevent Schedule Delay Caused by Requirement Elicitation
• Verification of BPEL Workflows Design using Model Checking
• An Extensible Aspect-Oriented Modeling Environment for Constructing Domain-Specific Languages

スポンサーリンク