Dealing with practical limitations of distributed timed model checking for timed automata
Two base algorithms are known for reachability verification over timed automata. They are called forward and backwards, and traverse the automata edges using either successors or predecessors. Both usually work with a data structure called Difference Bound Matrices (DBMs). Although forward is better...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , |
| Formato: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2006
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 11328caa a22011417a 4500 | ||
|---|---|---|---|
| 001 | PAPER-6991 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203643.0 | ||
| 008 | 190411s2006 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-33748311998 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 030 | |a FMSDE | ||
| 100 | 1 | |a Braberman, V. | |
| 245 | 1 | 0 | |a Dealing with practical limitations of distributed timed model checking for timed automata |
| 260 | |c 2006 | ||
| 270 | 1 | 0 | |m Braberman, V.; Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina; email: vbraber@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Aceto, L., Burgueno, A., Larsen, K.G., Model checking via reachability testing for timed automata (1998) Tools and Algorithms for Construction and Analysis of Systems (TACAS '98), pp. 263-280 | ||
| 504 | |a Alfonso, A., Braberman, V., Kicillof, N., Olivero, A., Visual timed event scenarios (2004) Proc. of the 26th ACM/IEEE International Conference on Software Engineering | ||
| 504 | |a Altisen, K., Tripakis, S., Tools for controller synthesis of timed systems (2002) RT-TOOLs | ||
| 504 | |a Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, I.I., An implementation of three algorithms for timing verification based on automata emptiness (1992) Proceedings of the 13th IEEE Real-time Systems Symposium, pp. 157-166. , Phoenix, Arizona | ||
| 504 | |a Alur, R., Courcoubetis, C., Dill, D.L., Model-checking in dense real-time (1993) Inform Comp, 104 (1), pp. 2-34 | ||
| 504 | |a Alur, R., Dill, D.L., A theory of timed automata (1994) Theor Comp Sci, 126 (2), pp. 183-235 | ||
| 504 | |a Barnat, J., Brim, L., Stríbřná, J., Distributed LTL model-checking in SPIN (2001) Proc. of the 8th International SPIN Workshop, pp. 200-216. , Dwyer MB (eds) Toronto, Canada | ||
| 504 | |a Behrmann, G., Distributed reachability analysis in timed automata (2005) Int J Softw Tools Technol Transf, 7 (1), pp. 19-30 | ||
| 504 | |a Behrmann, G., Hune, T., Vaandrager, F.W., Distributing timed model checking - How the search order matters (2000) LNCS, 1855, pp. 216-231. , Computer aided verification | ||
| 504 | |a Ben-David, S., Heyman, T., Grumberg, O., Schuster, A., Scalable distributed on-the-fly symbolic model checking (2000) Formal Methods in Computer-aided Design, pp. 390-404 | ||
| 504 | |a Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., UPPAAL - A tool suite for automatic verification of real-time systems (1995) Hybrid Systems, pp. 232-243 | ||
| 504 | |a Bollig, B., Leucker, M., Weber, M., Parallel model checking for the alternation free μ-calculus (2001) LNCS, 2031, pp. 543-558. , 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS '01) | ||
| 504 | |a Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S., Kronos: A model-checking tool for real-time systems (1998) LNCS, 1427, pp. 546-550. , Proc. of the 10th Intl. Conf. CAV '98 | ||
| 504 | |a Braberman, V., (2000) Modeling and Checking Real-time Systems Designs, , Phd. thesis, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires | ||
| 504 | |a Braberman, V., Garbervetsky, D., Olivero, A., ObsSlice: A timed automata slicer based on observers (2004) Proc of the 16th Intl Conf CAV '04 | ||
| 504 | |a Braberman, V., Olivero, A., Schapachnik, F., Zeus: A distributed timed model checker based on Kronos (2002) ENTCS, 68. , 1st workshop on parallel and distributed model checking, affiliated to CONCUR 2002 (13th International Conference on Concurrency Theory), Brno, Czech Republic | ||
| 504 | |a Braberman, V., Olivero, A., Schapachnik, F., Issues in distributed model-checking of timed automata: Building ZEUS (2004) Int J Softw Tools Technol Transf P. Online First | ||
| 504 | |a Braberman, V., Olivero, A., Schapachnik, F., On-the-fly workload prediction and redistribution in the distributed timed model checker ZEUS (2004) 3rd International Workshop on Parallel and Distributed Methods in Verification, , Affiliated to CONCUR 2004 (15th International Conference on Concurrency Theory London, UK | ||
| 504 | |a Cousot, P., (1978) Methodes Iteratives de Construction et D'Aptoximation 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 | ||
| 504 | |a Daws, C., Yovine, S., Reducing the number of clock variables of timed automata (1996) Proceedings IEEE Real-Time Systems Symposium (RTSS '96), pp. 73-81 | ||
| 504 | |a Dill, D.L., Timing assumptions and verification of finite-state concurrent systems (1990) LNCS, 407, pp. 197-212. , International workshop of automatic verification methods for finite state systems, Grenoble, France | ||
| 504 | |a 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. , Dwyer MB (ed) Toronto, Canada | ||
| 504 | |a Grumberg, O., Heyman, T., Schuster, A., Distributed symbolic model checking for μ.-calculus (2001) Computer Aided Verification, pp. 350-362 | ||
| 504 | |a Heljanko, K., Khomenko, V., Koutny, M., Parallelisation of the petri net unfolding algorithm (2002) Tools and Algorithms for Construction and Analysis of Systems (TACAS '02), pp. 371-385 | ||
| 504 | |a Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S., Symbolic model checking for real-time systems (1994) Inform Comput, 111 (2), pp. 193-244 | ||
| 504 | |a Heyman, T., Geist, D., Grumberg, O., Schuster, A., Achieving scalability in parallel reachability analysis of very large circuits (2002) Form Meth Syst des, 21 (2), pp. 317-338 | ||
| 504 | |a Krcal, P., Distributed explicit bounded LTL model checking (2003) ENTCS, 89. , Brim L, Grumberg O (eds) Electronic notes in theoretical computer science | ||
| 504 | |a Lerda, F., Sisto, R., Distributed-memory model checking with SPIN (1999) LNCS, 1680. , Proc. of the 5th International SPIN Workshop | ||
| 504 | |a Nicol, D.M., Ciardo, G., Automated parallelization of discrete state-space generation (1997) J Parallel Distr Comp, 47 (2), pp. 153-167 | ||
| 504 | |a Pnueli, A., Extracting controllers for timed automata (2005) Technical Report, , Department of Computer Science, Weizmann Institute of Science | ||
| 504 | |a Ranjan, R., Sanghavi, J., Brayton, R., Sangiovanni-Vincentelli, A., Binary decision diagrams on network of workstations (1996) International Conference on Computer Design, pp. 358-364 | ||
| 504 | |a 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 | ||
| 504 | |a Schloegel, K., Karypis, G., Kumar, V., A unified algorithm for load-balancing adaptive scientific simulations (2000) Technical Report, , University of Minnesota, Department of Computer Science/US Army HPC Research Center. Minneapolis, USA | ||
| 504 | |a Stern, U., Dill, D.L., Parallelizing the Murφ verifier (1997) LNCS, 1254, pp. 256-278. , Computer aided verification | ||
| 520 | 3 | |a Two base algorithms are known for reachability verification over timed automata. They are called forward and backwards, and traverse the automata edges using either successors or predecessors. Both usually work with a data structure called Difference Bound Matrices (DBMs). Although forward is better suited for on-the-fly construction of the model, the one known as backwards provides the basis for the verification of arbitrary formulae of the TCTL logic, and more importantly, for controller synthesis. Zeus is a distributed model checker for timed automata that uses the backwards algorithm. It works assigning each automata location to only one processor. This design choice seems the only reasonable way to deal with some complex operations involving many DBMs in order to avoid huge overheads due to distribution. This article explores the limitations of Zeus-like approaches for the distribution of timed model checkers. Our findings justify why close-to-linear speedups are so difficult -and sometimes impossible- to achieve in the general case. Nevertheless, we present mechanisms based on the way model checking is usually applied. Among others, these include model-topology-aware partitioning and on-the-fly workload redistribution. Combined, they have a positive impact on the speedups obtained. |l eng | |
| 536 | |a Detalles de la financiación: Inter-American Development Bank, OC/AR PICT 11738 | ||
| 536 | |a Detalles de la financiación: Secretaría de Ciencia y Técnica, Universidad de Buenos Aires, 2004 X020 | ||
| 536 | |a Detalles de la financiación: Consejo Nacional de Investigaciones Científicas y Técnicas | ||
| 536 | |a Detalles de la financiación: PI0509, TSI04B | ||
| 536 | |a Detalles de la financiación: 2005 | ||
| 536 | |a Detalles de la financiación: This research paper supported by BID OC/AR PICT 11738 grant. | ||
| 536 | |a Detalles de la financiación: V. Braberman: Research supported by UBACyT 2004 X020 and CONICET. | ||
| 536 | |a Detalles de la financiación: A. Olivero: Partially supported by UADE projects TSI04B and PI0509. | ||
| 536 | |a Detalles de la financiación: F. Schapachnik: Partially supported by an IDS 2003 grant and IBM Eclipse innovation award 2005. | ||
| 593 | |a Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina | ||
| 593 | |a Centro de Estudios Avanzados, FIyCE, Universidad Argentina de la Empresa, Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a DBM |
| 690 | 1 | 0 | |a DISTRIBUTED TIMED MODEL CHECKING |
| 690 | 1 | 0 | |a KRONOS |
| 690 | 1 | 0 | |a LOAD-BALANCE |
| 690 | 1 | 0 | |a REACHABILITY |
| 690 | 1 | 0 | |a RECONFIGURATION |
| 690 | 1 | 0 | |a REDISTRIBUTION |
| 690 | 1 | 0 | |a TIMED AUTOMATA |
| 690 | 1 | 0 | |a ZEUS |
| 690 | 1 | 0 | |a ALGORITHMS |
| 690 | 1 | 0 | |a CONTROL EQUIPMENT |
| 690 | 1 | 0 | |a DATA STRUCTURES |
| 690 | 1 | 0 | |a FORMAL LOGIC |
| 690 | 1 | 0 | |a PROGRAM PROCESSORS |
| 690 | 1 | 0 | |a TOPOLOGY |
| 690 | 1 | 0 | |a DIFFERENCE BOUND MATRICES (DBM) |
| 690 | 1 | 0 | |a DISTRIBUTED TIMED MODEL CHECKING |
| 690 | 1 | 0 | |a KRONOS |
| 690 | 1 | 0 | |a LOAD-BALANCE |
| 690 | 1 | 0 | |a REACHABILITY |
| 690 | 1 | 0 | |a RECONFIGURATION |
| 690 | 1 | 0 | |a REDISTRIBUTION |
| 690 | 1 | 0 | |a TIMED AUTOMATA |
| 690 | 1 | 0 | |a ZEUS |
| 690 | 1 | 0 | |a AUTOMATA THEORY |
| 700 | 1 | |a Olivero, A. | |
| 700 | 1 | |a Schapachnik, F. | |
| 773 | 0 | |d 2006 |g v. 29 |h pp. 197-214 |k n. 2 |p Formal Methods Syst Des |x 09259856 |t Formal Methods in System Design | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-33748311998&doi=10.1007%2fs10703-006-0012-3&partnerID=40&md5=d058cb476483056e2de7328c4a0d2444 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s10703-006-0012-3 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_09259856_v29_n2_p197_Braberman |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09259856_v29_n2_p197_Braberman |y Registro en la Biblioteca Digital |
| 961 | |a paper_09259856_v29_n2_p197_Braberman |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 67944 | ||