Zeus: A distributed timed model-checker based on Kronos

Mostrar todas las versiones(3)

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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, V., Olivero, A., Schapachnik, F.
Formato: Artículo publishedVersion
Lenguaje:Inglés
Publicado: 2002
Materias:
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
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_15710661_v68_n4_p503_Braberman
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paperaa:paper_15710661_v68_n4_p503_Braberman
record_format dspace
spelling paperaa:paper_15710661_v68_n4_p503_Braberman2023-06-12T16:50:48Z Zeus: A distributed timed model-checker based on Kronos Electron. Notes Theor. Comput. Sci. 2002;68(4):503-522 Braberman, V. Olivero, A. Schapachnik, F. 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 info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion application/pdf eng info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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)
language Inglés
orig_language_str_mv eng
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.
Olivero, A.
Schapachnik, F.
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.
format Artículo
Artículo
publishedVersion
author Braberman, V.
Olivero, A.
Schapachnik, F.
author_facet Braberman, V.
Olivero, A.
Schapachnik, F.
author_sort Braberman, V.
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 http://hdl.handle.net/20.500.12110/paper_15710661_v68_n4_p503_Braberman
work_keys_str_mv AT brabermanv zeusadistributedtimedmodelcheckerbasedonkronos
AT oliveroa zeusadistributedtimedmodelcheckerbasedonkronos
AT schapachnikf zeusadistributedtimedmodelcheckerbasedonkronos
_version_ 1769810141579837440

Ejemplares similares