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