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