Master Thesis Defense by Mr Andrey Rivkin
Mr Andrey Rivkin defended his master thesis on 'Formal verification of data-aware business processes based on Petri nets'.
Mr Andrey Rivkin defended his master thesis on 'Formal verification of data-aware business processes based on Petri nets' at TUD on 15 October 2013.
Abstract:
During the last decade many companies have recognized the effectiveness of Business Process Management in business processes automation and analysis. To guarantee that the enacted processes are trustworthy, correct, and aligned with the intended objectives, business process models need to be (automatically) verified at design time. This, in turn, requires to fix an underlying formal framework so as to define a precise execution semantics for the process models.
One of the common choices, in this respect, is constituted by Petri nets. Over the years, many variations and extensions of Petri nets (such as workflow and colored Petri nets) were proposed to build and analyze business processes at different levels of granularity.
One of the major limitations of contemporary process specification languages and the corre- sponding mainstream analysis techniques is that they focus on the control-flow perspective of business processes, while neglecting the manipulated data.
This triggered extensive research not only in the Petri net community (which produced several variants of colored nets and nets with data), but also in other communities, in particular the database one. In this area, a plethora of frameworks and techniques has been investigated when databases are not considered just as static containers of data, but as dynamic entities evolved through the execution of transactions, actions, and processes. One of the most promising framework in this area has been recently proposed under the name of Data-Centric Dynamic System (DCDS), where processes controlling the dynamics of the system and the manipulation of data (in the form of a full-fledged database with constraints) are equally central.
In this thesis we want to throw a bridge between Petri nets and DCDSs, so as to make it possible to compare and connect the results and techniques developed in the two settings. In particular, we study how variants of Petri nets at increasing level of complexity can be faithfully encoded as DCDSs. Beside providing syntactic translation mechanisms, we study their correctness, in the sense that the execution semantics of the obtained DCDS either coincide with the original Petri net one, or preserves the same properties defined in a suitable verification logic.