Issues in distributed timed model checking

VÍCTOR A. BRABERMAN; ALFREDO OLIVERO; FERNANDO SCHAPACHNIK

International Journal on Software Tools for Technology Transfer (STTT)

Springer Verlag

Lugar: Berlin, Heidelberg ; Año: 2005 vol. 7 p. 4 - 18

1433-2779

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.