Publication

A Formal Model for Compliance Verification of Service Compositions

Groefsema, H., van Beest, N. & Aiello, M., May-2018, In : Ieee transactions on services computing. 11, 3, p. 466-479 14 p.

Research output: Contribution to journalArticleAcademicpeer-review

Copy link to clipboard

Documents

  • A Formal Model for Compliance Verification of Service Compositions

    Final publisher's version, 1 MB, PDF document

    Request copy

DOI

Business processes design and execution environments increasingly need support from modular services in service compositions to offer the flexibility required by rapidly changing requirements. With each evolution, however, the service composition must continue to adhere to laws and regulations, resulting in a demand for automated compliance checking. Existing approaches, if at all, either offer only verification after the fact or linearize models to such an extent that parallel information is lost. We propose a mapping of service compositions to Kripke structures by using colored Petri nets. The resulting model allows preventative compliance verification using well-known temporal logics and model checking techniques while providing full insight into parallel executing branches and the local next invocation. Furthermore, the mapping causes limited state explosion, and allows for significant further model reduction. The approach is validated on a case study from a telecom company in Australia and evaluated with respect to performance and expressiveness. We demonstrate that the proposed mapping has increased expressiveness while being less vulnerable to state explosion than existing approaches, and show that even large service compositions can be verified preventatively with existing model checking techniques.
Original languageEnglish
Pages (from-to)466-479
Number of pages14
JournalIeee transactions on services computing
Volume11
Issue number3
Publication statusPublished - May-2018

    Keywords

  • Service Composition, Business process, Compliance, Verification, Temporal Logic, Colored Petri net, Kripke structure, COMPLIANCE-CHECKING, BUSINESS, SPECIFICATION, SUPPORT

View graph of relations

ID: 32822898