Translation pattern of BPEL process into Promela code

Ryosuke Nakashiro, Yasutaka Kamei, Naoyasu Ubayashi, Shin Nakajima, Akihito Iwai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

To verify behavioral specification of compound Web services, this paper introduces to apply model checking to Web services flows described by BPEL. Model checking is a formal method to formalize the behavior of designed system as an automaton and to analyze automatically whether or not the automaton satisfies the specification. This paper introduces translation pattern to convert a BPEL process to Promela code (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 translation pattern can automatically verify the specification except Exception handling pattern and Event handling pattern.

Original languageEnglish
Title of host publicationProceedings - Joint Conference of the 21st International Workshop on Software Measurement, IWSM 2011 and the 6th International Conference on Software Process and Product Measurement, MENSURA 2011
Pages285-290
Number of pages6
DOIs
Publication statusPublished - Dec 1 2011
EventJoint Conference of the 21st International Workshop on Software Measurement, IWSM 2011 and the 6th International Conference on Software Process and Product Measurement, MENSURA 2011 - Nara, Japan
Duration: Nov 3 2011Nov 4 2011

Publication series

NameProceedings - Joint Conference of the 21st International Workshop on Software Measurement, IWSM 2011 and the 6th International Conference on Software Process and Product Measurement, MENSURA 2011

Other

OtherJoint Conference of the 21st International Workshop on Software Measurement, IWSM 2011 and the 6th International Conference on Software Process and Product Measurement, MENSURA 2011
CountryJapan
CityNara
Period11/3/1111/4/11

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint Dive into the research topics of 'Translation pattern of BPEL process into Promela code'. Together they form a unique fingerprint.

  • Cite this

    Nakashiro, R., Kamei, Y., Ubayashi, N., Nakajima, S., & Iwai, A. (2011). Translation pattern of BPEL process into Promela code. In Proceedings - Joint Conference of the 21st International Workshop on Software Measurement, IWSM 2011 and the 6th International Conference on Software Process and Product Measurement, MENSURA 2011 (pp. 285-290). [6113074] (Proceedings - Joint Conference of the 21st International Workshop on Software Measurement, IWSM 2011 and the 6th International Conference on Software Process and Product Measurement, MENSURA 2011). https://doi.org/10.1109/IWSM-MENSURA.2011.42