* We apologize if this announcement is of no interest to you or
multiple
* copies of the announcement have reached you.
Hi, dear
Colleagues:
We are happy to announce version 3.1 of RED for
full TCTL model-checking of
real-time concurrent software systems
with the innovative Clock-Restriction
Diagram (CRD).
CRD is different from CDD of UPPAAL in that
CDD uses
DISJOINT intervals for arc labels while
CRD uses upperbounds, which are
structurally overlapping, for arc labels.
With our recent development,
the performace of RED 3.1 has been improved
greatly over version 3.0.
Please try our tools at
http://www.iis.sinica.edu.tw/~farn/red
or
http://val.iis.sinica.edu.tw
We welcome your trial of our tools and your
comments.
The following
table of performance data shows the most recent experiments
of red 3.1
compared to its predecessor.
All data are collected with exact verification.
No approximation
and symmetry reduciton is used.
+---------------+-----------------------+---------------+---------------+
|
benchmarks |
concurrencies
| red v.3.0 | red v.3.1
|
+---------------+-----------------------+---------------+---------------+
|
Fischer's | 3
processes
|
0.66s/47k |
0.2s/18k |
| mutual | 5 processes
| 18.84s/467k | 5.03s/94k |
|
exclusion | 7
processes
| 251.1s/2510k | 47.46s/384k |
|
| 8 processes
| 783.0s/5289k | 140.0s/851k |
|
| 9 processes
|
O/M
| 417.0s/2032k |
|
| 11 processes
|
O/M | 3179s/10897k
|
|
| 13 processes
|
O/M | 23600s/55978k
|
+---------------+-----------------------+---------------+---------------+
|
CSMA/CD
| bus + 3 senders | 0.43s/103k | 0.09s/103k |
|
mutual
| bus + 5 senders | 4.05s/292k | 0.41s/292k |
|
exclusion | bus
+ 7 senders | 50.14s/974k | 1.88s/723k |
|
| bus + 9 senders | 466.5s/4344k | 12.45s/3971k |
|
| bus + 11 senders | 3680s/19869k | 115.2s/21470k |
|
| bus + 13 senders | 28040s/91093k
| 1893s/111699k
|
+---------------+-----------------------+---------------+---------------+
|
FDDI
| ring + 11 stations
| 1.22s/345k
| 1.19s/345k |
|
token-ring | ring + 12
stations | 1.85s/456k | 1.79s/456k |
|
passing
| ring + 20 stations
| 16.88s/1311k | 16.59s/1311k |
|
| ring + 30 stations
| 81.37s/2893k | 81.95s/2899k |
|
| ring + 40 stations
| 266.1s/5692k | 266.9s/5962k |
|
| ring + 50 stations
|
N/A | 652.9s/9903k
|
|
| ring + 60 stations
|
N/A | 1264s/14018k
|
+---------------+-----------------------+---------------+---------------+
|
PATHOS
| 3 processes
|
0.45s/44k |
0.07s/25k |
| real-time | 4 processes
| 4.28s/113k
| 0.28s/52k |
| operating |
5 processes
| 49.55s/299k | 1.06s/89k |
|
system
| 6 processes
| 718.6s/1103k | 3.97s/218k |
| schedulability| 7 processes
|
O/M | 21.12s/636k
|
|
| 9 processes
|
O/M | 508.8s/6267k
|
|
| 11 processes
|
O/M | 8898s/65243k
|
+---------------+-----------------------+---------------+---------------+
|
Leader
| 3 processes
|
0.05s/46k |
0.05s/46k |
| election | 5
processes
| 0.40s/165k
| 0.42s/165k |
|
safety
| 7 processes
| 3.47s/479k
| 3.54s/479k
|
|
| 9 processes
| 19.07s/1366k | 19.21s/1366k |
|
| 11 processes
| 69.84s/3280k | 70.32s/3280k |
|
| 13 processes
| 206.9s/6946k | 207.9s/6946k |
|
| 14 processes
| 294.3s/8430k | 340.2s/9683k
|
+---------------+-----------------------+---------------+---------------+
|
Leader | 3
processes
|
1.08s/75k |
0.17s/45k |
| election | 5
processes
| 237.8s/1770k | 10.78s/846k |
| liveness | 7
processes
| 10981s/21800k | 458.5s/11693k |
|
| 8 processes
| N/A
| 2756s/37977k |
|
| 9 processes
|
N/A |19289s/114418k
|
+---------------+-----------------------+---------------+---------------+
data
collected on a Pentium IV 1.7GHz with 256MB memory running LINUX;
s:
seconds; k: kilobytes of memory in data-structure; O/M: Out of memory;