Describing and analyzing distributed software system designs

ABSTRACT

In this paper we outline an approach to describing and analyzing designs for distributed software systems. A descriptive notation is introduced, and analysis techniques applicable to designs expressed in that notation are presented. The usefulness of the approach is illustrated by applying it to a realistic distributed software-system design problem involving mutual exclusion in a computer network.

REFERENCES

• 1: Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
• 2: BATES, P., AND W1LEDEN, J. High-level debugging of distributed systems. J. Syst. Softw. (Dec. 1983), 255-264.
• 3: Per Brinch Hansen, Distributed processes: a concurrent programming concept, Communications of the ACM, v.21 n.11, p.934-941, Nov. 1978 [doi>10.1145/359642.359651]
• 4: Roy H. Campbell , Robert B. Kolstad, Path expressions in pascal, Proceedings of the 4th international conference on Software engineering, p.212-219, September 17-19, 1979, Munich, Germany
• 5: CLARKE, r., GRAHAM, R., AND WILEDEN, J. Thoughts on the design phase of an integrated software development environment. In Proceedings of the 14th Hawaii International Conference on Systems Science (Honolulu, Jan. 1981).
• 6: Laura K. Dillon, Analysis of distributed systems using constrained expressions (concurrent systems), 1984
• 7: DILLON, r., AVRUNIN, C., AND WII~EDEN, J. Analyzing distributed systems using constrained expressions. SDLM 83-3, Univ. of Massachusetts, Feb. 1983.
• 8: DoD. United States Department of Defense. Reference Manual for the Ada Programming Language. ANSI/MIL-STD-1815A, Jan. 1983.
• 9: Jerome A. Feldman, High level programming for distributed computing, Communications of the ACM, v.22 n.6, p.353-368, June 1979 [doi>10.1145/359114.359127]
• 10: FLOYD, R.W. Assigning meaning to programs. In Proceedings of Symposia in Applied Mathematics, Mathematical Aspects of Computer Science (1967), 19-32.
• 11: A. Nico Habermann, Synchronization of communicating processes, Communications of the ACM, v.15 n.3, p.171-176, March 1972 [doi>10.1145/361268.361277]
• 12: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 13: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 14: C. A. R. Hoare, Some Properties of Predicate Transformers, Journal of the ACM (JACM), v.25 n.3, p.461-480, July 1978 [doi>10.1145/322077.322088]
• 15: HOARE, C.A.R. A model for communicating sequential processes. In On the Construction of Programs, McKeag and McNaghton, Eds., Cambridge University Press, 1980, 229-243.
• 16: HOLZMANN, G.L. A theory for protocol validation. IEEE Trans. Comput. (Aug. 1982), 730-738.
• 17: Leslie Lamport, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, v.17 n.8, p.453-455, Aug. 1974 [doi>10.1145/361082.361093]
• 18: LAMPORT, L. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. (Mar. 1977), 125-143.
• 19: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 20: Leslie Lamport, A New Approach to Proving the Correctness of Multiprocess Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.84-97, July 1979 [doi>10.1145/357062.357068]
• 21: LAUER, P.E., AND CAMPBELL, R.H. Formal semantics for a class of high-level primitives for coordinating concurrent processes. Acta Inf. (1975), 247-332.
• 22: LAUER, P.E., TORRIGIANI, P.R., AND SHIELDS, M.W. COSY: A system specification language based on paths and processes. Acta Inf. (1979), 451-503.
• 23: Barbara Liskov, Primitives for distributed computing, Proceedings of the seventh ACM symposium on Operating systems principles, p.33-42, December 10-12, 1979, Pacific Grove, California, United States [doi>10.1145/800215.806567]
• 24: MISRA, J., AND CHANDY, K.M. Proofs of networks of processes. IEEE Trans. Soft. Eng. (July 1981), 417-426.
• 25: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 26: Amir Pnueli, The Temporal Semantics of Concurrent Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.1-20, July 02-04, 1979
• 27: Krithivasan Ramamritham , Robert M. Keller, Specifying and proving properties of sentinel processes, Proceedings of the 5th international conference on Software engineering, p.374-382, March 09-12, 1981, San Diego, California, United States
• 28: Glenn Ricart , Ashok K. Agrawala, An optimal algorithm for mutual exclusion in computer networks, Communications of the ACM, v.24 n.1, p.9-17, Jan. 1981 [doi>10.1145/358527.358537]
• 29: RICART, G., AND AGRAWALA, A.K. Corrigendum. Cornrnun. ACM (Sept. 1981), 578.
• 30: RIDDLE, W., WILEDEN, J., SAYLER, J., SEGAL, A., AND STAVELY, A. Behavior modeling during software design. IEEE Trans. Softw. Eng. (July 1978), 283-292.
• 31: RIDDLE, W. An approach to software system modeling and analysis. J. Comput. Lang. (1979), 49-66.
• 32: Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
• 33: WlLEDEN, J. Modeling parallel systems with dynamic structure. COINS Tech. Rep. 78-4, Univ. of Massachusetts, Jan. 1978.
• 34: Jack C. Wileden, DREAM - an approach to designing large scale, concurrent software systems, Proceedings of the 1979 annual conference, p.88-94, January 1979 [doi>10.1145/800177.810036]
• 35: WILEDEN, J. Techniques for modeling parallel systems with dynamic structure. J. Digital Syst. 4, 2 (Summer 1980), 177-197.
• 36: WmEDEN, J. Constrained expressions and the analysis of designs for dynamically structured distributed systems. In Proceedings of the 1982 International Conference on Parallel Processing (Aug. 1982), 340-344.

INDEX TERMS

Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Design languages
          Nouns: DYMOL

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Theory, Verification