Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
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: Mar 10 2017

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)
Bookmark and Share
  Featured Reviewer  
 
Verification (D.4.6 ... )
 
 
Distributed Programming (D.1.3 ... )
 
 
Parallel Programming (D.1.3 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Verification": Date
Muse--a computer assisted verification system
Halpern J., Owre S., Proctor N., Wilson W. IEEE Transactions on Software Engineering SE-13(2): 151-156, 1987. Type: Article
Dec 1 1987
The Specification and Modeling of Computer Security
McLean J. Computer 23(1): 9-16, 1990. Type: Article
Oct 1 1990
Digital system verification: a combined formal methods and simulation framework
Li L., Thornton M., Morgan and Claypool Publishers, San Rafael, CA, 2010.  100, Type: Book (978-1-608451-78-4)
Oct 24 2011
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy