Issues in distributed timed model checking
In this work we present ZEUS, a distributed timed model checker that evolves from the TCTL model checker Kronos [13] and that currently can handle backwards computation of reachability properties [2] over timed automata [3]. ZEUS was developed following a software architecture-centric approach. Its...
Guardado en:
| Autores principales: | , |
|---|---|
| Publicado: |
2005
|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_14332779_v7_n1_p4_Braberman http://hdl.handle.net/20.500.12110/paper_14332779_v7_n1_p4_Braberman |
| Aporte de: |
| Sumario: | In this work we present ZEUS, a distributed timed model checker that evolves from the TCTL model checker Kronos [13] and that currently can handle backwards computation of reachability properties [2] over timed automata [3]. ZEUS was developed following a software architecture-centric approach. Its conceptual architecture was conceived to be sufficiently modular to house several features such as a priori graph partitioning, synchronous and asynchronous computation, communication piggybacking, delayed messaging, and dead-time utilization. Surprisingly enough, early experiments pinpointed the difficulties of getting speedups using asynchronous versions and showed interesting results on the synchronous counterpart, although being intuitively less attractive. © Springer-Verlag 2004. |
|---|