Enforcing the Correct Execution of Processes Using Smart Contracts on Blockchains (ciclo LiMoSP)

In industry, automated operations are often encapsulated in processes that are executed by collaborating partners that share information following some agreed protocol. BPMN is a rich modeling notation allowing to specify the protocols that processes should follow (using Choreography diagrams) as well as the structure of the processes to be executed (using Collaboration diagrams). The problem is thus how to design a BPMN enforcer, i.e., a monitor ensuring the following requirements:
– It only allows correct executions of processes (soundness).
– It does not alter the execution of processes as long as they behave correctly (transparency).
– It can be inspected by any process owner at any time (trust).
– It is itself distributed in order to avoid performance bottlenecks.
This talk shows how to start from a formal semantics of BPMN choreography diagrams to design a toolchain that takes as input a BPMN choreography diagram and then synthesizes smart contracts that are executed on blockchains and implement the desired distributed BPMN enforcers.