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., Olivero, A., Schapachnik, F.
Formato:	JOUR
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:	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	todo:paper_14332779_v7_n1_p4_Braberman
record_format	dspace
spelling	todo:paper_14332779_v7_n1_p4_Braberman2023-10-03T16:14:10Z Issues in distributed timed model checking Braberman, V. Olivero, A. Schapachnik, F. 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. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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. Olivero, A. Schapachnik, F. 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.
format	JOUR
author	Braberman, V. Olivero, A. Schapachnik, F.
author_facet	Braberman, V. Olivero, A. Schapachnik, F.
author_sort	Braberman, V.
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
url	http://hdl.handle.net/20.500.12110/paper_14332779_v7_n1_p4_Braberman
work_keys_str_mv	AT brabermanv issuesindistributedtimedmodelchecking AT oliveroa issuesindistributedtimedmodelchecking AT schapachnikf issuesindistributedtimedmodelchecking
_version_	1807320924885614592

Issues in distributed timed model checking

Ejemplares similares