×

zbMATH — the first resource for mathematics

The timed failures – Stability model for CSP. (English) Zbl 0912.68038
Summary: We present a mathematical model which is the most abstract allowing (i) a fully compositional semantics for timed CSP and (ii) a natural abstraction map into the standard failures/divergences model of untimed CSP. We discuss in detail the construction and properties of this model, and explore the variety of nondeterministic behaviour it encompasses. We argue that, at least in some sense, this model is definitive for timed CSP.

MSC:
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Blamey, S.R., The soundness and completeness of axioms for CSP processes, () · Zbl 0792.68089
[2] Boucher, A.; Gerth, R., A timed failures model for extended communicating sequential processes, () · Zbl 0623.68022
[3] Brookes, S.D.; Hoare, C.A.R.; Roscoe, A.W., A theory of communicating sequential processes, J. ACM, 31, 560-599, (1984) · Zbl 0628.68025
[4] Brookes, S.D.; Roscoe, A.W., An improved failures model for communicating processes, () · Zbl 0565.68023
[5] Davies, J.W., Specification and proof in real-time systems, ()
[6] Davies, J.W.; Jackson, D.M.; Reed, G.M.; Reed, J.N.; Roscoe, A.W.; Schneider, S.A., Timed CSP, theory and practice, ()
[7] Davies, J.W.; Schneider, S.A., Factorising proofs in timed CSP, (), 129-159
[8] Davies, J.W.; Schneider, S.A., A brief history of timed CSP, Theoret. comput. sci., 138, 243-273, (1995) · Zbl 0874.68162
[9] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[10] Jackson, D.M., The specification of aircraft engine control software using timed CSP, ()
[11] Jackson, D.M., Logical verification of reactive software systems, ()
[12] Jones, G., A timed model for communicating processes, () · Zbl 0594.68025
[13] Kay, A.; Reed, J.N., A rely and guarantee method for timed CSP, IEEE trans. software eng., (1993)
[14] Koymans, R.; Shyamasundar, R.K.; de Roever, W.P.; Gerth, R.; Arun-Kumar, S., Compositional semantics for real-time distributed computing, () · Zbl 0565.68026
[15] Lowe, G., Probabilities and priorities in timed CSP, ()
[16] Lowe, G., Probabilistic and prioritized models of timed CSP, Theoret. comput. sci., 138, 315-353, (1995) · Zbl 0874.68163
[17] Mislove, M.W.; Roscoe, A.W.; Schneider, S.A., Fixed points without completeness, Theoret. comput. sci., 138, 273-315, (1995) · Zbl 0874.68186
[18] Reed, G.M., A uniform mathematical theory for real-time distributed computing, ()
[19] Reed, G.M., A hierarchy of models for real-time distributed computing, (), 80-128
[20] Reed, G.M.; Roscoe, A.W.; Reed, G.M.; Roscoe, A.W., A timed model for communicating sequential processes, (), Theoret. comput. sci., 58, 249-261, (1986) · Zbl 0655.68031
[21] Reed, G.M.; Roscoe, A.W., Metric spaces as models for real-time concurrency, (), 331-343 · Zbl 0644.68040
[22] Reed, G.M.; Roscoe, A.W.; Schneider, S.A., CSP and time-wise refinement, ()
[23] Roscoe, A.W., A mathematical theory of communicating processes, () · Zbl 1351.68148
[24] Scattergood, B., An application of timed CSP to robot control software, ()
[25] Schneider, S.A., Correctness and communication in real-time systems, ()
[26] S.A. Schneider, An operational semantics for Timed CSP, Inform. Comput., to appear. · Zbl 0827.68069
[27] Stamper, R., The specification of AGV control software using timed CSP, ()
[28] Superville, S., Specifying complex systems with timed CSP: a decomposition and specification of a telephone exchange system which has a central controller, ()
[29] Wallace, A.R., A TCSP case study of a flexible manufacturing system, ()
[30] Zwarico, A.E., A formal model of real-time computing, University of pennsylvania, technical report, (1986)
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.