Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.programming.threads > #2455 > unrolled thread

Analyzing parallel applications with Petri Nets

Started byaminer <aminer@toto.net>
First post2014-06-10 05:04 -0700
Last post2014-06-10 05:04 -0700
Articles 1 — 1 participant

Back to article view | Back to comp.programming.threads


Contents

  Analyzing parallel applications with Petri Nets aminer <aminer@toto.net> - 2014-06-10 05:04 -0700

#2455 — Analyzing parallel applications with Petri Nets

Fromaminer <aminer@toto.net>
Date2014-06-10 05:04 -0700
SubjectAnalyzing parallel applications with Petri Nets
Message-ID<ln7rs0$os4$1@news.albasani.net>
Hello,

I have lnvented a new technic that allows us to analyse
more easily parallel applications, i have included this technic
on the follwing tutorial that i have put on my website:

https://sites.google.com/site/aminer68/how-to-analyse-parallel-applications-with-petri-nets

I have used my new technic and Petri Nets and used Tina software
to analyse parallel applications and i have showed you how to model 
Semaphores, and Critical sections and how to model the windows 
WaitForsingleObject() and the windows WaitForMultipleObjects() using
Petri Nets.. and i have showed you how to model a parallel application 
in Object Pascal with Petri Nets to avoid deadlocks even in complex
parallel realtime safe critical  systems...

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 my html tutorial that uses Object pascal from here:

https://sites.google.com/site/aminer68/how-to-analyse-parallel-applications-with-petri-nets

and you can download Tina(TIme petri Net Analyzer) that i have used in 
my tutorial from here:

http://projects.laas.fr/tina/
Also you need to download Romeo from here:

http://romeo.rts-software.org/



Thank you,
Amine Moulay Ramdane.







[toc] | [standalone]


Back to top | Article view | comp.programming.threads


csiph-web