Safe distribution of declarative processes

TY - CHAP

T1 - Safe distribution of declarative processes

AU - Hildebrandt, Thomas

AU - Mukkamala, Raghava Rao

AU - Slaats, Tijs

N1 - Conference code: 9

PY - 2011

Y1 - 2011

N2 - We give a general technique for safe distribution of a declarative (global) process as a network of (local) synchronously communicating declarative processes. Both the global and local processes are given as Dynamic Condition Response (DCR) Graphs. DCR Graphs is a recently introduced declarative process model generalizing labelled prime event structures to a systems model able to finitely represent ω-regular languages. An operational semantics given as a transition semantics between markings of the graph allows DCR Graphs to be conveniently used as both specification and execution model. The technique for distribution is based on a new general notion of projection of DCR Graphs relative to a subset of labels and events identifying the set of external events that must be communicated from the other processes in the network in order for the distribution to be safe. We prove that for any vector of projections that covers a DCR Graph that the network of synchronously communicating DCR Graphs given by the projections is bisimilar to the original global process graph. We exemplify the distribution technique on a process identified in a case study of an cross-organizational case management system carried out jointly with Exformatics A/S.

AB - We give a general technique for safe distribution of a declarative (global) process as a network of (local) synchronously communicating declarative processes. Both the global and local processes are given as Dynamic Condition Response (DCR) Graphs. DCR Graphs is a recently introduced declarative process model generalizing labelled prime event structures to a systems model able to finitely represent ω-regular languages. An operational semantics given as a transition semantics between markings of the graph allows DCR Graphs to be conveniently used as both specification and execution model. The technique for distribution is based on a new general notion of projection of DCR Graphs relative to a subset of labels and events identifying the set of external events that must be communicated from the other processes in the network in order for the distribution to be safe. We prove that for any vector of projections that covers a DCR Graph that the network of synchronously communicating DCR Graphs given by the projections is bisimilar to the original global process graph. We exemplify the distribution technique on a process identified in a case study of an cross-organizational case management system carried out jointly with Exformatics A/S.

U2 - 10.1007/978-3-642-24690-6_17

DO - 10.1007/978-3-642-24690-6_17

M3 - Bidrag til bog/antologi

SN - 978-3-642-24689-0

T3 - Lecture notes in computer science

SP - 237

EP - 252

BT - Software Engineering and Formal Methods

A2 - Barthe, Gilles

A2 - Pardo, Alberto

A2 - Schneider, Gerardo

PB - Springer

T2 - 9th International Conference on Software Engineering and Formal Methods

Y2 - 14 November 2011 through 18 November 2011

ER -