Warning: Parameter 1 to Language::getMagic() expected to be a reference, value given in /usr/share/mediawiki/includes/StubObject.php on line 58
Declarative Modelling and Verification of Workflows – GRK-Wiki

Declarative Modelling and Verification of Workflows

Aus GRK-Wiki

Wechseln zu: Navigation, Suche

The research subject of Declarative Modelling and Verification of Workflows is a new approach for guaranteeing correctness of large distributed systems.

The subject is located in the field of resarch D (workflow management) and subproject D4 of the PhD graduate school Metrik.



  • characteristics of workflows in disaster management, and in self-stabilising/ self-organising systems
  • suitable models for adaptive and flexible workflows
  • expressiveness of models for adaptive and flexible workflows
  • identifying and analysing relevant properties of adaptive and flexible workflows
  • feasibility of formal workflow models in real scenarios


Problem Setting

The graduate school's envisioned distributed, self-organising, wireless (sensor) network for a disaster management system will use workflows at various levels, from resource management to modeling work procedures at the organizational level. The nature of the network gives rise to a number of new problems in the field of workflows.

The entire system will be implemented by a service-oriented architecture that is capable of integrating the various functionalities of the network's nodes. As the network is subject to permanent change by joining, leaving, and failing nodes and other unpredictable behaviour, it will implement self-organising, self-stabilising and adaptive behaviour at various technological levels. This behaviour comprises, among others, suitable routing protocols as well as the replication of data and services to sustain the networks functionality.

A light-weight middleware will provide basic algorithms encapsulated as services. By suitably composing these basic middleware services to complex services, the network's functionality in terms of availability of resources, connectivity, etc. can be guaranteed, provided the services work correctly. A reasonable approach for composing complex services out of basic middleware services are workflows, as it is exercised in service-oriented architecture.

Applications (e.g. a disaster management system) running in such a network will use the node's services to enable the flow of information from machines to machines, machines to humans, and humans to humans. By relating tasks and communication in their causal order, workflows are an excellent means to describe and realize these dynamics.

Both workflow types, at the level of resource management and at the organizational level, are to be executed in a highly dynamic environment. Standard modeling and verification techniques for workflows assume a 'static' environment where required resources are guaranteed to be available, communication is reliable and cooperating partners are known in advance. It is likely that these assumptions cease to hold in distributed, self-organising, wireless networks. Yet, the workflows of resource management must guarantee an adaptive, self-stabilising, self-organising behaviour such that the organizational workflows can guarantee the required flow of information. Existing modeling and verification techniques have to be analyzed, and, if necessary, extended, to support developers and engineers in their task of constructing a correct system.

Suggested Solution

We found that organizational workflows, as they are practically in effect today, are determined by three aspects:

  • The laws, regulations, and plans that govern the duties in case of an exceptional situation;
  • the concrete behaviour of individuals and small groups of trained professional with reliable actions and interactions in trained settings; and
  • the global tactical and strategic thinking that determines how the different groups shall act and interact in an unknown situation under limited resources.

A joint case study with the Taskforce "Earthquakes" of the GFZ Potsdam confirms this principle separation of concerns. We are therefore researching how this three-fold description of a highly dynamic, distributed process can formally be expressed.

We aim on a combination of three modeling paradigms:

  • We use declarative descriptions like temporal logics or constraints for regulations and plans;
  • we express the complete operational group-level behavior (as far as it may be operationalized) by established operational descriptions like Petri nets; and
  • we use scenario-based specifications to describe intra-group behavior on a global scale.

We then propose operators that detail out how one part (for instance the declarative description) of the model influences the other parts (the operational behaviour and the possible scenarios). This allows for changing one aspect of the model while consistently adapting all other aspects; we aim for doing this at run-time. We establish these formal notions at the most basic level like logics which allows to build high-level abstractions for the chosen domain of application and execution. Based on this model, we will research the expressiveness of our approach, validate its practicability and identify decidable and relevant properties for this class of systems.

Related Research Topics


  • Dirk Fahland: Towards Analyzing Declarative Workflows, In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings 07061, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007.
Persönliche Werkzeuge