Specifying and verifying contract-driven service compositions using commitments and model checking

作者：

Highlights：

• A novel approach is provided to specify and verify service compositions contracts.

• BPEL is extended to represent specifications and mark the points to be verified.

• Properties are derived automatically from composition implementations.

• The verification process relies on commitment logic and its model checking.

• Web services are verified from the perspectives of compliance and violations.

摘要

•A novel approach is provided to specify and verify service compositions contracts.•BPEL is extended to represent specifications and mark the points to be verified.•Properties are derived automatically from composition implementations.•The verification process relies on commitment logic and its model checking.•Web services are verified from the perspectives of compliance and violations.

论文关键词：Contract-driven web services,Web service composition,BPEL,Communicative commitments,Model checking

论文评审过程：Received 22 July 2016, Revised 22 December 2016, Accepted 23 December 2016, Available online 29 December 2016, Version of Record 24 January 2017.

论文官网地址：https://doi.org/10.1016/j.eswa.2016.12.031