[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

tool announcement, RED 3.1 for TCTL model-checking



* 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;