Zeus: A distributed timed model-checker based on Kronos
In this work we present Zeus, a Distributed Model-Checker that evolves from the tool Kronos [8] and that currently can handle backwards computation of TCTL-reachability properties [1] over timed-automata [2]. Zeus was developed following a software arc...
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Artículo publishedVersion |
| Publicado: |
2002
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_15710661_v68_n4_p503_Braberman https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_15710661_v68_n4_p503_Braberman_oai |
| Aporte de: |
| Sumario: | In this work we present Zeus, a Distributed Model-Checker that evolves from the tool Kronos [8] and that currently can handle backwards computation of TCTL-reachability properties [1] over timed-automata [2]. Zeus was developed following a software architecture centric approach. It introduces some interesting features such as a priori graph partitioning, a sophisticated machinery to reach optimum performance (communication piggybacking and delayed messaging) and dead-time utilization, where every processor uses time intervals of inactivity to perform auxiliary, time-consuming tasks that will later speed up the rest of the computation. Although some good results have been obtained, early experiments pinpointed the difficulties of getting speedups using a parallel asynchronous version. We also propose some paths to overcome those obstacles. We would like to thank Sergio Yovine for making Kronos libraries available to us. © 2002 Published by Elsevier Science B.V. |
|---|