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

Søren Debois, Thomas Hildebrandt, Tijs Slaats

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer 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
TitelFM 2015: Formal Methods : 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
RedaktørerNikolaj Bjørner, Frank de Boer
Antal sider18
ISBN (Trykt)978-3-319-19248-2
ISBN (Elektronisk)978-3-319-19249-9
StatusUdgivet - 2015
BegivenhedThe 20th International Symposium on Formal Methods - University of Oslo, Oslo, Norge
Varighed: 22 jun. 201526 jun. 2015
Konferencens nummer: 20


KonferenceThe 20th International Symposium on Formal Methods
LokationUniversity of Oslo
NavnLecture Notes in Computer Science


Dyk ned i forskningsemnerne om 'Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes'. Sammen danner de et unikt fingeraftryk.