Translation pattern of BPEL process into Promela code

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

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

2 引用 (Scopus)

抜粋

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.

元の言語英語
ホスト出版物のタイトル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
ページ285-290
ページ数6
DOI
出版物ステータス出版済み - 12 1 2011
イベント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 - Nara, 日本
継続期間: 11 3 201111 4 2011

出版物シリーズ

名前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

その他

その他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
日本
Nara
期間11/3/1111/4/11

All Science Journal Classification (ASJC) codes

  • Software

フィンガープリント Translation pattern of BPEL process into Promela code' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用

    Nakashiro, R., Kamei, Y., Ubayashi, N., Nakajima, S., & Iwai, A. (2011). Translation pattern of BPEL process into Promela code. : 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