Defining the semantics of reactive components in event-driven workflow execution with event histories

摘要

The definition of exact semantics of workflows and involved processing entities is an open yet urgent problem for most systems. This paper considers the semantics and correctness of event-driven workflow execution by reactive components. The basis for the formalization in our approach is provided by an event history which records all the events generated during the execution of workflows by these components. Based on the formal notion of history, it is possible to determine the semantics of workflow systems as the set of event histories they can generate. It also allows to formalize the semantics of reactive components—and consequently, the semantics of workflows—as well as to check whether their observable behavior is correct.In addition to the precise understanding of event-driven workflow execution, the formalized notion of event history also serves as the specification of the workflow execution engine. Ultimately, the semantics of reactive components provides the basis for specifying transformation rules used to map these components onto the execution level.