25 March 2021, 14:00, online

Speaker

Alessandro Gianola, Free University of Bozen-Bolzano

Title

Toward a Compositional Verification of Data-Aware Processes via CospanSpan(Graph)

Abstract

During the last two decades, a huge body of research has been dedicated to the difficult problem of reconciling data and process management within contemporary organizations. This requires to move from a purely control-flow understanding of business processes to a more holistic approach that also considers how data are manipulated and evolved by the process. However, a compositional description of the control-flow is still missing in these integrated models: indeed, it is not clear in the literature how to define the process component so as to guarantee the availability of significant semantic compositional operations. The lack of an algebra formalizing the control-flow makes very challenging the problem of describing and also verifying the combined models.

In this talk, I will present a categorical way for expressing fully compositional workflows, relying on the algebra of CospanSpan(Graph). In this model, the algebras employed to formalize finite-state control-flows are equipped with a plethora of algebraic operations: some of them can be interpreted semantically as sequential and parallel (with and without communication) composition of automata. However, the integration with data here is not supported yet.

Then, I will introduce the verification problem for DABs --- a data-aware extension of BPMN (Business Process Model and Notation), the standard language for modeling business processes --- to assess (parameterized) safety properties. Such integrated model exploits the model-theoretic framework of array-based systems, which allows us to adapt the well-known backward reachability procedure in a full-fledged SMT (Satisfiability Modulo Theories) setting.

Finally, I will argue why the DAB model seems to be the right candidate to incorporate the compositional description of control-flows provided by CospanSpan(Graph).