Computing Reviews

Model checking Petri nets with names using data-centric dynamic systems
Montali M., Rivkin A. Formal Aspects of Computing28(4):615-641,2016.Type:Article
Date Reviewed: 03/10/17

Carl Adam Petri established Petri net theory, in 1962, with the publication of his doctoral thesis, “Kommunikation mit Automaten.” In the following 54 years, a rich and extensive body of work has been added to the theory and language contributing to the fields of parallel and distributed computing. This 26-page paper focuses on Petri net theory and language, augmenting its use in model checking with the data-centric dynamic systems (DCDS) formalism. The authors state their main contribution: “Our results contribute to the cross-fertilization between the area of formal methods for concurrent systems and the foundations of data-aware processes.”

The first 13 pages introduce Petri nets with name creation and management (v-PNs), marking-labeled transitions (MTS), instance-aware workflow nets (IAW), and resource and instance-aware workflow nets (RIAW). The next six pages define the DCDS formalism as used in the paper and introduce the relational transition system (RTS). A complex example of a web-based shopping cart system is used to illustrate DCDS. The last seven pages, which include two pages of references, introduce the two translation algorithms to transition from a v-PN to a DCDS. Algorithm 1 is used as a data layer generator. Algorithm 2 is used as a process layer generator. The final diagram in figure 8 depicts the relationship between the MTS of the marked v-PN and the RTS of the DCDS obtained from applying the two algorithms.

A strength of the paper is the use of multiple examples of the problems in the various formalisms. A weakness would be the lack of continuity one might expect if two separate papers had been joined together.

Reviewer:  Nancy Eickelmann Review #: CR145115 (1705-0280)

Reproduction in whole or in part without permission is prohibited.   Copyright 2024 ComputingReviews.com™
Terms of Use
| Privacy Policy