Registro:
Documento: |
Artículo
|
Título: | On improving backwards verification of timed automata (extended abstract) |
Autor: | Braberman, V.; López Pombo, C.; Olivero, A. |
Ciudad: | Grenoble |
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: | Algorithms; Chaos theory; Formal logic; Iterative methods; Mathematical models; Mathematical operators; Semantics; Set theory; Backwards verification; Chaotic iteration; Fixpoint; Timed automata (TA); Finite automata |
Año: | 2002
|
Volumen: | 65
|
Número: | 6
|
Página de inicio: | 60
|
Página de fin: | 67
|
DOI: |
http://dx.doi.org/10.1016/S1571-0661(04)80469-9 |
Título revista: | Theory and Practice of Timed Systems (Satellite Event of ETAPS 2002)
|
Título revista abreviado: | Electron. Notes Theor. Comput. Sci.
|
ISSN: | 15710661
|
PDF: | https://bibliotecadigital.exactas.uba.ar/download/paper/paper_15710661_v65_n6_p60_Braberman.pdf |
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15710661_v65_n6_p60_Braberman |
Referencias:
- Alur, R., Courcoubetis, C., Dill, D., Model-Checking for Real-Time Systems (1993) Information and Computation, 104 (1), pp. 2-34
- Alur, R., Dill, D., A Theory of Timed Automata (1994) Theoretical Computer Science, 126, pp. 183-235
- Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., UPPAAL-A Tool Suite for the Automatic Verification of Real-Time Systems (1996) Proc. Hybrid Systems III, Lecture Notes on Computer Science 1066, pp. 232-243. , Springer Verlag
- Braberman, V., (2000) Modeling and Checking Real-time System Designs, , Ph.D. Thesis, Departamento de Computación, Universidad de Buenos Aires
- Braberman, V., Garbervetsky, D., Olivero, A., Improving the verification of timed systems using influence information Technical Report, TR2001-003. , http://www.dc.uba.ar/people/exclusivos/vbraber/tr01-003.ps, To appear in TACAS 2002. CS Department, FCEyN, Universidad de Buenos Aires
- 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 es Médicale de Grenoble, Institut National Polytechnique de Grenoble
- Daws, C., Olivero, A., Tripakis, S., Yovine, S., The Tool KRONOS (1996) Proc. of Hybrid Systems III, LNCS 1066, pp. 208-219. , Springer Verlag
- Dill, D., Timing assumptions and verification of finite-state concurrent systems (1989) Lecture Notes in Computer Science, 407, pp. 197-212. , Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Springer Verlag
- Elseaidy, W., Cleaveland, R., Baugh Jr., J., Modeling and Verifying Active Structural Control Systems (1997) Science of Computer Programming, 29 (1-2), pp. 99-122
- Henzinger, T.A., Ho, P.-H., Wong-Toi, H., HyTech: A model checker for hybrid systems (1997) Software Tools for Technology Transfer 1, pp. 110-122
- Kerbrat, A., Reachable state space analysis of lotos programs (1994) 7th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, , Bern, Switzerland, October
- Kang, I., Lee, I., Kim, Y.S., An efficient space generation for the analysis of real-time systems (1996) Proceedings of the International Symposium on Software Testing and Analysis
- (1999) Trans. on Software Engineering
- Pombo, L., C., G., (2001) Mejoras a Un Algoritmo de Model Checking Simbólico, Basadas en la Topología de Los Sistemas de Tiempo Real, , Bachelor in Computer Science Thesis. Departamento de Computación, Facultad de ciencias exactas y naturales, Universidad de Buenos Aires
- Karypis, G., Kumar, V., Multilevel algorithms for multi-constraint graph partitioning (1998) Proceedings of 10th Supercomputing Conference
- Nicollin, X., Sifakis, J., Yovine, S., Compiling Real-Time Specification into Extended Automata (1992) IEEE Trans. on Soft. Eng., Special Issue on Real-Time Systems, 189, pp. 794-804
- Tripakis, S., (1998) L'Analyse Formelle des Systemés Temporisés en Practique, , Phd. Thesis, Univesité Joseph Fourier, December
- Wang, F., RED: Model-checker for timed automata with clock-restriction diagram 2nd Workshop on Models for Timed Critical Systems 2001, , To be published in Electronic Notes in Theoretical Computer Science
- Yovine, S., (1993) Méthodes et Outils Pour la Vérification Symbolique de Systemès Temporisés, , Ph.D Thesis, Institut National Polytechnique de Grenoble
- Yovine, S., Model-Checking Timed Automata (1998) Embedded Systems, 1494. , G. Rozemberg, Vaandrager F. Lecture Notes in Computer Science, Springer Verlag
Citas:
---------- APA ----------
Braberman, V., López Pombo, C. & Olivero, A.
(2002)
. On improving backwards verification of timed automata (extended abstract). Theory and Practice of Timed Systems (Satellite Event of ETAPS 2002), 65(6), 60-67.
http://dx.doi.org/10.1016/S1571-0661(04)80469-9---------- CHICAGO ----------
Braberman, V., López Pombo, C., Olivero, A.
"On improving backwards verification of timed automata (extended abstract)"
. Theory and Practice of Timed Systems (Satellite Event of ETAPS 2002) 65, no. 6
(2002) : 60-67.
http://dx.doi.org/10.1016/S1571-0661(04)80469-9---------- MLA ----------
Braberman, V., López Pombo, C., Olivero, A.
"On improving backwards verification of timed automata (extended abstract)"
. Theory and Practice of Timed Systems (Satellite Event of ETAPS 2002), vol. 65, no. 6, 2002, pp. 60-67.
http://dx.doi.org/10.1016/S1571-0661(04)80469-9---------- VANCOUVER ----------
Braberman, V., López Pombo, C., Olivero, A. On improving backwards verification of timed automata (extended abstract). Electron. Notes Theor. Comput. Sci. 2002;65(6):60-67.
http://dx.doi.org/10.1016/S1571-0661(04)80469-9