Loading...
Please wait, while we are loading the content...
Similar Documents
Parallel State Space Construction for Model-checking Parallel State Space Construction for Model-checking
| Content Provider | Semantic Scholar |
|---|---|
| Author | Mateescu, Radu |
| Copyright Year | 2001 |
| Abstract | The veriication of concurrent nite-state systems by model-checking often requires to generate (a large part of) the state space of the system under analysis. Because of the state explosion problem, this may be a resource-consuming operation, both in terms of memory and Cpu time. In this report, we aim at improving the performances of state space construction by using parallelization techniques. We present parallel algorithms for constructing state spaces (or Labeled Transition Systems) on a network or a cluster of workstations. Each node in the network builds a part of the state space, all parts being merged to form the whole state space upon termination of the parallel computation. These algorithms have been implemented within the Cadp veriication tool set and experimented on various concurrent applications speciied in Lotos. The results obtained show linear speedups and a good load balancing between network nodes. Construction paralllle des espaces d''tats pour la vriication basse sur les moddles RRsumm : La vriication nummrative des systtmes distribuus nombre ni d''tats nnces-site souvent la ggnnration (d'une large partie) de l'espace d''tats du systtme vriier. A cause du probllme de l'explosion d''tats, cette opration peut tre cooteuse en mmmoire et en temps de calcul. Ce rapport propose d'optimiser les performances de la construction des espaces d''tats au moyen de techniques de parallllisation. Nous prrsentons des algorithmes paralllles pour construire les espaces d''tats (ou les systtmes de transitions etiquettes) sur un rrseau ou une grappe de stations de travail. Chaque noeud du rrseau construit une partie de l'espace d''tats, toutes les parties tant rassemblles pour former l'espace d''tats complet aprrs terminaison du calcul paralllle. Ces algorithmes ont tt impllmentts dans la boote outils Cadp et exprimentts sur diiirentes applications distribuues spciiies en Lotos. Les rrsultats obtenus mettent en vidence des gains en vitesse linnaires et un bon quilibrage de charge entre les noeuds du rrseau. |
| File Format | PDF HTM / HTML |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
