Model Checking Business Processes for Web Service Compositions in mCRL2

被引：0
|
作者：
Sun, Meng [1 ]
Li, Shaodong
Ou, Yufei
机构：
[1] Peking Univ, Sch Math Sci, LMAM, Beijing 100871, Peoples R China
来源：
2014 SIXTH INTERNATIONAL CONFERENCE ON INTELLIGENT HUMAN-MACHINE SYSTEMS AND CYBERNETICS (IHMSC), VOL 2 | 2014年
关键词：
D O I：
10.1109/IHMSC.2014.151
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
BPEL has emerged as the de facto industry standard for composing web services. In this paper, we focus on a core subset of BPEL, called BPEL*, and provide a set of rules for translating BPEL* into the process algebra language mCRL2, which can be used to verify properties of BPEL processes. An employee travel arrangement example is provided to show our approach.
引用
收藏
页码：202 / 205
页数：4
相关论文
共 50 条
  • [1] Family-Based Model Checking with mCRL2
    ter Beek, Maurice H.
    de Vink, Erik P.
    Willemse, Tim A. C.
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2017, 2017, 10202 : 387 - 405
  • [2] Towards model checking executable UML specifications in mCRL2
    Hansen, Helle Hvid
    Ketema, Jeroen
    Luttik, Bas
    Mousavi, MohammadReza
    van de Pol, Jaco
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) : 83 - 90
  • [3] Family-Based Model Checking of SPL based on mCRL2
    Ben Snaiba, Ziad
    de Vink, Erik P.
    Willemse, Tim A. C.
    [J]. 21ST INTERNATIONAL SYSTEM & SOFTWARE PRODUCT LINE CONFERENCE (SPLC 2017), VOL 2, 2017, : 13 - 16
  • [4] Reo+mCRL2: A framework for model-checking dataflow in service compositions
    Kokash, Natallia
    Krause, Christian
    de Vink, Erik
    [J]. FORMAL ASPECTS OF COMPUTING, 2012, 24 (02) : 187 - 216
  • [5] Generation and Evaluation of Business Continuity Processes using Algebraic Graph Transformation and the mCRL2 Process Algebra
    Brandt, Christoph
    Hermann, Frank
    Groote, Jan Friso
    [J]. JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY, 2011, 43 (01): : 65 - 85
  • [6] An Automatic Modeling Method for Web Service Business Processes towards CPN Model Checking
    Sun, Tao
    Zuo, Kangshuai
    Zhong, Wenjie
    [J]. 2022 IEEE INTL CONF ON PARALLEL & DISTRIBUTED PROCESSING WITH APPLICATIONS, BIG DATA & CLOUD COMPUTING, SUSTAINABLE COMPUTING & COMMUNICATIONS, SOCIAL COMPUTING & NETWORKING, ISPA/BDCLOUD/SOCIALCOM/SUSTAINCOM, 2022, : 715 - 721
  • [7] Checking conformance between business processes and web service contract in service oriented applications
    Bhuiyan, Jenny
    Nepal, Surya
    Zic, John
    [J]. 2006 AUSTRALIAN SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2006, : 80 - +
  • [8] Formal Verification of an Industrial UML-like Model using mCRL2
    Stramaglia, Anna
    Keiren, Jeroen J. A.
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2022), 2022, 13487 : 86 - 102
  • [9] Model checking adaptive service compositions
    Bugliesi, M.
    Marin, A.
    Rossi, S.
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2014, 94 : 289 - 306
  • [10] A framework for model checking Web service compositions based on BPEL4WS
    Dai, Guilan
    Bai, Xiaoying
    Zhao, Chongchong
    [J]. ICEBE 2007: IEEE INTERNATIONAL CONFERENCE ON E-BUSINESS ENGINEERING, PROCEEDINGS, 2007, : 165 - +
12345