Compositional semantics for real-time distributed computing. (English) Zbl 0669.68055
A method to define the semantics of programs written in real-time languages is developed for the language Mini CSP-R. It takes in account the communication between several processes, parallel commands and real- time problems. The meaning of Mini CSP-R commands is defined denotationally by relating the meaning of each construct to the meaning of its components. The authors compare their method with some another methods of defining the semantics. As an appendix, the paper contains the comparison of the languages Mini CSP-R and CSP-R. As another appendix, it points out the simulation of the languages ADA in CSP-R.
Reviewer: M.Jůza
MSC:
| 68Q55 | Semantics in the theory of computing |
| 68N25 | Theory of operating systems |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Ada, The Programming Language Ada Reference Manual, (Lecture Notes in Comput. Sci., Vol. 155 (1983), Springer-Verlag: Springer-Verlag New York/Berlin) |
| [2] | Berry, G.; Cosserat, L., The ESTEREL synchronous programming language and its mathematical semantics, (Seminar on Concurrency. Seminar on Concurrency, July 1984, Carnegie-Mellon University. Seminar on Concurrency. Seminar on Concurrency, July 1984, Carnegie-Mellon University, Lecture Notes in Comput. Sci., Vol. 197 (1985), Springer-Verlag: Springer-Verlag New York/Berlin), 389-448 · Zbl 0599.68023 |
| [3] | Bernstein, A.; Harter, P. K., Proving real-time properties of programs with temporal logic, (8th ACM Symp. on Operating Systems Principles (1981)), 1-11 |
| [4] | Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. Assoc. Comput. Mach., 31, 560-599 (1984) · Zbl 0628.68025 |
| [5] | Barringer, H.; Kuiper, R.; Pnueli, A., Now you may compose temporal logic specifications, (16th ACM Symp. Theory of Comput. (1984)), 51-63 |
| [6] | Branquart, P.; Louis, G.; Wodon, P., An analytical description of CHILL, the CCITT high level language VI, (Lecture Notes in Comput. Sci., Vol. 128 (1982), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0474.68001 |
| [7] | (Bjørner, D.; Oest, O. N., Towards a Formal Description of Ada. Towards a Formal Description of Ada, Lecture Notes in Comput. Sci., Vol. 98 (1980), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0451.68015 |
| [8] | Boucher, A., (D. Phil. thesis (1986), Department of Computer Science, University of Oxford) |
| [9] | CACM, A case study: The space shuttle software system, Comm. ACM, 27, No. 9 (1984) |
| [10] | Camerini, J., Sémantique Mathématique de Primitives Temps Reel, (Thèse de 3ième cycle (1982), IMA, Université de Nice) |
| [11] | Dijkstra, E. W., Communication with an Automatic Computer, (Ph.D. thesis (1959), Mathematical Centre: Mathematical Centre Amsterdam) · Zbl 0492.68049 |
| [12] | Francez, N.; Lehmann, D.; Pnueli, A., A linear-history semantics for languages for distributed programming, Theoret. Comput. Sci., 32, 25-46 (1984) · Zbl 0543.68019 |
| [13] | Gerth, R.; Boucher, A., A timed failures model for extended communicating processes, (14th Int. Colloq. Automata. Lang. Programming. 14th Int. Colloq. Automata. Lang. Programming, Lecture Notes in Comput. Sci., Vol. 267 (1987), Springer-Verlag: Springer-Verlag New York/Berlin), 95-114 · Zbl 0623.68022 |
| [14] | Gerth, R., A maximal parallelism semantics for Occam, notes (1985) |
| [15] | Harel, D., Statecharts: A visual formalism for complex systems, Sci. Comput. Programming, 8, 231-274 (1987) · Zbl 0637.68010 |
| [16] | Huizing, C.; Gerth, R.; de Roever, W. P., Full abstraction of a real-time denotational semantics for an OCCAM-like language, (14th ACM Principles of Programming Lang (1987)), 223-237 |
| [17] | Hehner, E. C.R.; Hoare, C. A.R., A more complete model of communicating processes, Theoret. Comput. Sci., 26, 105-120 (1983) · Zbl 0513.68020 |
| [18] | Halpern, J. Y.; Megiddo, N.; Munshi, A. A., (Optimal Precision in the Presence of Uncertainty (1985), IBM Research Lab: IBM Research Lab San Jose) · Zbl 0598.68033 |
| [19] | Hoare, C. A.R., Communicating sequential processes, Comm. ACM, 21, No. 8 (1978) · Zbl 0383.68028 |
| [20] | Hooman, J., A compositional proof theory for real-time distributed message passing, (Proceedings of PARLE. Proceedings of PARLE, Lecture Notes in Comput. Sci., Vol. 259 (1987), Springer-Verlag: Springer-Verlag New York/Berlin), 315-332, Vol. II · Zbl 0615.68024 |
| [21] | Hooman, J., A compositional proof-system for an OCCAM-like real-time language, (Computing Science Notes 87/14 (1988), Department of Mathematics and Computing Science, Eindhoven University of Technology) |
| [22] | Jones, G., D.Phil. thesis (1982), Oxford, unpublished |
| [23] | Koymans, R., Denotational semantics for real-time programming constructs in concurrent languages, notes (1984) |
| [24] | Koymans, R.; Vytopil, J.; de Roever, W. P., Real-time programming and asynchronous message passing, (2nd ACM Principles of Distrib. Comput. (1983)), 187-197 |
| [25] | Misra, J.; Chandy, K. M., Proofs of networks of processes, IEEE Trans. Software Engrg., SE-7, No. 4, 417-426 (1981) · Zbl 0468.68030 |
| [26] | Milner, R., An approach to the semantics of parallel programs, (Proceedings, Convegno di Informatica Teorica. Proceedings, Convegno di Informatica Teorica, Pisa (1973)) |
| [27] | Milner, R., Calculi for synchrony and asynchrony, Theoret. Comput. Sci., 25, 267-310 (1983) · Zbl 0512.68026 |
| [28] | OCCAM, (The Occam Language Reference Manual (1984), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ) |
| [29] | Salwicki, A.; Müldner, T., On the algorithmic properties of concurrent programs, (Lecture Notes in Comput. Sci., Vol. 125 (1981), Springer-Verlag: Springer-Verlag New York/Berlin), 169-197 · Zbl 0472.68012 |
| [30] | Shyamasundar, R. K.; de Roever, W. P., Semantics of real-time Ada, notes (1983) |
| [31] | Zwiers, J.; de Roever, W. P.; van Emde Boas, P., Compositionality and concurrent networks: Soundness and completeness of a proofsystem, (12th Int. Colloq. Automata. Lang. Programming. 12th Int. Colloq. Automata. Lang. Programming, Lecture Notes in Comput. Sci., Vol. 194 (1985), Springer-Verlag: Springer-Verlag New York/Berlin), 509-519 · Zbl 0566.68014 |
| [32] | Zwiers, J., Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and Their Connection, (Ph.D. thesis (1988), Eindhoven University of Technology) · Zbl 0667.68020 |
| [33] | Zijlstra, E., Real-Time Semantics, (Master thesis (1984), University of Amsterdam) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
