This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Software Environment for the Specification and Analysis of Problems of Coordination and Concurrency
March 1988 (vol. 14 no. 3)
pp. 280-290

The SPANNER software environment for the specification and analysis of concurrent process coordination and resource sharing coordination is described. In the SPANNER environment, one can formally produce a specification of a distributed computing problem, and then verify its validity through reachability analysis and simulation. SPANNER is based on a finite-state machine model called the selection/resolution model. The capabilities of SPANNER are illustrated by the analysis of two classical coordination problems: (1) the dining philosophers; and (2) Dijkstra's concurrent programming problem. In addition, some of the more recently implemented capabilities of the SPANNER system are discussed, such as process types and cluster variables.

[1] S. Aggarwal, D. Barbara, and K. Z. Meth, "SPANNER: A tool for the specification, analysis, and evaluation of protocols,"IEEE Trans. Software Eng., vol. SE-13, pp. 1218-1237, Aug. 1987.
[2] S. Aggarwal, D. Barbará, and K. Z. Meth, "Specifying and analyzing protocols with SPANNER," inProc. Int. Conf. Communications '86, Toronto, Ont., Canada, June 1986.
[3] S. Aggarwal, D. Barbará, and K. Z. Meth, "SPANNER update: New features and capabilities," AT&T, Tech. Memo., 1986.
[4] S. Aggarwal, C. Courcoubetis, and P. W. Wolper, "Introducing liveness properties in finite-state protocol verification," 1986, to be published.
[5] S. Aggarwal and Z. Har'El, "SIMUL-A tool for the simulation and analysis of protocols,"Comput. Networks, to be published.
[6] S. Aggarwal, R. P. Kurshan, and K. K. Sabnani, "A calculus for protocol specification and validation," inProtocol Specification, Testing and Verification, III, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: North-Holland, 1983.
[7] T. P. Blumer and R. L. Tenney, "A formal specification technique and implementation method for protocols,"Comput. Networks, vol. 6, no. 3, July 1982.
[8] G. V. Bochmann, "Finite state descriptions of communication protocols,"Comput. Networks, vol. 2, Oct. 1978.
[9] E. A. Emerson and E. Clarke, "Design and synthesis of synchronization skeletons using branching-time temporal logic," inProc. Workshop Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.
[10] E. W. Dijkstra, "Solution of a problem in concurrent programming control,"Commun. ACM, vol. 8, pp. 569-569, Sept. 1965.
[11] V. Gehlot and I. Lee, "Formal specification and verification of the X.25 based protocol," Univ. Pennsylvania, Tech. Rep. 1987.
[12] B. Hailpern and S. Owicki, "Modular verification of computer communication protocols,"IEEE Trans. Comm., vol. COM-31, Jan. 1983.
[13] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[14] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[15] R. P. Kurshan, "Modelling concurrent processes," inProc. Amer. Math. Soc. Symp. Applied Math., vol. 31, 1985.
[16] R. P. Kurshan and B. Gopinath, "The selection/resolution model for concurrent processes," unpublished work.
[17] L. Lamport, "A new solution of Dijkstra's concurrent programming problem,"Commun. ACM, vol. 17, no. 8, pp. 453-455, 1974.
[18] R. J. Linn, "The features and facilities of Estelle: A formal description technique based upon an extended finite state machine model," inProtocol, Specification, Testing, and Verification V, M. Diaz, Ed. Amsterdam, The Netherlands: North-Holland, 1986, pp. 271-296.
[19] Z. Manna and A. Pneuli, "Verification of concurrent programs: The temporal framework," inThe Correctness Problem in Computer Science, Boyer and Moore, Eds. New York: Academic 1981.
[20] Z. Manna and P. Wolper, "Synthesis of communicating processes from temporal logic specifications,"ACM Trans. Programm. Languag. Syst., vol. 6, no. 1, pp. 68-93, Jan. 1984.
[21] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[22] H. Rudin and C. H. West, Eds.,Protocol Specification, Testing, and Verification, III. Amsterdam, The Netherlands: North-Holland, 1983.
[23] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223-252, Sept. 1977.
[24] C. A. Sunshine, Ed.,Communicating Protocol Modeling. Dedham, MA: Artech House, 1981.
[25] F. J. W. Symons, "Introduction to numerical petri nets, a general graphical model of concurrent processing systems,"Australian Telecommun. Res., vol. 14, no. 1, 1980.
[26] P. Zafiropulo, "Protocol validation by duologue-matrix analysis,"IEEE Trans. Commun., vol. COM-26, no. 8, pp. 1187-1193, Aug. 1978.
[27] P. Zafiropulo, "Information processing systems-Open systems interconnection-- LOTOS," Draft Proposal, 1985.

Index Terms:
software environment; specification; coordination; concurrency; SPANNER software environment; distributed computing; reachability analysis; simulation; finite-state machine model; selection/resolution model; dining philosophers; concurrent programming; cluster variables; distributed processing; parallel programming; programming environments
Citation:
S. Aggarwal, D. Barbar?, K.Z. Meth, "A Software Environment for the Specification and Analysis of Problems of Coordination and Concurrency," IEEE Transactions on Software Engineering, vol. 14, no. 3, pp. 280-290, March 1988, doi:10.1109/32.4649
Usage of this product signifies your acceptance of the Terms of Use.