Navegar

Colección

Datos Estadísticas

Conferencia

Braberman, V.; Pieniazek, F.; IEEE Computer Society Technical Committee on Software Engineering "Duration properties over real time system designs" (2000) 10th International Workshop on Software Specification and Design, IWSSD 2000:51-61
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor

Abstract:

Constraints on the accumulated sojourn time at partic ular system states are among the possible requirements for a real-time system. These requirements are called dura tion properties. The need to predict temporal behavior of critical real-time systems has encouraged the development of a useful collection of results for run-time scheduling as well as an interesting set of formal automatic techniques based on model-checking. However, no automatic technique directly supports the verification of duration requirements over physical designs of real-time software. In [6] it is pre sented an approach that applies known scheduling theory to automatically derive simple and compositional formal mod els based on timed automata [1 ]. In this article, we com bine that modeling method with a conservative algorithm that extends [5] to check duration properties over the result ing timed automata. © 2000 IEEE.

Registro:

Documento: Conferencia
Título:Duration properties over real time system designs
Autor:Braberman, V.; Pieniazek, F.; IEEE Computer Society Technical Committee on Software Engineering
Filiación:Dep. de Computatión FCEyN, Universidad de Buenos Aires, Argentina
Palabras clave:Automata; Duration properties; Model-checking; Real-time system designs; Automata theory; Design; Interactive computer systems; Model checking; Scheduling; Specifications; Systems analysis; Verification; Automata; Automatic technique; Duration properties; Physical design; Real-time software; Run-time scheduling; Scheduling theory; Temporal behavior; Real time systems
Año:2000
Página de inicio:51
Página de fin:61
DOI: http://dx.doi.org/10.1109/IWSSD.2000.891126
Título revista:10th International Workshop on Software Specification and Design, IWSSD 2000
Título revista abreviado:Int. Workshop Softw. Specif. Des., IWSSD
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_07695088_v_n_p51_Braberman

Referencias:

  • Alur, R., Dill, D., A theory of timed automata (1994) Theoretical Comp. Science, 126, pp. 183-235
  • Audsley, N.C., Burns, A., Richardson, M.F., Wellings, A.J., STRESS: A simulator for hard real-time systems (1994) Software Practice and Experience
  • Avrunin, G.S., Corbett, J.C., Dillon, L.K., Analyzing partially implemented real-time systems (1998) IEEE Trans. Software Eng., 24 (8)
  • Braberman, V., (2000) Modeling and Checking Real-Time System Designs, , Phd. Thesis, Universidad de Buenos Aires
  • Braberman, V., Van Hung, D., On checking timed automata for linear duration invariants (1998) Proc. Real Time Systems Symp. (RTSS'98), , IEEE Computer Soc. Press, Los Alamitos, Calif
  • Braberman, V., Felder, M., Verification of real-time designs: Combining scheduling theory with automatic formal verification (1999) Proc. ESEC/FSE'99 LNCS, 1687, pp. 494-510
  • Buttazzo, G., (1997) Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications, , Kluwer Pub., Boston
  • Campos, S., Clarke, E., Marrero, W., Minea, M., VERUS: A tool for quantitative analysis of finite state real-time systems (1995) Proc. of SIGPLAN Work-shop on Lang., Compilers and Tools for Real-Time Systems
  • Felder, M., Pezze, M., A formal approach to the design of real-time systems (1997) Workshop KIT125
  • Fredette, A.N., Cleaveland, R., RTSL: A formal language for real-time schedulability analysis (1993) Proc. IEEERTSS'93, pp. 274-283. , Dec
  • Hopcroft, J.E., Ulman, J.D., (1979) Introduction to Automata Theory, Languages and Computation, , Adison-Wesley
  • Humprey, M., Stankovic, J., CAISARTS: A tool for real-time scheduling assistance (1995) Proc. IEEE RTSS'95
  • Jahanian, F., Stuart, D., A method for verifying properties of modechart specifications (1988) Proc. IEEE RTSS'88
  • Kang, I., Lee, I., Kim, Y.S., An efficient space generation for the analysis of Real-Time systems (1996) Proc. of ISSTA'96
  • Kesten, Y., Pnueli, A., Sifakis, J., Yovine, S., Decidable integration graphs (1999) Information and Computation, 150 (2), pp. 209-243. , Academic Press
  • (1992) LNCS, 736
  • Klein, M.H., Ralya, T., Pollak, P., Obenza, R., Harbour, M.G., (1993) A Practitioner's Handbook for Real-Time Analysis - Guide to Rate Monotonic Analysis for Real Time Systems, , SEI, Kluwer Pub
  • Lam, W., Brayton, R.K., Alternating rq timed automata (1993) Proc. CAV'93, LNCS, 697
  • Pieniazek, F., Braberman, V., On checking finitary timed automata for duration properties (1999) Tech. Rep. UBA, TR99-007, , http://www.dc.uba.ar/people/proyinv/tr.html
  • Sokolsky, O., Lee, I., Ben-Abdallah, H., Specification and analysis of real-time systems with PARAGON (1999) Annals of Software Eng.
  • Tripakis, S., Yovine, S., Analysis of timed systems based on time-abstracting bisimulations (2000) Formal Methods in System Design, , To appear in, Kluwer Pub
  • Vestal, S., Modeling and verification of real-time software using extended linear hybrid automata (2000) 5th NSAS Langley Formal Methods Workshop
  • Xuan Dong, L., Van Hung, D., Checking linear duration invariants by linear programming (1996) Concurrency and Paralellism, Prog., Networking, and Security, LNCS, 1179
  • Zhou, C., Hoare, C.A.R., Ravn, A.P., A calculus of durations (1991) Information Processing Letters, 40 (5)A4 - IEEE Computer Society Technical Committee on Software Engineering

Citas:

---------- APA ----------
Braberman, V., Pieniazek, F. & IEEE Computer Society Technical Committee on Software Engineering (2000) . Duration properties over real time system designs. 10th International Workshop on Software Specification and Design, IWSSD 2000, 51-61.
http://dx.doi.org/10.1109/IWSSD.2000.891126
---------- CHICAGO ----------
Braberman, V., Pieniazek, F., IEEE Computer Society Technical Committee on Software Engineering "Duration properties over real time system designs" . 10th International Workshop on Software Specification and Design, IWSSD 2000 (2000) : 51-61.
http://dx.doi.org/10.1109/IWSSD.2000.891126
---------- MLA ----------
Braberman, V., Pieniazek, F., IEEE Computer Society Technical Committee on Software Engineering "Duration properties over real time system designs" . 10th International Workshop on Software Specification and Design, IWSSD 2000, 2000, pp. 51-61.
http://dx.doi.org/10.1109/IWSSD.2000.891126
---------- VANCOUVER ----------
Braberman, V., Pieniazek, F., IEEE Computer Society Technical Committee on Software Engineering Duration properties over real time system designs. Int. Workshop Softw. Specif. Des., IWSSD. 2000:51-61.
http://dx.doi.org/10.1109/IWSSD.2000.891126