Name
Abstract | ||
|---|---|---|
In this paper we address the problem of distributing model checking of timed automata. We demonstrate through four real life ex- amples that the combined processing and memory resources of multi- processor computers can be eectiv ely utilized. The approach assumes a distributed memory model and is applied to both a network of worksta- tions and a symmetric multiprocessor machine. However, certain unex- pected phenomena have to be taken into account. We show how in the timed case the search order of the state space is crucial for the eectiv e- ness and scalability of the exploration. An eectiv e heuristic to counter the eect of the search order is provided. Some of the results open up for improvements in the single processor case. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/10722167_19 | CAV |
Keywords | Field | DocType |
timed model checking,search order,model checking,state space,distributed memory | Heuristic,Model checking,Computer science,Algorithm,Distributed memory,Finite-state machine,Theoretical computer science,Multiprocessing,State space,Formal verification,Scalability,Distributed computing | Conference |
ISBN | Citations | PageRank |
3-540-67770-4 | 56 | 5.24 |
References | Authors | |
12 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gerd Behrmann | 1 | 1648 | 81.69 |
| Thomas Hune | 2 | 230 | 16.61 |
| Frits W. Vaandrager | 3 | 1195 | 126.09 |