This Article 
 Bibliographic References 
 Add to: 
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
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.