This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Rely and Guarantee Method for Timed CSP: A Specification and Design of a Telephone Exchange
June 1993 (vol. 19 no. 6)
pp. 625-639

A rely and guarantee method for timed communicating sequential processes (TCPSs), by which the behavior of a component belonging to a composite system is specified in terms of what it guarantees to its neighbors and what it relies on from them, is described. The method is illustrated using an overview of the specification of a plain old telephone service together with part of a design that provably satisfies this specification. The specification and design deal with safety, liveness, and troublesome race conditions.

[1] B. Biebow and J. Hagelstein, Algebraic Specification of Synchronization and Errors: A Telephonic Example,Lecture Notes in Computer Science, vol. 186, 1985, 294-308.
[2] G. Bochmann, "A general transition model for protocols and communication services,"IEEE Trans. Commun., vol. 28, pp. 643-650, 1980.
[3] S. D. Brookes and A. W. Roscoe, "An improved failures model for communicating sequential processes," inProc. Pittsburgh Seminar on Concurrency, Springer LNCS 197, 1985.
[4] M. Daniels, "Modelling real-time behaviour with an interval time calculus," inProc. Formal Techniques in Real-time and Fault-tolerant Syst., Springer LNCS 571, 1992.
[5] J. W. Davies, "Specification and proof in real-time systems," D. Phil. thesis, Oxford Univ., 1991.
[6] J. W. Davies, D. M. Jackson, and S. A. Schneider, "Making things happen in timed CSP," Oxford Univ. Programming Research Group Tech. Rep. PRG-TR-2-90, 1990.
[7] J.W. Davies and S. A. Schneider, "An extended syntax for timed CSP," Oxford Univ. Programming Research Group Tech. Rep. PRG-TR-4-90, 1990.
[8] M. Faci, L. Logrippo, and B. Stepien, Formal "Specification of telephone system in LOTOS: The constraint-oriented style approach," Tech. Rep., Univ. of Ottowa, Canada, 1990; Computer Networks and ISDN Systems.
[9] A. Finkelstein, M. Goedicke, and J. Kramer, "Viewpoint oriented software development," inProc. Third Int. Workshop Software Engineering and Its Appl., Toulouse, Dec. 1990.
[10] P. Graubmann, "Behavioural specification of concurrent systems," Rex Internal Document REX-WP1-SIE-001-V1.0, 1989.
[11] M. Hennessy and R. Milner, "Algebraic laws for nondeterminism and concurrency,"J. ACM, vol. 32, no. 1, pp. 137-161, Jan. 1985.
[12] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[13] "Call processing specification parts 1-4," Rex Internal Documents REX- WP8-1NT-003-VI.0. 007-VI.0, Intracom, 1990.
[14] "SDL description of the telecommunications demonstrator," REX Internal Document REX-WP8-INT-007-VI.0, Intrasoft, Apr. 1990.
[15] M. Jackson, System Development. Englewood Cliffs, NJ: Prentice-Hall Int., 1983.
[16] D. M. Jackson, "The specification of aircraft engine control software in timed CSP," M.Sc. thesis, Oxford Univ. 1989.
[17] K. Jensen, "Colored Petri nets," inAdvances in Petri Nets(LNCS 254). New York: Springer-Verlag, 1987, pp. 248-299.
[18] C. Jones, "Development methods for computer programs including a notion of interference," D. Phil. thesis, Oxford Univ., June 1981; PRG Tech. Mono. 25.
[19] C. Jones, "Tentative steps towards a development method for interfering programs,"ACM Trans. Prog. Lang., vol. 5,4 pp. 596-619, Oct. 1983.
[20] C. Jones, "Interference resumed," Tech. Rep. UMCS-91-5-1, Manchester Univ., 1991; Australian Software Engineering Research 1991, P. Bailes, Ed., Springer-Verlag.
[21] A. Kay, "A theory of rely and guarantee in timed CSP," in preparation.
[22] A. Kay and J. N. Reed, "A specification of a telephone exchange in timed CSP," Oxford Univ. Programming Research Group Tech. Rep. PRG-TR-19-90, 1990.
[23] A. Kay and J. N. Reed, "Using rely and guarantee in TCSP," Oxford Univ. Programming Research Group Tech. Rep. PRG-TR-11-91, 1991.
[24] J. Kramer, J. Magee, M. Sloman, N. Duranker, S. Crane, K. Twidle, "An introduction to distributed programming in Rex," submitted toEsprit '91 Conf.
[25] S. S. Lam and A. U. Shankar, "Understanding interfaces," inProc. Fourth Int. Conf. Formal Description Techniques, Sydney, Australia, 1991.
[26] L. Chen, "An interleaving model for real-time systems," LFCS report series, ECS-LFCS-91-184, Univ. of Edinburgh, 1991.
[27] F. Moller and C. Tofts, "A temporal calculus of communicating systems," inProc. CONCUR 90, Springer LNCS 458, 1990.
[28] X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron, "ATP: An algebra for timed processes," inProc. IFIP Working Conf. Programming Concepts and Methods, 1990.
[29] G. M. Reed, "A uniform theory for real-time distributed computing," Ph.D. dissertation, St. Edmund Hall, Oxford University, 1988.
[30] G. Reed and A. Roscoe, "A timed model for communicating sequential processes, " inProc. ICALP '86, Springer-Verlag LCNS 226, 1986, pp. 314-323.
[31] G. M. Reed and A. W. Roscoe, "Metric spaces as models for real-time concurrency," inProc. Math. Found. of Computer Science, LNCS 298, 1987.
[32] A. Rockstrom and R. Saracco, "SDL-CCITT specification and description language,"IEEE Trans. Commun., vol. COM-30, no. 6, pp. 1310-1318, June 1982.
[33] K. Stølen, "Development of totally correct shared-state parallel programs," Ph.D. dissertation, Manchester Univ., 1990; Tech. Rep. UMCS- 91-1-1.
[34] I. Tvrdy, "Formal modelling of telematics services using LOTOS,"Microprocessing and Microprogramming, vol. 25, nos. 1-5, pp. 313-317, 1989.
[35] J. C. P. Woodcock and B. Dickinson, "Using VDM with rely and guarantee conditions: experiences from a real project," inProc. VDM '88-VDM--The Way Ahead(Lecture Notes in Computer Sci., vol. 328), R. Bloomfield, L. Marshall, and R. Jones, Eds. Berlin: Springer-Verlag, 1988, pp. 434-458.
[36] P. Zave, "The operational versus the conventional approach to software development,"Commun. ACM, vol. 27, no. 2, pp. 104-118, Feb. 1984.
[37] P. Zave, "A distributed alternative to finite-state-machine specifications,"ACM Trans. Programming Languages and Syst., vol. 7, no. 1, pp. 10-36, Jan. 1985.

Index Terms:
rely method; telephone exchange; guarantee method; timed communicating sequential processes; specification; telephone service; safety; liveness; troublesome race conditions; communicating sequential processes; formal specification; telecommunications computing; telephone exchanges
Citation:
A. Kay, J.N. Reed, "A Rely and Guarantee Method for Timed CSP: A Specification and Design of a Telephone Exchange," IEEE Transactions on Software Engineering, vol. 19, no. 6, pp. 625-639, June 1993, doi:10.1109/32.232027
Usage of this product signifies your acceptance of the Terms of Use.