On-the-fly Workload Prediction and Redistribution in the Distributed Time Model Cheker Zeus

VICTOR A. BRABERMAN; ALFREDO OLIVERO; FERNANDO SCHAPACHNIK

Electr. Notes Theor. Comput. Sci.

Elsevier

Año: 2005 vol. 128 p. 3 - 18

1571-0661

In this work we present the on-the-fly workload prediction and redistribution techniques used in Zeus [Braberman, V., A. Olivero and F. Schapachnik, Zeus: A distributed timed model checker based on kronos, in: Workshop on Parallel and Distributed Model Checking, affiliated to CONCUR 2002 (13th International Conference on Concurrency Theory), ENTCS 68 (2002), Braberman, V., A. Olivero and F. Schapachnik, Issues in Distributed Model-Checking of Timed Automata: building zeus, to appear in International Journal of Software Tools for Technology Transfer (2004)], a Distributed Model Checker that evolves from the tool Kronos [Daws, C., A. Olivero, S. Tripakis and S. Yovine, The Tool KRONOS, in: Proceedings of Hybrid Systems III, LNCS 1066 (1996), pp. 208–219]. After reviewing why it is so hard to have good speedups in distributed timed model checking, we present the methods used to get promising results when verifying reachability properties over timed automata [Alur, R. and D. L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183–235].