Formal Foundations of Hybrid Process Models
The design, implementation, and analysis of software systems are often driven by process models that capture the actions executed by a system along with their causal dependencies. Such a process model can be defined imperatively or declaratively, either defining states and state transitions of the system explicitly or imposing a set of constraints for the occurrences of actions that must be satisfied by the system. Recently, hybrid process models that combine imperative and declarative modelling emerged as a promising formalism to model systems that show both, parts of very rigid, structured behaviour suited for imperative modelling and parts of flexible, widely unconstrained behaviour suited for declarative modelling.
A major obstacle for the application of hybrid process models, however, is the lack of a theory for the synthesis of a model that combines imperative and declarative model parts. Consequently, both modelling paradigms are linked in an ad-hoc manner in the course of control-flow specification, which is error-prone, leads to inconsistencies in large-scale specifications, neglects the full potential of hybrid process models, and severely limits the development of automated tool support.
The aim of this project is to develop a theory for the synthesis of hybrid process models. Given a behavioural specification modelled as a transition system, I will answer the question of how to construct a hybrid model comprising a net system and declarative constraints that jointly capture the behavioural specification. Taking the theory of regions for net synthesis as a starting point, I will devise algorithms that integrate declarative constraints in the synthesis step. Technically, this integration will be achieved by encoding declarative constraints as state-based (in-) equalities. These equations are then used to adapt the equation systems that are solved to identify the structure of the net system. The novel synthesis technique will be complemented by a mechanism that aims at minimising the structure of the hybrid model under a set of declarative constraint templates – providing a means to synthesise particularly compact models.
Hybrid process models have the potential to dramatically improve the design, implementation, and analysis of systems due to their integrated view on rigid as well as on flexible behaviour. The research on their formal foundations will foster the applicability of hybrid process modelling and provide the basis for novel techniques to re-factor and validate process models.
Mittelgeber
German Israel Foundation
Laufzeit
Projektstart: 01/2017
Projektende: 06/2018
