Using (Timed) Petri Nets for Verification of Parameterized (Timed) Systems
Parosh Abdulla
Uppsala University
Abstract
We consider parameterized systems which typically
consist of networks with an arbitrary number of components.
The goal is to verify the correctness of the system
regardless of the number of components.
Examples of parameterized systems include mutual exclusion protocols,
cache coherence protocols, and broadcast protocols.
First, we consider systems where each component is
a finitestate process.We show how to capture the behaviour of such a
system using a Petri net.
Then, we show how to generalize the results to parameterized
systems of timed processes using Timed Petri Nets.
In a timed Petri net, each token is equipped with a realvalued
clock representing the ``age'' of the token.
Each arc in the net is provided with a subinterval
of the natural numbers, restricting the ages
of the tokens traveling through the arc.
Timed Petri nets are strictly more powerful
than timed automata, since they operate on an unbounded number
of realvalued clocks.
Place: Information technology, Uppsala University
Room: 1113
Time: 15.1516.15 (+ discussions)
Room 1113 is in building 1, floor 1, room 13
(in the southern part of the building).
Help on how to find ASTEC Seminars.
There will be an extended period for discussions after the seminar.
Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 16.15
Everyone is welcome !
Updated 15Nov2001 17:04 by Roland Grönroos
email: info at astec.uu.se
Location: http://www.astec.uu.se/Seminars/01/1127.shtml
