* Report on verification of unknown number of processes
@ 1999-03-10 6:29 Farn Wang
0 siblings, 0 replies; only message in thread
From: Farn Wang @ 1999-03-10 6:29 UTC (permalink / raw)
To: categories
Recently, we have developed a new verification technique which
can be used to verify infinite state systems.
A manuscript:
Verification of Dynamic Linear Lists for All Numbers of Processes
in PostScript format can be obtained through my webpage:
http://www.iis.sinica.edu.tw/~farn/index.html#quo
A preliminary report can also be found in TR-IIS-98-019 published last year.
Thank you for reading this email.
Best wishes,
Farn
ABSTRACT:
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
during transitions.
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.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~1999-03-10 6:29 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1999-03-10 6:29 Report on verification of unknown number of processes Farn Wang
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).