More Web Proxy on the site http://driver.im/

article

Open access

Constrained expressions: toward broad applicability of analysis methods for distributed software systems

Editor: Susan L. Graham Authors:

Laura K. Dillon,

George S. Avrunin,

Jack C. WiledenAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 10, Issue 3

Pages 374 - 402

https://doi.org/10.1145/44501.44502

Published: 01 July 1988 Publication History

Abstract

It is extremely difficult to characterize the possible behaviors of a distributed software system through informal reasoning. Developers of distributed systems require tools that support formal reasoning about properties of the behaviors of their systems. These tools should be applicable to designs and other preimplementation descriptions of a system, as well as to completed programs. Furthermore, they should not limit a developer's choice of development languages.

In this paper we present a basis for broadly applicable analysis methods for distributed software systems. The constrained expression formalism can be used with a wide variety of distributed system development notations to give a uniform closed-form representation of a system's behavior. A collection of formal analysis techniques can then be applied with this representation to establish properties of the system. Examples of these formal analysis techniques appear elsewhere. Here we illustrate the broad applicability of the constrained expression formalism by showing how constrained expression representations are obtained from descriptions of systems in three different notations: SDYMOL, CSP, and Petri nets. Features of these three notations span most of the significant alternatives for describing distributed software systems. Our examples thus offer persuasive evidence for the broad applicability of the constrained expression approach.

References

[1]

AVERY, S.M. Development of a behavior generator for constrained expressions. Tech. Rep. SDLM/84-2, Software Development Laboratory, Dept. of Computer and Information Science, Univ. of Massachusetts, Amherst, June 1984.

[2]

AVRUNIN, G.S. Experiments in constrained expression analysis. Tech. Rep. 87-125, Dept. of Computer and Information Science, Univ. of Massachusetts, Amherst, 1987.

[3]

AVRUNIN, G. S., AND WILEDEN, J. C. Algebraic techniques for the analysis of concurrent systems. In Proceedings of the Sixteenth Annual Hawaii International Conference on System Science (Jan. 1983). Western Periodicals, 1983, pp. 51-57.

[4]

AVRUNIN, G. S., AND WILEDEN, J. C. Describing and analyzing distributed system designs. ACM Trans. Program. Lang. Syst. 7, 3 (July 1985), 380-403.

[5]

AVRUNIN, G. S., DILLON, L. K., WILEDEN, J. C., AND RIDDLE, W.E. Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems. IEEE Trans. So{tw. Eng. SE-12, 12 (Feb. 1986), 278-292.

[6]

BATES, P., AND WILEDEN, J.C. High level debugging of distributed systems. J. Syst. Softw. 3, 4 (Dec. 1983), 255-264.

[7]

CAMPBELL, R. $., AND HABERMANN, A.N. The specification of process synchronization by path expressions. In Lecture Notes in Computer Science, Springer-Verlag, Heidelberg, 1974, pp. 89-102.

[8]

CHEN, B. S., AND YEH, R.T. Formal specification and verification of distributed systems. IEEE Trans. Softw. Eng. 6 (Nov. 1983), 710-722.

[9]

CROFT, W., AND LEFKOWITZ, L. Task support in an office system. ACM Trans. Office Inf. Syst. 2, 3 (July 1984), 197-212.

[10]

DILLON, L.K. Analysis of distributed systems using constrained expressions. Ph.D. dissertation, Univ. of Massachusetts, Amherst, Sept. 1984. Also available as TR 84-18.

[11]

DILLON, L.K. Overview of the constrained expression design language. Tech. Rep. TRCS86- 21, Computer Science Dept., Univ. of California, Santa Barbara, Oct. 1986.

[12]

DILLON, L. K. Simplification and reduction of CEDL constrained expressions. Tech. Rep. TRCS86-29, Computer Science Dept., Univ. of California, Santa Barbara, Nov. 1986.

[13]

GINSBURG, S. The Mathematical Theory of Context-Free Languages. McGraw Hill, New York, 1966.

[14]

GREIF, I. A language for formal problem specification. Commun. ACM 20, 12 (Dec. 1977), 931-935.

[15]

HABERMANN, A.N. Synchronization of communicating processes. Commun. ACM 25, 3 (Mar. 1972), 171-176.

[16]

HACK, M. Petri net languages. Memo 124, Computation Structures Group, MIT, Cambridge, Mass., June 1975.

[17]

HOARE, C. A. R. Communicating sequential processes. Commun. ACM 21, 8 (Aug. 1978), 666-677.

[18]

HOARE, C. A.R. Specifications, programs and implementations. Tech. Mono. PRG-29, Oxford Univ. Computing Laboratory, Oxford, England, June 1982.

[19]

HOARE, C. A.R. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, N.J. 1985.

[20]

HOLZMANN, G.J. A theory of protocol validation. IEEE Trans. Comput. (Aug. 1982), 730-738.

[21]

LAMPORT, L. A new approach to proving the correctness of multiprocess programs. ACM Trans. Program. Lang. Syst. (July 1979), 84-97.

[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]

MISRA, J., AND CHANDY, K. M. Proofs of networks of processes. IEEE Trans. So{tw. Eng. SE-7, 4 (July 1981), 417-426.

[24]

NGUYEN, V., DEMERS, A., GRIES, D., AND OWICKI, S. A model and temporal proof system for networks of processes. Distributed Comput. (Jan. 1986), 7-25.

[25]

PETERSON, J. Computation sequence sets. J. Comput. Syst. Sci. 13, i (Aug. 1976), 1-24.

[26]

PETERSON, J. Petri nets. ACM Comput. Surv. 9, 3 (Sept. 1977), 223-252.

[27]

RIDDLE, W.E. An approach to software system behavior modeling. Cornput. Lang. (Elmsford, N.Y.) 4 (1979), 29-47.

[28]

SHAW, A.C. Software descriptions with flow expressions. IEEE Trans. Softw. Eng. SE-4, 3 (May 1978), 242-254.

[29]

SUNDARAM, U. A constrained expression deriver for CEDL: An overview. Tech. Rep. SDLM 86-1, Software Development Laboratory, Dept. of Computer and Information Science, Univ. of Massachusetts, Amherst, Aug. 1986.

[30]

SUNDARAM, U., AVRUNIN, G. S., AND WILEDEN, J.C. Design of the deriver for CEDL. To be published.

[31]

TAYLOR, R.N. A general-purpose algorithm for analyzing concurrent programs. Commun. ACM 6, 5 (May 1983), 362-376.

[32]

WELTER, M. Counter expressions. Tech. Rep. RSSM/24, Dept. of Computer and Communication Science, Univ. of Michigan, Ann Arbor, Oct. 1976.

[33]

WILEDEN, J.C. Techniques for modelling parallel systems with dynamic structure. J. Digital Syst. (Summner 1980), 177-197.

[34]

WILEDEN, J.C. Constrained expressions and the analysis of designs for dynamically-structured distributed systems. In Proceedings o{ the 1982 International Conference on Parallel Processing (Bellaire, Mich., Aug. 1982). IEEE Computer Society Press, New York, pp. 340-344.

Cited By

Brzozowski JDavies SMadan A(2018)State complexity of pattern matching in regular languagesTheoretical Computer Science10.1016/j.tcs.2018.12.014Online publication date: Dec-2018
https://doi.org/10.1016/j.tcs.2018.12.014
Ghezzi CKemmerer R(2005)ASTRAL: An assertion language for specifying realtime systemsESEC '9110.1007/3540547428_46(122-146)Online publication date: 2-Jul-2005
https://doi.org/10.1007/3540547428_46
Ghezzi CFelder MBellettini C(2005)Real-time systems: A survey of approaches to formal specification and verificationSoftware Engineering — ESEC '9310.1007/3-540-57209-0_3(11-36)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-57209-0_3
Show More Cited By

Index Terms

Constrained expressions: toward broad applicability of analysis methods for distributed software systems
1. Software and its engineering
  1. Software notations and tools
    1. System description languages
      1. Design languages
  2. Software organization and properties
    1. Contextual software domains
      1. Operating systems
        Process management
        Concurrency control
    2. Software system structures
      1. Distributed systems organizing principles
2. Theory of computation

Recommendations

Constrained Expression: Toward Broad Applicability of Analysis Methods
Formal semantics for tabular expressions and software cost reduction method
Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems

We describe an approach to the design of concurrent software systems based on the constrained expression formalism. This formalism provides a rigorous conceptual model for the semantics of concurrent computations, thereby supporting analysis of ...

Reviews

Reviewer: Ali Mili

Constrained expressions are a notational device for representing the interactions among the asynchronous components of a distributed system. They operate by explicitly characterizing the illegal sequences of events among the set of all possible sequences; the authors find this exclusion-based approach to be “both simpler and more natural” than generating the set of legal sequences directly. In order to demonstrate the generality of the proposed notation, the authors show how it captures descriptions in three languages which are currently used to describe concurrency, namely SDYMOL, CSP, and Petri nets. The paper is readable with reasonable effort, although some of its motivation is obscured by weak reasoning (for example, the contrast between “formal analysis methods” and “appropriate development notations” is unclear).

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 10, Issue 3

July 1988

158 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/44501

Editor:
Susan L. Graham

Issue’s Table of Contents

Copyright © 1988 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1988

Published in TOPLAS Volume 10, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
372
Total Downloads

Downloads (Last 12 months)45
Downloads (Last 6 weeks)8

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Brzozowski JDavies SMadan A(2018)State complexity of pattern matching in regular languagesTheoretical Computer Science10.1016/j.tcs.2018.12.014Online publication date: Dec-2018
https://doi.org/10.1016/j.tcs.2018.12.014
Ghezzi CKemmerer R(2005)ASTRAL: An assertion language for specifying realtime systemsESEC '9110.1007/3540547428_46(122-146)Online publication date: 2-Jul-2005
https://doi.org/10.1007/3540547428_46
Ghezzi CFelder MBellettini C(2005)Real-time systems: A survey of approaches to formal specification and verificationSoftware Engineering — ESEC '9310.1007/3-540-57209-0_3(11-36)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-57209-0_3
Avrunin GBuy UCorbett J(2005)Integer programming in the analysis of concurrent systemsComputer Aided Verification10.1007/3-540-55179-4_10(92-102)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-55179-4_10
Cook JWolf A(1999)Software process validationACM Transactions on Software Engineering and Methodology10.1145/304399.3044018:2(147-176)Online publication date: 1-Apr-1999
https://dl.acm.org/doi/10.1145/304399.304401
Coen-Porisini AGhezzi CKemmerer R(1997)Specification of realtime systems using ASTRALIEEE Transactions on Software Engineering10.5555/254499.27100823:9(572-598)Online publication date: 1-Sep-1997
https://dl.acm.org/doi/10.5555/254499.271008
Pezzè MYoung MAdrion W(1997)Constructing multi-formalism state-space analysis toolsProceedings of the 19th international conference on Software engineering10.1145/253228.253278(239-250)Online publication date: 1-May-1997
https://dl.acm.org/doi/10.1145/253228.253278
Coen-Porisini AGhezzi CKemmerer R(1997)Specification of realtime systems using ASTRALIEEE Transactions on Software Engineering10.1109/32.62949423:9(572-598)Online publication date: Jan-1997
https://doi.org/10.1109/32.629494
Pezzè MYoung M(1996)Generation of multi-formalism state-space analysis toolsProceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis10.1145/229000.226314(172-179)Online publication date: 1-May-1996
https://dl.acm.org/doi/10.1145/229000.226314
Pezzè MYoung M(1996)Generation of multi-formalism state-space analysis toolsACM SIGSOFT Software Engineering Notes10.1145/226295.22631421:3(172-179)Online publication date: 1-May-1996
https://dl.acm.org/doi/10.1145/226295.226314
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents