ITU

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

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

View graph of relations

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 http://tiger.itu.dk:8018/.
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
PublisherSpringer
Publication date2015
Pages143-160
ISBN (Print)978-3-319-19248-2
ISBN (Electronic)978-3-319-19249-9
DOIs
Publication statusPublished - 2015
EventThe 20th International Symposium on Formal Methods - University of Oslo, Oslo, Norway
Duration: 22 Jun 201526 Jun 2015
Conference number: 20
http://fm2015.ifi.uio.no/

Conference

ConferenceThe 20th International Symposium on Formal Methods
Nummer20
LocationUniversity of Oslo
LandNorway
ByOslo
Periode22/06/201526/06/2015
Internetadresse
SeriesLecture Notes in Computer Science
Volume9109
ISSN0302-9743

Downloads

No data available

ID: 80629837