Name
Abstract | ||
|---|---|---|
ARA is a verification tool which applies some recent improved speed verification techniques. ARA accepts as input systems described in Basic Lotos. With ARA, a system can be verified by showing that it is behaviourally equivalent with its specification. For comparing behaviours, ARA uses a novel CSP-like but catastrophe-free behavioural equivalence notion called CFFD-equivalence. ARA can also reduce the behaviour of the system into a small normal form, and show the result graphically. ARA applies two techniques to cope with the state explosion problem: compositional LTS construction and the stubborn set method. The paper contains a detailed example of the validation of a communication protocol using ARA. The paper concentrates on the intuition behind the various novel ideas of ARA; formal details are mostly omitted. |
Year | DOI | Venue |
|---|---|---|
1993 | 10.1007/BFb0024669 | FME |
Keywords | Field | DocType |
advanced reachability analysis,communication protocol,normal form | Computer science,Intuition,Reachability,Theoretical computer science,Real-time computing,Linear temporal logic,Equivalence (measure theory),Communications protocol | Conference |
ISBN | Citations | PageRank |
3-540-56662-7 | 24 | 1.45 |
References | Authors | |
19 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Antti Valmari | 1 | 1710 | 149.51 |
| J. Kemppainen | 2 | 24 | 2.13 |
| Matthew Clegg | 3 | 167 | 12.51 |
| Mikko Levanto | 4 | 30 | 3.00 |