Design of parallel and distributed systems with high-level Petri nets using CASE technology

2002 ◽  
Author(s):  
B. Mikolajczak ◽  
J.T. Rumbut
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
High Level

scholarly journals Computer Aided Verification of Lamport's Fast Mutual Exclusion Algorithm - Using Coloured Petri Nets and Occurrence Graphs with Symmetries

1997 ◽  
Vol 26 (512) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Lars Michael Kristensen
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Mutual Exclusion ◽  
Condensed State ◽  
Coloured Petri Nets ◽  
Computer Tool ◽  
State Spaces ◽  
Index Terms ◽  
High Level ◽  
Mutual Exclusion Algorithm

<p>In this paper, we present a new computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Coloured Petri Nets(CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a signigicant increase in the number of states which can be analysed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. CP-nets and OS-graphs are not our invention. Our contribution is development of the tool and verification of the example.</p><p><strong>Index Terms:</strong> Modelling and Analysis of Distributed Systems, Formal Verification, Coloured Petri Nets, High-Level Petri Nets, Occurrence Graphs, State Spaces, Symmetries, Mutual Exclusion.</p>

scholarly journals Analysing Coloured Petri Nets by the Occurrence Graph Method

1997 ◽  
Vol 26 (517) ◽  
Author(s):  
Jens Bæk Jørgensen
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Research Area ◽  
Coloured Petri Nets ◽  
Main Subject ◽  
Graph Method ◽  
Research Areas ◽  
High Level ◽  
Phd Thesis ◽  
Work Done

<p>This paper provides an overview og the work done for the author's PhD thesis. The research area of Coloured Petri Nets is introduced, and the available analysis methods are presented. The occurrence graph method, which is the main subject of this thesis, is described in more detail. Summaries of the six papers which, together with this overview, comprise the thesis are given, and the contributions are discussed.</p><p>A large portion of this overview is dedicated to a description of related work. The aim is twofold: First, to survey pertinent results within the research areas of -- in increasing generality -- Coloured Petri Nets, High-level Petri Nets, and formalisms for modelling and analysis of parallel and distributed systems. Second, to put the results obtained in this thesis in a wider perspective by comparing them with important related work.</p>

Sign in / Sign up

Export Citation Format

Share Document