AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL

Web services composition (WSC) has an enormous potential for the organizations in the B2B area. In fact, different services collaborate through the exchange of messages to implement complex business processes. BPEL is one of the most used languages to develop such cooperation. However, it has been proved that its use is complex and can require some expertise in XML syntax. Even its graphical representation is not evident to handle. This is why the authors propose to model Web services using oWF-nets, a subclass of Petri nets, and then, to translate them to BPEL. Whilst, a WSC is with added value only if the involved services are compatible. So in this context, across the translation proposed the researchers develop a verification layer of the WSC compatibility. Hence, they propose a framework named D&A4WSC which allows to model the WSC by oWF-nets, to check their compatibility with the model checker NuSMV and to translate them if they are compatible in BPEL processes using the oWFN2BPEL compiler. D&A4WSC permits, furthermore, to formally analyze a BPEL process.

Download Full-text

A Symbolic Model Checker for Petri Nets: pnmc

Transactions on Petri Nets and Other Models of Concurrency XI - Lecture Notes in Computer Science ◽

10.1007/978-3-662-53401-4_15 ◽

2016 ◽

pp. 297-306 ◽

Cited By ~ 2

Author(s):

Alexandre Hamez

Keyword(s):

Petri Nets ◽

Model Checker ◽

Symbolic Model

Download Full-text

Feasible Dynamic Reconfigurations of Petri Nets

Formal Methods in Manufacturing Systems - Advances in Civil and Industrial Engineering ◽

10.4018/978-1-4666-4034-4.ch010 ◽

2013 ◽

pp. 247-267

Author(s):

Jia Feng Zhang ◽

Olfa Mosbahi ◽

Mohamed Khalgui ◽

Atef Gharbi

Keyword(s):

Petri Nets ◽

Real World ◽

Production System ◽

Manufacturing Systems ◽

Research Work ◽

Reconfigurable Systems ◽

Model Checker ◽

Simple Modification ◽

The Third ◽

Verification Methods

Reconfigurable systems have received much attention from academia and industry because they are efficient, agile, and reasonably priced, and they are the trend of all future systems. The chapter focuses on dynamic automatic reconfigurations of Control Systems to be classically modeled by Petri nets. Several modeling and verification methods for such systems are shown and compared before the introduction of the research work on feasible dynamic reconfigurations and the implementation of manufacturing systems based on Petri nets. Three different reconfiguration scenarios can be applied at run-time to such systems: Addition/Removal of places, Addition/Removal/Update of transitions, or finally, the simple modification of the initial marking. Three formal modules are defined accordingly, which allow the reconfigurations of the system’s Petri nets model: the first module to dynamically change places of the model, the second to dynamically reconfigure transitions within a given subset of places, and the third to modify the initial markings of places. To check the correct behavior of this architecture according to user requirements, the model checker SESA is applied for the verification of CTL-based properties of the proposed modules and also of the system. The contribution is applied to a real-world Benchmark Production System.

Download Full-text

A CTL* Model Checker for Petri Nets

Application and Theory of Petri Nets and Concurrency - Lecture Notes in Computer Science ◽

10.1007/978-3-030-51831-8_21 ◽

2020 ◽

pp. 403-413

Author(s):

Elvio Gilberto Amparore ◽

Susanna Donatelli ◽

Francesco Gallà

Keyword(s):

Petri Nets ◽

Model Checker

Download Full-text

An Approach for the Transformation and Verification of BPMN Models to Colored Petri Nets Models

International Journal of Software Innovation ◽

10.4018/ijsi.2020010102 ◽

2020 ◽

Vol 8 (1) ◽

pp. 17-49 ◽

Cited By ~ 2

Author(s):

Said Meghzili ◽

Allaoua Chaoui ◽

Martin Strecker ◽

Elhillali Kerkouche

Keyword(s):

Petri Nets ◽

Structural Properties ◽

Graph Transformation ◽

Colored Petri Nets ◽

Model Checker ◽

Model Driven Engineering ◽

Model Driven ◽

Successful Termination ◽

Cpn Tools

The correctness of transformations has recently begun to attract the attention of the researchers in Model Driven Engineering (MDE). The objective of this article is twofold. First, it presents an approach for transforming BPMN models to Colored Petri nets models using GROOVE and EMF/Xpand tools. Second, it proposes an approach for checking the correctness of the transformation itself. More precisely, we have defined the termination property of the transformation and the preservation of some structural properties of BPMN models by the transformation using the GROOVE graph transformation tool. The authors have also applied the approach on a case study through which the authors have verified the successful termination of the transformation using GROOVE Model Checker and the target model properties using CPN Tools.

Download Full-text