[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Report on verification of unknown number of processes
- To: PetriNets@daimu.aau.dk, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com
- Subject: Report on verification of unknown number of processes
- From: firstname.lastname@example.org (Farn Wang)
- Date: Wed, 10 Mar 1999 14:29:03 +0800 (CST)
- Cc: email@example.com
Hi, dear fella :
Recently, we have developed a new verification technique which
can be used to verify infinite state systems.
Verification of Dynamic Linear Lists for All Numbers of Processes
in PostScript format can be obtained through my webpage:
A preliminary report can also be found in TR-IIS-98-019 published last year.
Thank you for reading this email.
In real-world design and verification of concurrent systems
with many identical processes, the
number of processes is never a factor in the system correctness.
This paper embodies such an engineering reasoning to
propose an almost automatic method to safely verify
safety properties of such systems.
The central idea is to construct a finite collective quotient structure
(CQS) which collapses state-space representations for all system
implementations with all numbers of processes.
The problem is presented as safety bound problem which ask if
the number of processes satisfying a certain property exceeds a given bound.
Our method can be applied to systems with dynamic linear lists of unknown
number of processes.
Processes can be deleted from or inserted at any position of the linear list
We have used our method to develop CQS constructing algorithms for
two classes of concurrent systems :
(1) untimed systems with a global waiting queue and
(2) dense-time systems with one local timer per process.
We show that our method is both sound and complete in verifying the
first class of systems.
The verification problem for the second class systems is
undecidable even with only one global binary variable.
However, our method can still automatically generate a
CQS of size no more than 1512 nodes to
verify that an algorithm in the class: Fischer's timed
algorithm indeed preserves mutual exclusion for any number of processes.