How to analyse parallel applications with Petri Nets

Analyzing parallel applications with Petri Nets By Amine Moulay Ramdane.

The demand for high availability and reliability of computer and software systems has led to a formal verification of such systems. There are two principal approaches to formal verification: model checking and theorem proving.

I will talk about Petri Nets and how to model parallel programs and how to exploit verification tools as Tina to verify the properties such as liveleness of the system. I will restrict the discussion to so-called "1-conservative" Petri Nets, in which the capacity of each place is assumed to be 1, and each edge will remove exactly one mark from a net if it leads from a place to a transition and add exactly one when it leads from a transition to a place.

You can download the html tutorial from here:

You can go to download the zip files by clicking on the following web link:

https://drive.google.com/drive/folders/1W6fLKvf5islKfn5z8MkXNvIaVLh9hHbY?usp=sharing