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:	JOUR
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	todo:paper_15710661_v68_n4_p503_Braberman
record_format	dspace
spelling	todo:paper_15710661_v68_n4_p503_Braberman2023-10-03T16:27:15Z Zeus: A distributed timed model-checker based on Kronos 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. JOUR 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)
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	JOUR
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
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_	1807320543181930496

Zeus: A distributed timed model-checker based on Kronos

Ejemplares similares