×

zbMATH — the first resource for mathematics

Models for reactivity. (English) Zbl 0790.68041
Summary: A hierarchy of models that capture realistic aspects of reactive, real- time, and hybrid systems is introduced. On the most abstract level, the qualitative (non-quantitative) model of reactive systems captures the temporal precedence aspect of time. A more refined model is that of real- time systems, which represents the metric aspect of time. The third and most detailed model is that of hybrid systems, which allows the incorporation of continuous components into a reactive system.
For each of the three levels, we present a computational model, a requirement specification language based on extensions of temporal logic, system description languages based on Statecharts and a textual programming language, proof rules for proving validity of properties, and examples of such proofs.

MSC:
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M., Lamport, L.: An old-fashioned recipe for real time. In: Bakker, J.W. de, Huizing, C., Roever, W.-P. de, Rozenberg, G. (eds.) Real-time: theory in practice. (Lect. Notes Comput. Sci., vol. 600, pp. 1-27) Berlin Heidelberg New York: Springer 1992
[2] Bernstein, A., Harter, P.K.: Proving real time properties of programs with temporal logic. In: Proceedings of the Eighth Symposium on Operating Systems Principles, pp. 1-11. New York: ACM 1981
[3] Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett.40(5), 269-276 (1992) · Zbl 0743.68097
[4] Dijkstra, E.W.: Guarded commands, nondeterminancy, and formal derivation of programs. Commun. ACM18(8), 453-457 (1975) · Zbl 0308.68017
[5] Dijkstra, E.W.: A discipline of programming. Englewood Cliffs, NJ: Prentice-Hall 1976 · Zbl 0368.68005
[6] Harel, D.: Statecharts: a visual approach to complex systems. Technical report, Department of Applied Mathematics, Weizmann Institute of Science CS84-05, 1984
[7] Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program.8, 231-274 (1987) · Zbl 0637.68010
[8] Henzinger, T.A.: The temporal specification and verification of real-time systems. PhD thesis, Stanford University, 1991
[9] Henzinger, T.A.: Sooner is safer than later. Inf. Process. Lett.43(3), 135-142 (1992) · Zbl 0753.68041
[10] Harel, E., Lichtenstein, O., Pnueli, A.: Explicit clock temporal logic. In: Proceedings of the 5th IEEE Symposium Logic in Computer Sciences, pp. 402-413, 1990
[11] Henzinger, T., Manna, Z., Pnueli, A.: Temporal proof methodologies for real-time systems. In: Proceedings of the 18th ACM Symposium Principle of Programming Languages, pp. 353-366, 1991
[12] Henzinger, T., Manna, Z., Pnueli, A.: Timed transition systems. In: Bakker, J.W. de, Huizing, C., Roever, W.-P. de, Rozenberg, G. (eds.) Real-time: theory in practice. (Lect. Notes Comput. Sci., vol. 600, pp. 226-251) Berlin Heidelberg New York: Springer 1992
[13] Koymans, R., Roever, W.-P. de: Examples of a real-time temporal logic specifications. In: Denvir, B.D., Harwood, W.T., Jackson, M.I., Wray, M.J. (eds.) The analysis of concurrent systems (Lect. Notes Comput. Sci., vol. 207, pp. 231-252) Berlin Heidelberg New York: Springer 1985
[14] Koymans, R.: Specifying real-time properties with metric temporal logic. Realtime Systems2(4), 255-299 (1990)
[15] Kesten, Y., Pnueli, A.: Age before beauty. Technical report, Department of Applied Mathematics, Weizmann Institute of Science, 1992
[16] Kesten, Y., Pnueli, A.: Timed and hybrid statecharts and their textual representation. In: Vytopil, J. (ed.) Formal techniques in real-time and fault-tolerant systems. (Lect. Notes Comput. Sci., vol. 571, pp. 591-619) Berlin Heidelberg New York: Springer 1992
[17] Koymans, R., Vytopyl, J., Roever, W.-P. de: Real-time programming and asynchronous message passing. In: Proceedings of the 2nd ACM Symposium Principles of Distribution Computer, pp. 187-197, 1983
[18] Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: Bakker, J.W. de, Huizing, C., Roever, W.-P. de, Rozenberg, G. (eds.) Real-time: theory in practice. (Lect. Notes Comput. Sci., vol. 600, pp. 447-484) Berlin Heidelberg New York: Springer 1992
[19] Manna, Z., Pnueli, A.: Proving precedence properties: the temporal way. In: Piloty, R., Barbacci, M., Borrione, D., Dietmeyer, D., Hill, F., Skelly, P. (eds.) CONLAN report. (Lect. Notes Comput. Sci., vol. 154, pp. 491-512) Berlin Heidelberg New York: Springer 1983
[20] Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci.83(1), 97-130 (1991) · Zbl 0795.68133
[21] Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: specification. Berlin Heidelberg New York: Springer 1991 · Zbl 0753.68003
[22] Manna, Z., Pnueli, A.: Time for concurrency. In: Bensoussan, A., Verjus, J.-P. (eds.) Future tendencies in computer science, control and applied mathematics (Lect. Notes Comput. Sci., Vol. 653, pp. 129-153) Berlin Heidelberg New York: Springer 1992
[23] Manna, Z., Pnueli, A.: Verifying hybrid systems. In: Ravn, A., Rischel, H. (eds.) Workshop on Hybrid Systems. (Lect. Notes Comput. Sci., to appear) Berlin Heidelberg New York: Springer 1993
[24] Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR ’90. Theories of Concurrency: unification and extension. (Lect. Notes Comput. Sci., vol. 458, pp. 401-415) Berlin Heidelberg New York: Springer 1990
[25] Nicollin, X., Sifakis, J., Yovine, S.: From ATP to timed graphs and hybrid systems. In: Bakker, J.W. de, Huizing, C., Roever, W.-P. de, Rozenberg, G. (eds.) Real-time: theory in practice. (Lect. Notes Comput. Sci., vol. 600, pp. 549-572) Berlin Heidelberg New York: Springer 1992 · Zbl 0790.68067
[26] Ostroff, J.S.: Temporal logic of real-time systems. Advanced Software Development Series. Taunton, England: Research Studies Press (John Wiley & Sons) 1990
[27] Pnueli, A., Harel, E.: Applications of temporal logic to the specification of real time systems. In: Joseph, M. (ed.) Formal techniques in real-time and fault-tolerant systems. (Lect. Notes Comput. Sci., vol. 331, pp. 84-98) Berlin Heidelberg New York: Springer 1988 · Zbl 0688.68024
[28] Pnueli, A.: How vital is liveness? In: Cleaveland, W.R. (ed.) CONCUR ’92. (Lect. Notes Comput. Sci., vol. 630, pp. 162-175) Berlin Heidelberg New York: Springer 1992
[29] Schneider, F.B., Bloom, B., Marzullo, K.: Putting time into proof outlines. In: Bakker, J.W. de, Huizing, C., Roever, W.-P. de, Rozenberg, G. (eds.) Real-time: theory in practice. (Lect. Notes Comput. Sci., vol. 600, 618-639) Berlin Heidelberg New York: Springer 1992
[30] Sifakis, J.: An overview and synthesis on timed process algebra. In: Larsen, K.G., Skou, A. (eds.) Computer aided verification. (Lect. Notes Comput. Sci., vol. 575, pp. 376-398) Berlin Heidelberg New York: Springer 1991
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.