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

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Braberman, Víctor Adrián, Schapachnik, Fernando Pablo
Publicado:	2005
Materias:	Distributed timed model checking KRONOS Timed automata Timed systems ZEUS Automata theory Computer aided software engineering Computer architecture Computer simulation Data storage equipment Data structures Real time systems Difference bound matrices Distributed time model checking Distributed computer systems
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:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_14332779_v7_n1_p4_Braberman
record_format	dspace
spelling	paper:paper_14332779_v7_n1_p4_Braberman2023-06-08T16:14:18Z Issues in distributed timed model checking Braberman, Víctor Adrián Schapachnik, Fernando Pablo Distributed timed model checking KRONOS Timed automata Timed systems ZEUS Automata theory Computer aided software engineering Computer architecture Computer simulation Data storage equipment Data structures Real time systems Difference bound matrices Distributed time model checking Timed automata Timed systems Distributed computer systems 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. 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. 2005 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
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Distributed timed model checking KRONOS Timed automata Timed systems ZEUS Automata theory Computer aided software engineering Computer architecture Computer simulation Data storage equipment Data structures Real time systems Difference bound matrices Distributed time model checking Timed automata Timed systems Distributed computer systems
spellingShingle	Distributed timed model checking KRONOS Timed automata Timed systems ZEUS Automata theory Computer aided software engineering Computer architecture Computer simulation Data storage equipment Data structures Real time systems Difference bound matrices Distributed time model checking Timed automata Timed systems Distributed computer systems Braberman, Víctor Adrián Schapachnik, Fernando Pablo Issues in distributed timed model checking
topic_facet	Distributed timed model checking KRONOS Timed automata Timed systems ZEUS Automata theory Computer aided software engineering Computer architecture Computer simulation Data storage equipment Data structures Real time systems Difference bound matrices Distributed time model checking Timed automata Timed systems Distributed computer systems
description	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.
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	Issues in distributed timed model checking
title_short	Issues in distributed timed model checking
title_full	Issues in distributed timed model checking
title_fullStr	Issues in distributed timed model checking
title_full_unstemmed	Issues in distributed timed model checking
title_sort	issues in distributed timed model checking
publishDate	2005
url	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
work_keys_str_mv	AT brabermanvictoradrian issuesindistributedtimedmodelchecking AT schapachnikfernandopablo issuesindistributedtimedmodelchecking
_version_	1768544746916020224

Issues in distributed timed model checking

Ejemplares similares