Nothing Special   »   [go: up one dir, main page]

skip to main content
article
Open access

Describing and analyzing distributed software system designs

Published: 01 July 1985 Publication History

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]
APT, K., FRANCEZ, N., AND DEROEVER, W. A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2, 3 (July 1980), 359-385.
[2]
BATES, P., AND W1LEDEN, J. High-level debugging of distributed systems. J. Syst. Softw. (Dec. 1983), 255-264.
[3]
BRINCH HANSEN, P. Distributed processes: A concurrent programming concept. Commun. ACM (Nov. 1978), 934-941.
[4]
CAMPBELL, R., AND KOLSTAD, R. Path expressions in Pascal. In Proceedings of the 4th International Conference on Software Engineering (Munich, Sept. 1979).
[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]
DILLON, L. Analysis of distributed systems using constrained expressions, Ph.D. dissertation, Computer and Information Science Dept., Univ. of Massachusetts, Aug. 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]
FELDMAN, J. High-level programming for distributed computing. Commun. ACM (June 1979), 353-368.
[10]
FLOYD, R.W. Assigning meaning to programs. In Proceedings of Symposia in Applied Mathematics, Mathematical Aspects of Computer Science (1967), 19-32.
[11]
HABERMANN, A.N. Synchronization of communicating processes. Commun. ACM (Mar. 1972), 171-176.
[12]
HOARE, C.A.R. An axiomatic basis of computer programming. Commun. ACM (Oct. 1969), 576- 580, 583.
[13]
HOARE, C.A.R. Communicating sequential processes. Cornmun. ACM (Aug. 1978), 666-677.
[14]
HOARE, C.A.R. Some properties of predicate transformers. J. ACM (July 1978), 461-480.
[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]
LAMPORT, L. A new solution of Dijkstra's concurrent programming problem. Commun. ACM (Aug. 1974), 453-455.
[18]
LAMPORT, L. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. (Mar. 1977), 125-143.
[19]
LAMrORT, L. Time, clocks and the ordering of events in a distributed system. Comrnun. ACM (July 1978), 558-565.
[20]
LAMPORT, L. A new approach to proving the correctness of multiprocess programs. ACM Trans. Program. Lang. Syst. 1, 3 (July 1979), 84-97.
[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]
LISKOV, B. Primitives for distributed computing. In Proceedings of the 7th Symposium on Operating Systems Principles (Dec. 1979), 33-42.
[24]
MISRA, J., AND CHANDY, K.M. Proofs of networks of processes. IEEE Trans. Soft. Eng. (July 1981), 417-426.
[25]
OWICKI, S., AND GRIES, D. Verifing properties of parallel programs: An axiomatic approach. Commun. ACM (May 1976), 279-285.
[26]
PNUELI, A. The temporal semantics of concurrent programs. In Semantics of Concurrent Computation, Kahn, Eds., Springer-Verlag, New York, 1979, 1-20.
[27]
RAMAMRITHAM, $., AND KELLER, R.M. Specifying and proving properties of sentinel processes. In Proceedings of the 5th International Conference on Software Engineering (1981), 374-382.
[28]
RICART, C., AND AGRAWALA, A.K. An optimal algorithm for mutual exclusion in computer networks. Cornrnun. ACM (Jan. 1981), 9-17.
[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]
TAYLOR, R.N. A general purpose algorithm for analyzing concurrent programs. Cornrnun. ACM (May 1983), 362-376.
[33]
WlLEDEN, J. Modeling parallel systems with dynamic structure. COINS Tech. Rep. 78-4, Univ. of Massachusetts, Jan. 1978.
[34]
WILEDEN, J. DREAM--an approach to the design of large-scale concurrent software systems. In Proceedings of the 1979 National Conference of the ACM (Oct. 1979), ACM, New York, 88-94.
[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.

Cited By

View all
  • (2002)Behavior relativity of Petri netsJournal of Computer Science and Technology10.1007/BF0296076717:6(770-780)Online publication date: 1-Nov-2002
  • (1996)An Application of Petri Net Reduction for Ada Tasking Deadlock AnalysisIEEE Transactions on Parallel and Distributed Systems10.1109/71.5533017:12(1307-1322)Online publication date: 1-Dec-1996
  • (1995)Automatic detection of errors in distributed systemsProceedings of the 1995 ACM 23rd annual conference on Computer science10.1145/259526.259534(30-35)Online publication date: 27-Feb-1995
  • Show More Cited By

Index Terms

  1. Describing and analyzing distributed software system designs

                        Recommendations

                        Reviews

                        Helmar Burkhart

                        Distributed computer systems, whether loosely or tightly coupled, are characterized by parallelism. For such systems, software must carefully be designed and verified. Therefore, the authors' problem is relevant: Which techniques might aid in the preimplementation stage of distributed software development__?__ The paper provides both a technique and a case study. In the first part, a descriptive formalism and a notation are introduced. The notation describes systems as collections of sequential processes communicating entirely via message transmission. In order to investigate the usefulness, this approach is then applied to the problem of how to achieve mutual exclusion in a computer network. The Agrawala-Ricart algorithm [1,2] has been chosen for this case study, and a specification using the proposed notation DYMOL is given. Finally, this specification is analyzed by a technique which models the possible behaviors of the system as a set of symbol strings. To have maximum benefit when reading this paper, a thorough understanding of the Agrawala-Ricart algorithm seems mandatory. Unlike the authors of this paper, I recommend that potential readers first refer to [1] and [2]; the comparison between the original notation (ALGOL style) and this paper's design notation is very informative. I have found the original notation more natural than the somewhat artificial constructs of the DYMOL specification. Although the proposed specification hides implementation aspects, it is not shorter. In conclusion, I find the paper interesting for researchers working in the fields of software specification and verification techniques.

                        Access critical reviews of Computing literature here

                        Become a reviewer for Computing Reviews.

                        Comments

                        Please enable JavaScript to view thecomments powered by Disqus.

                        Information & Contributors

                        Information

                        Published In

                        cover image ACM Transactions on Programming Languages and Systems
                        ACM Transactions on Programming Languages and Systems  Volume 7, Issue 3
                        July 1985
                        134 pages
                        ISSN:0164-0925
                        EISSN:1558-4593
                        DOI:10.1145/3916
                        Issue’s Table of Contents
                        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                        Publisher

                        Association for Computing Machinery

                        New York, NY, United States

                        Publication History

                        Published: 01 July 1985
                        Published in TOPLAS Volume 7, Issue 3

                        Permissions

                        Request permissions for this article.

                        Check for updates

                        Qualifiers

                        • Article

                        Contributors

                        Other Metrics

                        Bibliometrics & Citations

                        Bibliometrics

                        Article Metrics

                        • Downloads (Last 12 months)61
                        • Downloads (Last 6 weeks)8
                        Reflects downloads up to 18 Nov 2024

                        Other Metrics

                        Citations

                        Cited By

                        View all
                        • (2002)Behavior relativity of Petri netsJournal of Computer Science and Technology10.1007/BF0296076717:6(770-780)Online publication date: 1-Nov-2002
                        • (1996)An Application of Petri Net Reduction for Ada Tasking Deadlock AnalysisIEEE Transactions on Parallel and Distributed Systems10.1109/71.5533017:12(1307-1322)Online publication date: 1-Dec-1996
                        • (1995)Automatic detection of errors in distributed systemsProceedings of the 1995 ACM 23rd annual conference on Computer science10.1145/259526.259534(30-35)Online publication date: 27-Feb-1995
                        • (1993)Real-time software methodologies: Are they suitable for developing Manufacturing control software?International Journal of Flexible Manufacturing Systems10.1007/BF013589495:2(95-128)Online publication date: Jun-1993
                        • (1991)Automated Analysis of Concurrent Systems with the Constrained Expression ToolsetIEEE Transactions on Software Engineering10.1109/32.10697517:11(1204-1222)Online publication date: 1-Nov-1991
                        • (1990)Applying Petri net reduction to support Ada-tasking deadlock detectionProceedings.,10th International Conference on Distributed Computing Systems10.1109/ICDCS.1990.89289(96-103)Online publication date: 1990
                        • (1990)Design and Implementation of a Petri Net Based Toolkit for Ada Tasking AnalysisIEEE Transactions on Parallel and Distributed Systems10.1109/71.801721:4(424-441)Online publication date: 1-Oct-1990
                        • (1990)Key references in distributed computer systems 1959–1989Distributed Computer Systems10.1016/B978-0-408-02938-4.50016-4(193-295)Online publication date: 1990
                        • (1989)Experiments in automated analysis of concurrent software systemsACM SIGSOFT Software Engineering Notes10.1145/75309.7532314:8(124-130)Online publication date: 1-Nov-1989
                        • (1989)Experiments in automated analysis of concurrent software systemsProceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification10.1145/75308.75323(124-130)Online publication date: 1-Nov-1989
                        • Show More Cited By

                        View Options

                        View options

                        PDF

                        View or Download as a PDF file.

                        PDF

                        eReader

                        View online with eReader.

                        eReader

                        Login options

                        Full Access

                        Media

                        Figures

                        Other

                        Tables

                        Share

                        Share

                        Share this Publication link

                        Share on social media