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
Descripción
Sumario: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.

Ejemplares similares