Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes

Søren Debois, Thomas Hildebrandt, Tijs Slaats

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


We study modularity, run-time adaptation and refinement under safety and liveness constraints in event-based process models with dynamic sub-process instantiation. The study is part of a larger programme to provide semantically well-founded technologies for modelling, implementation and verification of flexible, run-time adaptable process-aware information systems, moved into practice via the Dynamic Condition Response (DCR) Graphs notation co-developed with our industrial partner. Our key contributions are: (1) A formal theory of dynamic sub-process instantiation for declarative, event-based processes under safety and liveness constraints, given as the DCR* process language, equipped with a compositional operational semantics and conservatively extending the DCR Graphs notation; (2) an expressiveness analysis revealing that the DCR* process language is Turing-complete, while the fragment cor- responding to DCR Graphs (without dynamic sub-process instantiation) characterises exactly the languages that are the union of a regular and an omega-regular language; (3) a formalisation of run-time refinement and adaptation by composition for DCR* processes and a proof that such refinement is undecidable in general; and finally (4) a decidable and practically useful sub-class of run-time refinements. Our results are illustrated by a running example inspired by a recent Electronic Case Management solution based on DCR Graphs and delivered by our industrial partner. An online prototype implementation of the DCR* language (including examples from the paper) and its visualisation as DCR Graphs can be found at
Original languageEnglish
Title of host publicationFM 2015: Formal Methods : 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
EditorsNikolaj Bjørner, Frank de Boer
Number of pages18
Publication date2015
ISBN (Print)978-3-319-19248-2
ISBN (Electronic)978-3-319-19249-9
Publication statusPublished - 2015
EventThe 20th International Symposium on Formal Methods - University of Oslo, Oslo, Norway
Duration: 22 Jun 201526 Jun 2015
Conference number: 20


ConferenceThe 20th International Symposium on Formal Methods
LocationUniversity of Oslo
Internet address
SeriesLecture Notes in Computer Science


  • - Modularity
  • - Run-time Adaptation
  • - Safety and Liveness Constraints
  • - Event-based Process Models
  • - Dynamic Sub-process Instantiation
  • - Process-aware Information Systems
  • - DCR Graphs
  • - Compositional Operational Semantics
  • - Turing-complete
  • - Run-time Refinement and Adaptation


Dive into the research topics of 'Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes'. Together they form a unique fingerprint.

Cite this