Artículo
Braberman, V.; Obes, J.L.; Olivero, A.; Schapachnik, F. "Hypervolume approximation in timed automata model checking" (2007) 5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007. 4763 LNCS:69-81
Consulte la política de Acceso Abierto del editor
Abstract:
Difference Bound Matrices (DBMs) are the most commonly used data structure for model checking timed automata. Since long they are being used in successful tools like KRONOS or UPPAAL. As DBMs represent convex polyhedra in an n-dimensional space, this paper explores the idea of using its hypervolume as the basis for two optimization techniques. One of them is very simple to implement. The other, an improvement over the first, requires more involved programming. Each of them saves verification time (up to 19% in our case studies), with a modest increase of memory requirements. Their impact differs among the different case studies but, as they can be combined, there is no need to choose a priori. © Springer-Verlag Berlin Heidelberg 2007.
Registro:
| Documento: | Artículo |
| Título: | Hypervolume approximation in timed automata model checking |
| Autor: | Braberman, V.; Obes, J.L.; Olivero, A.; Schapachnik, F. |
| Ciudad: | Salzburg |
| Filiación: | Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina CONICET Facultad de Ingeniería y Cs. Exactas, Universidad Argentina de la Empresa, Buenos Aires, Argentina |
| Palabras clave: | Automata theory; Computer aided software engineering; Data structures; Verification; Difference Bound Matrices; Hypervolume approximation; Timed automata; Model checking |
| Año: | 2007 |
| Volumen: | 4763 LNCS |
| Página de inicio: | 69 |
| Página de fin: | 81 |
| Título revista: | 5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman |
Referencias:
- Alur, R., Dill, D.L., A theory of timed automata (1994) Theoretical Computer Science, 126 (2), pp. 183-235
- Bouajjani, A., Tripakis, S., Yovine, S., On-the-Fly Symbolic Model-Checking for Real-Time Systems (1997) 18th IEEE Real-Time Systems Symposium (RTSS '97), , San Francisco, USA, IEEE Computer Scienty Press, Los Alamitos
- Behrmann, G., Bouyer, P., Larsen, K., Pelnek, R., Lower and upper bounds in zone based abstractions of timed automata (2004) LNCS, 2988, pp. 312-326. , Jensen, K, Podelski, A, eds, TACAS 2004, Springer, Heidelberg
- Behrmann, G., David, A., Larsen, K.G., Yi, W., Unification & sharing in timed automata verification (2003) LNCS, 2648, pp. 225-229. , Ball, T, Rajamani, S.K, eds, Model Checking Software, Springer, Heidelberg
- Bengtsson, J., Reducing memory usage in symbolic state-space exploration for timed systems (2001), Technical Report 2001-009, Department of Information Technology, Uppsala University; 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. , IEEE Computer Society Press, Los Alamitos
- Wang, F., Efficient verification of timed automata with BDD-like data-structures (2002) LNCS, 2575, pp. 189-205. , Zuck, L.D, Attie, P.C, Cortesi, A, Mukhopadhyay, S, eds, VMCAI 2003, Springer, Heidelberg
- Braberman, V., Garbervetsky, D., Olivero, A.: ObsSlice: A timed automata slicer based on observers. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, 3114, Springer, Heidelberg (2004); Braberman, V., Olivero, A., Schapachnik, F., Optimizing timed automata model checking via clock reordering (2006) 27th IEEE International Real-Time Systems Symposium, , Work in Progress Session, IEEE, Los Alamitos
- Balarin, F., Approximate reachability analysis of timed automata (1996) Proceedings of the 17th IEEE Real-Time Systems Symposium (RTSS '96), p. 52. , IEEE Computer Society, Washington, DC, USA
- Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, 1427, pp. 546-550. Springer, Heidelberg (1998); 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. , Springer, Heidelberg
- Dill, D.L., Timing assumptions and verification of finite-state concurrent systems (1990) LNCS, 407, pp. 197-212. , Sifakis, J, ed, Automatic Verification Methods for Finite State Systems, Springer, Heidelberg
- Yovine, S., Model checking timed automata (1998) LNCS, 1494. , Rozenberg, G, ed, Lectures on Embedded Systems, Springer, Heidelberg
- Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., Compact data structures and state-space reduction for model-checking real-time systems (2003) Real-Time Syst, 25 (2-3), pp. 255-275
- van Emde Boas, P., Kaas, R., Zijlstra, E., Design and implementation of an efficient priority queue (1977) Mathematical Systems Theory, 10, pp. 99-127
- Braberman, V., Olivero, A., Schapachnik, F., Issues in Distributed Model-Checking of Timed Automata: Building ZEUS (2005) International Journal of Software Tools for Technology Transfer, 7, pp. 4-18
- Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H., 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, pp
- Braberman, V., (2000) Modeling and Checking Real-Time Systems Designs, , Ph d. thesis, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires
Citas:
---------- APA ----------
Braberman, V., Obes, J.L., Olivero, A. & Schapachnik, F. (2007) . Hypervolume approximation in timed automata model checking. 5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007, 4763 LNCS, 69-81.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman [ ]
---------- CHICAGO ----------
Braberman, V., Obes, J.L., Olivero, A., Schapachnik, F. "Hypervolume approximation in timed automata model checking" . 5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007 4763 LNCS (2007) : 69-81.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman [ ]
---------- MLA ----------
Braberman, V., Obes, J.L., Olivero, A., Schapachnik, F. "Hypervolume approximation in timed automata model checking" . 5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007, vol. 4763 LNCS, 2007, pp. 69-81.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman [ ]
---------- VANCOUVER ----------
Braberman, V., Obes, J.L., Olivero, A., Schapachnik, F. Hypervolume approximation in timed automata model checking. Lect. Notes Comput. Sci. 2007;4763 LNCS:69-81.Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4763LNCS_n_p69_Braberman [ ]
