Prosega/CPN: An Extension of CPN Tools for Automata-based Analysis and System Verification
This paper presents Prosega/CPN (Protocol Sequence Generator and Analyzer), an extension of CPN Tools for supporting automata-based analysis and verification. The tool implements several operations such as the generation of a minimized deterministic finite-state automaton (FSA) from a CPN’s occurrence graph, language generation, and FSA comparison. The solution is supported by the Simulator Extensions feature whose development has been driven by the need of integrating CPN with other formal methods.
CPN Tools is an advanced tool for editing, simulating, and analyzing colored Petri nets. This paper discusses the fourth major release of the tool, which makes it simple to use the tool for ordinary Petri nets, including adding inhibitor and reset arcs, and PNML export. This version also supports declarative modeling using constraints, and adds an extension framework making it easy for third parties to extend CPN Tools using Java.
The article analyzes the methods and provides a solution to the problem of detecting logical contradictions in business process models of the health care company. Practical purpose of solving the problem is to increase the efficiency of data management for municipal agencies as stakeholder of company. The methodology is based on formal tools relational logic formalism and the methodology involved is describing business processes by DEMO paradigm. Essentially used the simulator MIT Alloy Analyzer. Analyzed business processes specific organization, provides guidance on the elimination of contradictions.
CPN Tools is a tool for modeling, simulating, and analyzing colored Petri nets. The latest iteration of the tool, CPN Tools 4, extends this with constraints known from declarative languages such as Declare and DCR Graphs. Furthermore, this version introduces an explicit process perspective, powerful extensibility allowing third parties to extend the tools capabilities, and a visualization perspective making it possible to make high-level visualizations of executions directly in the tool.
In our demonstration, we show how it is possible to create models incorporating declarative and imperative constructs and how to use these models to generate simulation logs that can be directly imported into ProM. We show off the new process perspective on top of colored Petri nets, exemplify the use of the perspective to generate readable Java code directly from models, and show how the visualization perspective makes it possible to show the formal underlying model alongside an easier-tograsp for non-experts high-level visualization.
Our intended audience comprise current users of CPN Tools interested in recent developments and practitioners interested in colored Petri nets and hybrid models. We expect to tailor each demonstration to the wishes of the audience.
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and verication, programming and specification languages, etc.
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 invited talks in full paper length. The papers cover various topics in the field of Petri nets and related models of concurrency.
Nested Petri nets (NP-nets) are Petri nets with net tokens - an extension of high-level Petri nets for modeling active objects, mobility and dynamics in distributed systems. In this paper we present an algorithm for translating two-level NP-nets into behaviorally equivalent Colored Petri nets with the view of applying CPN methods and tools for nested Petri nets analysis. We prove, that the proposed translation preserves dynamic semantics in terms of bisimulation equivalence.
This volume contains the Post-Conference Proceedings of ISoLA 2006, the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2006), which was held in Paphos, Cyprus on 15th-19th November 2006, sponsored by EASST and in cooperation with the IEEE Technical Committee on Complex Systems.
In this paper, we address the problem of setting a deterministic Finite State Machine (FSM) to a designated initial state. Differently from other papers, we propose to use adaptive synchronizing sequences (test cases) for this purpose and show that for weakly-connected deterministic complete reduced FSMs the problem of checking the existence of an adaptive synchronizing sequence is in P. For partial deterministic reduced FSMs the problem is PSPACE-complete.