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

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, V., Olivero, A., Schapachnik, F.
Formato: Artículo publishedVersion
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
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_15710661_v68_n4_p503_Braberman_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-paper_15710661_v68_n4_p503_Braberman_oai
record_format dspace
spelling I28-R145-paper_15710661_v68_n4_p503_Braberman_oai2024-08-16 Braberman, V. Olivero, A. Schapachnik, F. 2002 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. application/pdf http://hdl.handle.net/20.500.12110/paper_15710661_v68_n4_p503_Braberman info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar Electron. Notes Theor. Comput. Sci. 2002;68(4):503-522 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 Zeus: A distributed timed model-checker based on Kronos info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_15710661_v68_n4_p503_Braberman_oai
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (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.
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
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_15710661_v68_n4_p503_Braberman_oai
work_keys_str_mv AT brabermanv zeusadistributedtimedmodelcheckerbasedonkronos
AT oliveroa zeusadistributedtimedmodelcheckerbasedonkronos
AT schapachnikf zeusadistributedtimedmodelcheckerbasedonkronos
_version_ 1809357122559803392

Ejemplares similares