Towards the formal model and verification of web service choreography description language

被引：0
|
作者：
Zhao Xiangpeng [1 ]
Yang Hongli
Qiu Zongyan
机构：
[1] Peking Univ, Sch Math, LMAM, Beijing 100871, Peoples R China
[2] Peking Univ, Sch Math, Dept Informat, Beijing 100871, Peoples R China
来源：
WEB SERVICES AND FORMAL METHODS, PROCEEDINGS | 2006年 / 4184卷
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The Web Services Choreography Description Language (WS-CDL) is a W3C specification for the description of peer-to-peer collaborations of participants from a global viewpoint. For the rigorous development and tools support for the language, the formal semantics of WS-CDL is worth investigating. This paper proposes a small language CDL as a formal model of the simplified WS-CDL, which includes important concepts related to participant roles and collaborations among them in a choreography. The formal operational semantics of CDL is given. Based on the formal model, we discuss further: 1) project a given choreography to orchestration views, which provides a basis for the implementation of the choreography by code generation; 2) translate WS-CDL to the input language of the model-checker SPIN, which allows us to automatically verify the correctness of a given choreography. An automatic translator has been implemented.
引用
收藏
页码：273 / 287
页数：15
相关论文
共 50 条
  • [21] Towards a Universal Service Description Language
    Simon, L
    Bansal, A
    Mallya, A
    Kona, S
    Gupta, G
    Hite, TD
    [J]. International Conference on Next Generation Web Services Practices, 2005, : 175 - 180
  • [22] Model-driven approach supporting formal verification for web service composition protocols
    Dumez, C.
    Bakhouya, M.
    Gaber, J.
    Wack, M.
    Lorenz, P.
    [J]. JOURNAL OF NETWORK AND COMPUTER APPLICATIONS, 2013, 36 (04) : 1102 - 1115
  • [23] Towards a Formal Verification Approach for Service Component Architecture
    Chargui, Wael
    Rouis, Taoufik Sakka
    Kmimech, Mourad
    Bhiri, Mohamed Tahar
    Sliman, Layth
    Raddaoui, Badran
    [J]. NEW TRENDS IN INTELLIGENT SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2017, 297 : 466 - 479
  • [24] A formal model for Web service composition
    Lecue, Freddy
    Leger, Alain
    [J]. LEADING THE WEB IN CONCURRENT ENGINEERING: NEXT GENERATION CONCURRENT ENGINEERING, 2006, 143 : 37 - 46
  • [25] Towards a Goal-driven Method for Web Service Choreography Validation
    Parsa, Saeed
    Amiri, Mohammad Javad
    Ebrahimifard, Amir
    Arani, Mostafa Khoramabadi
    [J]. 2016 SECOND INTERNATIONAL CONFERENCE ON WEB RESEARCH (ICWR), 2016, : 66 - 71
  • [26] A Formal Model for Compliance Verification of Service Compositions
    Groefsema, Heerko
    van Beest, Nick R. T. P.
    Aiello, Marco
    [J]. IEEE TRANSACTIONS ON SERVICES COMPUTING, 2018, 11 (03) : 466 - 479
  • [27] Semantic Web Service Composition Using Formal Verification Techniques
    Kil, Hyunyoung
    Nam, Wonhong
    [J]. COMPUTER APPLICATIONS FOR DATABASE, EDUCATION, AND UBIQUITOUS COMPUTING, 2012, 352 : 72 - +
  • [28] Web service choreography conformance verification in M2M systems through the piX-model
    Van Seghbroeck, Gregory
    De Turck, Filip
    Dhoedt, Bart
    Demeester, Piet
    [J]. 2007 IEEE INTERNATIONAL CONFERENCE ON PERVASIVE SERVICES, 2007, : 385 - +
  • [29] Formal Transaction Modeling and Verification for an Adaptable Web Service Orchestration
    Zatout, Sara
    Benabdelhafid, Maya Souilah
    Boufaida, Mahmoud
    [J]. 2018 IEEE 18TH INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY COMPANION (QRS-C), 2018, : 531 - 536
  • [30] A Formal Basis for Cross-Checking ebXML BPSS Choreography and Web Service Orchestration
    Yeung, W. L.
    [J]. 2008 IEEE ASIA-PACIFIC SERVICES COMPUTING CONFERENCE, VOLS 1-3, PROCEEDINGS, 2008, : 524 - 529
12345