Artículo
Braberman, V.; Garbervetsky, D.; Olivero, A. "OBSSLICE: A timed automata slicer based on observers" (2004) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3114:470-474
Consulte la política de Acceso Abierto del editor
Abstract:
OBSSLICE is an optimization tool suited for the verification of timed automata using virtual observers. It discovers the set of modelling elements that can be safely ignored at each location of the observer by synthesizing behavioral dependence information among components. OBSSLlCE is fed with a network of timed automata and generates a transformed network which is equivalent to the one provided up to branching-time observation. Preliminary results have proven that eliminating irrelevant activity mitigates state space explosion and has a positive -and sometimes dramatic- impact on the performance of verification tools in terms of time, size and counterexample length. © Springer-Verlag Berlin Heidelberg 2004.
Registro:
| Documento: | Artículo |
| Título: | OBSSLICE: A timed automata slicer based on observers |
| Autor: | Braberman, V.; Garbervetsky, D.; Olivero, A. |
| Filiación: | Departamento de Computación - FCEyN, Universidad de Buenos Aires, Argentina Centro de Estudios Avanzados, Universidad Argentina de la Empresa, Argentina |
| Palabras clave: | Computer aided analysis; Modelling elements; Optimization tools; State-space explosion; Timed Automata; Verification tools; Automata theory |
| Año: | 2004 |
| Volumen: | 3114 |
| Página de inicio: | 470 |
| Página de fin: | 474 |
| Título revista: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman |
Referencias:
- Braberman, V., Garbervetsky, D., Olivero, A., Improving the verification of timed systems using influence information (2002) LNCS, 2280. , Proc. TACAS '02
- Alfonso, A., Braberman, V., Kicillof, N., Olivero, A., Visual timed event scenarios (2004) Proc. of the 26th ACM/IEEE ICSE '04, , to appear
- Daws, C., Olivero, A., Tripakis, S., Yovine, S., The Tool KRONOS (1996) LNCS, 1066, pp. 208-219. , Proc. of Hybrid Systems III
- Tripakis, S., (1998) L'Analyse Formelle des Systèmes Temporisés en Practique, , PhD thesis, Univesité Joseph Fourier
- Behrmann, G., David, A., Larsen, K., Möller, O., Pettersson, P., Yi, W., UPPAAL - Present and future (2001) Proc. IEEE CDC '01, , IEEE Computer Society Press
- Braberman, V., Felder, M., Verification of real-time designs: Combining scheduling theory with automatic formal verification (1999) LNCS, 1687. , ESEC/FSE '99
- Braberman, V., (2000) Modeling and Checking Real-Time Systems Designs, , PhD thesis, FCEyN, Universidad de Buenos Aires
Citas:
---------- APA ----------
Braberman, V., Garbervetsky, D. & Olivero, A. (2004) . OBSSLICE: A timed automata slicer based on observers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3114, 470-474.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman [ ]
---------- CHICAGO ----------
Braberman, V., Garbervetsky, D., Olivero, A. "OBSSLICE: A timed automata slicer based on observers" . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3114 (2004) : 470-474.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman [ ]
---------- MLA ----------
Braberman, V., Garbervetsky, D., Olivero, A. "OBSSLICE: A timed automata slicer based on observers" . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3114, 2004, pp. 470-474.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman [ ]
---------- VANCOUVER ----------
Braberman, V., Garbervetsky, D., Olivero, A. OBSSLICE: A timed automata slicer based on observers. Lect. Notes Comput. Sci. 2004;3114:470-474.Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman [ ]
