ZEUS: A Distributed Timed Model- Checker Based on KRONOS

VICTOR A. BRABERMAN; AFREDO OLIVERO; FERNANDO SCHAPACHNIK

Electr. Notes Theor. Comput. Sci.

Elsevier

Año: 2003 vol. 68 p. 503 - 522

In this work we present Zeus, a Distributed Model-Checker that evolves from the tool Kronos and that currently can handle backwards computation of TCTLreachability properties over timed-automata. 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 experiment pinpointed the dificulties of getting speedups using a parallel asynchronous version. We also propose some paths to overcome those obstacles.