MBT/CPN: A Tool for Model-Based Software Testing of Distributed Systems Protocols Using Coloured Petri Nets

2018 ◽  
pp. 97-113
Author(s):  
Rui Wang ◽  
Lars Michael Kristensen ◽  
Volker Stolz
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Software Testing ◽  
Coloured Petri Nets ◽  
Model Based

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 A Theory for Bipolar Synchronisation Schemes

1983 ◽  
Vol 12 (158) ◽  
Author(s):  
H. J. Genrich ◽  
P. S. Thiagarajan
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Concurrent Programs ◽  
Model Based ◽  
Systematic Fashion ◽  
Good Behaviour ◽  
Do So

The aim is to better understand the relationships between choice and concurrency that lead to the good behaviour of distributed systems. In order to do so, we formulate a model based on Petri nets and develop its theory. The model is called bipolar synchronisation schemes (bp schemes) and the theory we construct is mainly devoted to synthesizing, in a systematic fashion, all well behaved bp schemes. We also provide a computational interpretation of well behaved bp schemes. Through this interpretation the insights gained by developing the theory of bp schemes can be transferred to concurrent programs.

Sign in / Sign up

Export Citation Format

Share Document