Navegar

Colección

Datos Estadísticas

Artículo

Este artículo es de Acceso Abierto y puede ser descargado en su versión final desde nuestro repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

In this work we present Zeus, a Distributed Model-Checker that evolves from the tool Kronos [8] and that currently can handle backwards computation of TCTL-reachability properties [1] over timed-automata [2]. 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 experiments pinpointed the difficulties of getting speedups using a parallel asynchronous version. We also propose some paths to overcome those obstacles. We would like to thank Sergio Yovine for making Kronos libraries available to us. © 2002 Published by Elsevier Science B.V.

Registro:

Documento: Artículo
Título:Zeus: A distributed timed model-checker based on Kronos
Autor:Braberman, V.; Olivero, A.; Schapachnik, F.
Ciudad:Brno
Filiación:Computer Science Department, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina
Department of Information Technology, FIyCE, Universidad Argentina de la Empresa, Buenos Aires, Argentina
Palabras clave:Automata theory; Computation theory; Computer architecture; Computer software; Graph theory; Mathematical models; Matrix algebra; Problem solving; Program processors; Real time systems; Set theory; Distributed timed model-checker; Model-checking; Time-consuming tasks; Timed automata; Distributed computer systems
Año:2002
Volumen:68
Número:4
Página de inicio:503
Página de fin:522
DOI: http://dx.doi.org/10.1016/S1571-0661(05)80389-5
Título revista:PDMC 2002, Parallel and Distributed Model Checking (Satellite Workshop of CONCUR 2002)
Título revista abreviado:Electron. Notes Theor. Comput. Sci.
ISSN:15710661
PDF:https://bibliotecadigital.exactas.uba.ar/download/paper/paper_15710661_v68_n4_p503_Braberman.pdf
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15710661_v68_n4_p503_Braberman

Referencias:

  • Alur, R., Courcoubetis, C., Dill, D.L., Model-checking in dense real-time (1993) Information and Computation, 104, pp. 2-34. , http://citeseer.nj.nec.com/alur93modelchecking.html, URL
  • Alur, R., Dill, D.L., A theory of timed automata (1994) Theoretical Computer Science, 126, pp. 183-235. , http://citeseer.nj.nec.com/alur94theory.html, URL
  • Barnat, J., Brim, L., Stríbřná, J., Distributed LTL model-checking in SPIN (2001) In: SPIN, pp. 200-216. , http://citeseer.nj.nec.com/article/barnat00distributed.html, URL
  • Behrmann, G., Hune, T., Vaandrager, F.W., Distributing timed model checking - How the search order matters (2000) Computer Aided Verification LNCS, 1855, pp. 216-231. , http://citeseer.nj.nec.com/behrmann00distributing.html, URL
  • Ben-David, S., Heyman, T., Grumberg, O., Schuster, A., Scalable distributed on-the-fly symbolic model checking (2000) In: Formal Methods in Computer-Aided Design, pp. 390-404. , http://citeseer.nj.nec.com/326863.html, URL
  • Braberman, V., López, P.C., Olivero, A., On improving backwards verification for timed automata (2002) TPTS 2002, Satellite Event for the Joint European Conference on Theory and Practice of Software, ETAPS 2002 ENTCS, 65. , http://www.elsevier.com/locate/entcs/volume65.html, URL
  • Cousot, P., (1978) "Methodes Iteratives de Construction et d'Aproximation de Points Fixes d'Operateurs Monotones Sur Un Treillis, Analyse Semantique des Programmes," Ph D. Thesis, Université Scientifique et Médicale de Grenoble, Institut National Polytechnique de Grenoble
  • Daws, C., Olivero, A., Tripakis, S., Yovine, S., The Tool KRONOS, in: Proceedings of Hybrid Systems III (1996) LNCS, 1066, pp. 208-219
  • Daws, C., Yovine, S., Two examples of verification of multirate timed automata with (1995) KRONOS Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS'95), pp. 66-75. , http://citeseer.nj.nec.com/daws95two.html, URL
  • Dill, D.L., Timing assumptions and verification of finite-state concurrent systems (1990) International Workshop of Automatic Verification Methods for Finite State Systems LNCS, 407, pp. 197-212
  • Garavel, H., Mateescu, R., Smarandache, I.M., Parallel state space construction for model-checking (2001) Proc. of the 8th International SPIN Workshop, pp. 217-234. , http://citeseer.nj.nec.com/474094.html, M.B. Dwyer. Toronto, Canada URL
  • Grumberg, O., Heyman, T., Schuster, A., Distributed symbolic model checking for m̈-calculus (2001) In: Computer Aided Verification, pp. 350-362. , http://citeseer.nj.nec.com/473825.html, URL
  • Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S., Symbolic Model Checking for Real-Time Systems (1994) Information and Computation, 111, pp. 193-244
  • Heyman, T., Geist, D., Grumberg, O., Schuster, A., Achieving scalability in parallel reachability analysis of very large circuits (2000) Computer Aided Verification, 12th International Conference LNCS, 1855, pp. 20-35. , http://citeseer.nj.nec.com/heyman00achieving.html, Grumberg O. URL
  • Karypis, G., Kumar, V., Parallel multilevel k-way partitioning scheme for irregular graphs (1998) Technical Report, University of Minnesota, Department of Computer Science / US Army HPC Research Center. Minneapolis, USA
  • Lerda, F., Sisto, R., Distributed-memory model checking with SPIN (1999) Proc. of the 5th International SPIN Workshop LNCS, 1680. , http://citeseer.nj.nec.com/lerda99distributedmemory.html, URL
  • Bozga, M., Maler, O., Pnueli, A., Yovine, S., Some progress in the symbolic verification of timed automata (1997) Proceedings of the 9 Th International Conference on Computer Aided Verification (CAV'97) LNCS, 1254, pp. 179-190. , http://citeseer.nj.nec.com/bozga97some.html, Grumberg O. URL
  • Ranjan, R., Sanghavi, J., Brayton, R., Sangiovanni-Vincentelli, A., Binary decision diagrams on network of workstations (1996) In: International Conference on Computer Design, pp. 358-364. , http://citeseer.nj.nec.com/ranjan96binary.html, URL
  • Schapachnik, F., (2002) "Distributed and Parallel Verification of Real-Time Systems," Degree Thesis, Departamento de Computación, Facultad de Ciencias Exactas Y Naturales, Universidad de Buenos Aires, , http://www.cvi.com.ar/zeus/tesis_schapachnik.ps.gz, URL
  • Stern, U., Dill, D.L., Parallelizing the Murφ verifier (1997) In: Computer Aided Verification LNCS, 1254, pp. 256-278. , http://citeseer.nj.nec.com/stern97parallelizing.html, URL
  • Tripakis, S., Yovine, S., Verification of the fast reservation protocol with delayed transmission using the tool Kronos (1998) Proceedings of the 4th IEEE Real-Time Technology and Applications Symposium (RTAS'98, pp. 165-170. , http://citeseer.nj.nec.com/186425.html, URL

Citas:

---------- APA ----------
Braberman, V., Olivero, A. & Schapachnik, F. (2002) . Zeus: A distributed timed model-checker based on Kronos. PDMC 2002, Parallel and Distributed Model Checking (Satellite Workshop of CONCUR 2002), 68(4), 503-522.
http://dx.doi.org/10.1016/S1571-0661(05)80389-5
---------- CHICAGO ----------
Braberman, V., Olivero, A., Schapachnik, F. "Zeus: A distributed timed model-checker based on Kronos" . PDMC 2002, Parallel and Distributed Model Checking (Satellite Workshop of CONCUR 2002) 68, no. 4 (2002) : 503-522.
http://dx.doi.org/10.1016/S1571-0661(05)80389-5
---------- MLA ----------
Braberman, V., Olivero, A., Schapachnik, F. "Zeus: A distributed timed model-checker based on Kronos" . PDMC 2002, Parallel and Distributed Model Checking (Satellite Workshop of CONCUR 2002), vol. 68, no. 4, 2002, pp. 503-522.
http://dx.doi.org/10.1016/S1571-0661(05)80389-5
---------- VANCOUVER ----------
Braberman, V., Olivero, A., Schapachnik, F. Zeus: A distributed timed model-checker based on Kronos. Electron. Notes Theor. Comput. Sci. 2002;68(4):503-522.
http://dx.doi.org/10.1016/S1571-0661(05)80389-5