MIT Category Theory Seminar
2020/03/12
©Spifong
Title: Towards a compositional, SMT-based verification of data-aware processes
Abstract:
During the last two decades, a huge body of research has been dedicated to the challenging 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. In parallel, a flourishing series of results has been dedicated to the formalization of such integrated models, and to the study of the boundaries of decidability for their analysis and verification. However, in these integrated models a compositional description of the control-flow is still missing: 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 semantically be interpreted as sequential or 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 to adapt the well-known backward reachability procedure in a full-fledged SMT (Satisfiability Modulo Theories) setting. By using suitable forms of quantifier elimination, backward reachability can be proved to be sound and complete for checking (un)safety, and interesting fragments where backward reachability is a full decision procedure can be isolated. Moreover, the SMT technology can be exploited in implementations, building on the well-known MCMT model checker for array-based system.
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).