Archivio Istituzionale della RicercaThe main limiting factor of the model checker SPIN is currently the amount of available physical memory. This paper explores the possibility of exploiting a distributed-memory execution environment, such as a network of workstations interconnected by a standard LAN, to extend the size of the verification problems that can be successfully handled by SPIN. A distributed version of the algorithm used by SPIN to verify safety properties is presented, and its compatibility with the main memory and complexity reduction mechanisms of SPIN is discussed. Finally, some preliminary experimental results are presented.
Distributed-Memory Model Checking with SPIN / Lerda, F.; Sisto, Riccardo. - 1680:(1999), pp. 22-39. (Intervento presentato al convegno 5th and 6th International SPIN Workshops tenutosi a Trento (ITA). Toulouse (FRA) nel July 5, 1999. September 21 and 24, 1999) [10.1007/3-540-48234-2_3].
Distributed-Memory Model Checking with SPIN
SISTO, Riccardo
1999
Abstract
The main limiting factor of the model checker SPIN is currently the amount of available physical memory. This paper explores the possibility of exploiting a distributed-memory execution environment, such as a network of workstations interconnected by a standard LAN, to extend the size of the verification problems that can be successfully handled by SPIN. A distributed version of the algorithm used by SPIN to verify safety properties is presented, and its compatibility with the main memory and complexity reduction mechanisms of SPIN is discussed. Finally, some preliminary experimental results are presented.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/1418124
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo