Navegar

Colección

Datos Estadísticas

Artículo

Este artículo es de Acceso Abierto y puede ser descargado en su versión final desde nuestro repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

We introduce the notion of Timed I/O Components as Timed Automata "á la" Alur & Dill where an "admissible" I/O interface is declared. That notion has, what we consider, a key modeling property: non-zeno preservation under syntactically-checkable "I/O compatibility" among interacting components. Also a reduced parallel composition is posssible based on the ability of statically detect influence of behavior between components [8,10,11]. On the other hand, with some simple extra conditions, modular assume-guarantee style of reasoning like [15,19] is valid in our model. © 2002 Published by Elsevier Science B. V.

Registro:

Documento: Artículo
Título:Extending timed automata for compositional modeling healthy timed systems
Autor:Braberman, V.; Olivero, A.
Ciudad:Firenze
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:Automata theory; Mathematical models; Statistical methods; Compositional modeling; Key modeling; Timed Automata; Computer programming languages
Año:2002
Volumen:52
Número:3
Página de inicio:227
Página de fin:245
DOI: http://dx.doi.org/10.1016/S1571-0661(04)00226-9
Título revista:QAPL'01, Quantitative Aspects of Programming Languages (Satellite Event of PLI 2001)
Título revista abreviado:Electron. Notes Theor. Comput. Sci.
ISSN:15710661
PDF:https://bibliotecadigital.exactas.uba.ar/download/paper/paper_15710661_v52_n3_p227_Braberman.pdf
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15710661_v52_n3_p227_Braberman

Referencias:

  • Alpern, B., Schneider, F., Verifying Temporal Properties without Temporal Logic (1989) ACM Trans. Programming Languages and Systems, 11 (1), pp. 147-167
  • Alur, R., (1991) Techniques for Automatic Verification of Real-time Systems, , Ph.D. thesis, Stanford University
  • Alur, R., Courcoubetis, C., Dill, D., Model-checking for real-time systems (1990) Proceedings of Logic in Computer Science, pp. 414-425. , IEEE Computer Society, Los Alamitos, Calif
  • (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
  • Alur, R., Henzinger, T., Modularity for timed and hybrid systems (1997) LNCS, 1243. , Proceedings of CONCUR'97
  • Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., UPPAAL- a tool suite for the automatic verification of real- time systems (1996) LNCS, 1066, pp. 232-243. , Proceedings of Hybrid Systems III Springer Verlag
  • Bornot, S., Sifakis, J., An algebraic framework for urgency Information and Computation, , To appear in Academic Press
  • Braberman, V., (2000) Modeling and Checking Real-time System Designs, , Ph.D Thesis, Universidad de Buenos Aires [Thesis]
  • Braberman, V., Felder, M., Verification of real-time designs: Combining scheduling theory with automatic formal verification (1999) LNCS, 1687, pp. 494-510. , Proceedings of 7th European Conf. on Software Eng./ 7th ACM SIGSOFT Symposium on the Foundations of Software Eng., (ESEC/FSE 99) Springer Verlag, Sept
  • Braberman, V., Garbervetski, D., Olivero, A., Improving the verification of timed systems using influence information TACAS 2002, , Submitted to
  • Braberman, V., Garbervetski, D., Olivero, A., Influence information to improve the verification of timed systems Tech. Report, DC-UBA 2001-003
  • Clarke, E., Grumberg, O., Peled, D., (2000) "model Checking", p. 330. , MIT Press
  • Daws, C., Olivero, A., Tripakis, S., Yovine, S., The tool KRONOS (1996) LNCS, 1066, pp. 208-219. , Proceedings of Hybrid Systems III Springer Verlag
  • De Alfaro, L., Henzinger, T.A., Interface theories for component-based design (2001) LNCS, 2211, pp. 148-165. , Proceedings of EMSOFT 01: Embedded Software Springer Verlag
  • Gawlick, R., Segala, R., Sogaard-Andersen, J., Lynch, N., Liveness in timed and untimed systems (1994) LNCS, 820, pp. 166-177. , Proceedings of ICALP Springer Verlag
  • (1998) Information and Computation
  • Garbervetsky, G., (2000) Un Método de Reducción para la Composición de Sistemas Temporizados, , Master Thesis, Universidad de Buenos Aires
  • Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S., Symbolic model checking for real-time systems (1994) Information and Computation, 111 (2), pp. 193-244
  • Larsen, K.G., Laroussinie, F., CMC: A tool for compositional model-checking of real-time systems (1998) Proceedings of FORTE-PSTV'98, pp. 439-456. , Kluwer Academic Publishers
  • Kurshan, R.P., Tasiran, S., Alur, R., Brayton, R.K., Verifying abstractions of timed systems (1996) LNCS, 1119. , Proceedings CONCUR 96 Springer Verlag
  • Merritt, M., Modugno, F., Tuttle, M., Time constrained automata (1991) LNCS, 527. , Proceedings of CONCUR'91 Springer Verlag
  • Nicollin, X., Sifakis, J., Yovine, S., Compiling Real-Time Specification into Extended Automata (1992) IEEE Trans. on Soft. Eng, 18 (9), pp. 794-804
  • Springintveld, J., Vaandrager, F., D'argenio, P., Testing timed automata (2001) Theoretical Computer Science, 254 (1-2), pp. 225-257. , To appear in
  • Tripakis, S., (1998) L'Analyse Formelle des Systemès Temporisés en Practique, , Phd. Thesis, Univesité Joseph Fourier, December
  • Vaandrager, F., Lynch, N., Action transducers and timed automata (1992) LNCS, 630, pp. 436-455. , Proceedings of CONCUR'92
  • Yi, W., Real-time behavior of asynchronous agents (1990) LNCS, 458, pp. SpringerVerlag. , Proceedings of CONCUR'90
  • Yovine, S., Model-Checking Timed Automata (1998) Embedded Systems, , G. Rozemberg F. Vaandrager Springer Verlag LNCS 1494

Citas:

---------- APA ----------
Braberman, V. & Olivero, A. (2002) . Extending timed automata for compositional modeling healthy timed systems. QAPL'01, Quantitative Aspects of Programming Languages (Satellite Event of PLI 2001), 52(3), 227-245.
http://dx.doi.org/10.1016/S1571-0661(04)00226-9
---------- CHICAGO ----------
Braberman, V., Olivero, A. "Extending timed automata for compositional modeling healthy timed systems" . QAPL'01, Quantitative Aspects of Programming Languages (Satellite Event of PLI 2001) 52, no. 3 (2002) : 227-245.
http://dx.doi.org/10.1016/S1571-0661(04)00226-9
---------- MLA ----------
Braberman, V., Olivero, A. "Extending timed automata for compositional modeling healthy timed systems" . QAPL'01, Quantitative Aspects of Programming Languages (Satellite Event of PLI 2001), vol. 52, no. 3, 2002, pp. 227-245.
http://dx.doi.org/10.1016/S1571-0661(04)00226-9
---------- VANCOUVER ----------
Braberman, V., Olivero, A. Extending timed automata for compositional modeling healthy timed systems. Electron. Notes Theor. Comput. Sci. 2002;52(3):227-245.
http://dx.doi.org/10.1016/S1571-0661(04)00226-9