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 architecture centric approach. It introduces some i...
Guardado en:
| Autores principales: | , |
|---|---|
| Publicado: |
2002
|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15710661_v68_n4_p503_Braberman http://hdl.handle.net/20.500.12110/paper_15710661_v68_n4_p503_Braberman |
| Aporte de: |
| id |
paper:paper_15710661_v68_n4_p503_Braberman |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_15710661_v68_n4_p503_Braberman2023-06-08T16:24:35Z Zeus: A distributed timed model-checker based on Kronos Braberman, Víctor Adrián Schapachnik, Fernando Pablo Automata theory Computation theory Computer architecture Computer software Graph theory Mathematical models Matrix algebra Problem solving Program processors Real time systems Set theory Distributed timed model-checker Model-checking Time-consuming tasks Timed automata Distributed computer systems 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. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Schapachnik, F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2002 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15710661_v68_n4_p503_Braberman http://hdl.handle.net/20.500.12110/paper_15710661_v68_n4_p503_Braberman |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Automata theory Computation theory Computer architecture Computer software Graph theory Mathematical models Matrix algebra Problem solving Program processors Real time systems Set theory Distributed timed model-checker Model-checking Time-consuming tasks Timed automata Distributed computer systems |
| spellingShingle |
Automata theory Computation theory Computer architecture Computer software Graph theory Mathematical models Matrix algebra Problem solving Program processors Real time systems Set theory Distributed timed model-checker Model-checking Time-consuming tasks Timed automata Distributed computer systems Braberman, Víctor Adrián Schapachnik, Fernando Pablo Zeus: A distributed timed model-checker based on Kronos |
| topic_facet |
Automata theory Computation theory Computer architecture Computer software Graph theory Mathematical models Matrix algebra Problem solving Program processors Real time systems Set theory Distributed timed model-checker Model-checking Time-consuming tasks Timed automata Distributed computer systems |
| description |
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. |
| author |
Braberman, Víctor Adrián Schapachnik, Fernando Pablo |
| author_facet |
Braberman, Víctor Adrián Schapachnik, Fernando Pablo |
| author_sort |
Braberman, Víctor Adrián |
| title |
Zeus: A distributed timed model-checker based on Kronos |
| title_short |
Zeus: A distributed timed model-checker based on Kronos |
| title_full |
Zeus: A distributed timed model-checker based on Kronos |
| title_fullStr |
Zeus: A distributed timed model-checker based on Kronos |
| title_full_unstemmed |
Zeus: A distributed timed model-checker based on Kronos |
| title_sort |
zeus: a distributed timed model-checker based on kronos |
| publishDate |
2002 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15710661_v68_n4_p503_Braberman http://hdl.handle.net/20.500.12110/paper_15710661_v68_n4_p503_Braberman |
| work_keys_str_mv |
AT brabermanvictoradrian zeusadistributedtimedmodelcheckerbasedonkronos AT schapachnikfernandopablo zeusadistributedtimedmodelcheckerbasedonkronos |
| _version_ |
1768544293097570304 |