OBSSLICE: A timed automata slicer based on observers
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 ne...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , |
| Formato: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2004
|
| Acceso en línea: | Registro en Scopus Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 03720caa a22004817a 4500 | ||
|---|---|---|---|
| 001 | PAPER-4311 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203351.0 | ||
| 008 | 190411s2004 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-35048889598 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Braberman, V. | |
| 245 | 1 | 0 | |a OBSSLICE: A timed automata slicer based on observers |
| 260 | |c 2004 | ||
| 270 | 1 | 0 | |m Departamento de Computación - FCEyN, Universidad de Buenos AiresArgentina; email: vbraber@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Braberman, V., Garbervetsky, D., Olivero, A., Improving the verification of timed systems using influence information (2002) LNCS, 2280. , Proc. TACAS '02 | ||
| 504 | |a Alfonso, A., Braberman, V., Kicillof, N., Olivero, A., Visual timed event scenarios (2004) Proc. of the 26th ACM/IEEE ICSE '04, , to appear | ||
| 504 | |a Daws, C., Olivero, A., Tripakis, S., Yovine, S., The Tool KRONOS (1996) LNCS, 1066, pp. 208-219. , Proc. of Hybrid Systems III | ||
| 504 | |a Tripakis, S., (1998) L'Analyse Formelle des Systèmes Temporisés en Practique, , PhD thesis, Univesité Joseph Fourier | ||
| 504 | |a 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 | ||
| 504 | |a Braberman, V., Felder, M., Verification of real-time designs: Combining scheduling theory with automatic formal verification (1999) LNCS, 1687. , ESEC/FSE '99 | ||
| 504 | |a Braberman, V., (2000) Modeling and Checking Real-Time Systems Designs, , PhD thesis, FCEyN, Universidad de Buenos Aires | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Departamento de Computación - FCEyN, Universidad de Buenos Aires, Argentina | ||
| 593 | |a Centro de Estudios Avanzados, Universidad Argentina de la Empresa, Argentina | ||
| 690 | 1 | 0 | |a COMPUTER AIDED ANALYSIS |
| 690 | 1 | 0 | |a MODELLING ELEMENTS |
| 690 | 1 | 0 | |a OPTIMIZATION TOOLS |
| 690 | 1 | 0 | |a STATE-SPACE EXPLOSION |
| 690 | 1 | 0 | |a TIMED AUTOMATA |
| 690 | 1 | 0 | |a VERIFICATION TOOLS |
| 690 | 1 | 0 | |a AUTOMATA THEORY |
| 700 | 1 | |a Garbervetsky, D. | |
| 700 | 1 | |a Olivero, A. | |
| 773 | 0 | |d 2004 |g v. 3114 |h pp. 470-474 |p Lect. Notes Comput. Sci. |x 03029743 |w (AR-BaUEN)CENRE-983 |t Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-35048889598&partnerID=40&md5=199e6374b0c2a0820095ab604be8a496 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_03029743_v3114_n_p470_Braberman |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman |y Registro en la Biblioteca Digital |
| 961 | |a paper_03029743_v3114_n_p470_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 | ||
| 963 | |a VARI | ||
| 999 | |c 65264 | ||