Publication

Design-time Compliance of Service Compositions in Dynamic Service Environments

Groefsema, H. & van Beest, N., Oct-2015, 8th IEEEE International Conference on Service Oriented Computing & Applications (SOCA). IEEE (The Institute of Electrical and Electronics Engineers), p. 108-115 8 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

In order to improve the flexibility of information systems, an increasing amount of business processes is being automated by implementing tasks as modular services in service compositions. As organizations are required to adhere to laws and regulations, with this increased flexibility there is a demand for automated compliance checking of business processes. Model checking is a technique which exhaustively and automatically verifies system models against specifications of interest, e.g. a finite state machine against a set of logic formulas. When model checking business processes, existing approaches either cause large amounts of overhead, linearize models to such an extent that activity parallelization is lost, offer only checking of runtime execution traces, or introduce new and unknown logics. In order to fully benefit from existing model checking techniques, we propose a mapping from workflow patterns to a class of labeled transition systems known as Kripke structures. With this mapping, we provide pre-runtime compliance checking using well-known branching time temporal logics. The approach is validated on a complex abstract process which includes a deferred choice, parallel branching, and a loop. The process is modeled using the Business Process Model and Notation (BPMN) standard, converted into a colored Petri net using the workflow patterns, and subsequently translated into a Kripke structure, which is then used for verification.
Original languageEnglish
Title of host publication8th IEEEE International Conference on Service Oriented Computing & Applications (SOCA)
PublisherIEEE (The Institute of Electrical and Electronics Engineers)
Pages108-115
Number of pages8
Publication statusPublished - Oct-2015
EventThe 8th IEEE International Conference on Service Oriented Computing & Applications Rome, Italy, 19-21 October 2015 - Rome, Italy
Duration: 19-Oct-201521-Oct-2015

Conference

ConferenceThe 8th IEEE International Conference on Service Oriented Computing & Applications Rome, Italy, 19-21 October 2015
CountryItaly
CityRome
Period19/10/201521/10/2015

Event

The 8th IEEE International Conference on Service Oriented Computing & Applications Rome, Italy, 19-21 October 2015

19/10/201521/10/2015

Rome, Italy

Event: Conference

    Keywords

  • Business Process Management, BPMN, Petri net, Kripke models, Verification, Temporal Logic

View graph of relations

ID: 23038634