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

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: George S. Avrunin, Experiments in Constrained Expression Analysis, University of Massachusetts, Amherst, MA, 1988
• 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: George S. Avrunin , Jack C. Wileden, Describing and analyzing distributed software system designs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.380-403, July 1985 [doi>10.1145/3916.3989]
• 5: G S Avrunin , L K Dillon , J C Wileden , W E Riddle, Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems, IEEE Transactions on Software Engineering, v.12 n.2, p.278-292, Feb. 1986
• 6: BATES, P., AND WILEDEN, J.C. High level debugging of distributed systems. J. Syst. Softw. 3, 4 (Dec. 1983), 255-264.
• 7: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 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: W Bruce Croft , Lawrence S. Lefkowitz, Task support in an office system, ACM Transactions on Information Systems (TOIS), v.2 n.3, p.197-212, July 1984 [doi>10.1145/1206.1483]
• 10: Laura K. Dillon, Analysis of distributed systems using constrained expressions (concurrent systems), 1984
• 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: Seymour Ginsburg, The Mathematical Theory of Context-Free Languages, McGraw-Hill, Inc., New York, NY, 1966
• 14: Irene Greif, A language for formal problem specification, Communications of the ACM, v.20 n.12, p.931-935, Dec. 1977 [doi>10.1145/359897.359904]
• 15: 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]
• 16: M. Hack, PETRI NET LANGUAGE, Massachusetts Institute of Technology, Cambridge, MA, 1976
• 17: 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]
• 18: HOARE, C. A.R. Specifications, programs and implementations. Tech. Mono. PRG-29, Oxford Univ. Computing Laboratory, Oxford, England, June 1982.
• 19: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 20: HOLZMANN, G.J. A theory of protocol validation. IEEE Trans. Comput. (Aug. 1982), 730-738.
• 21: 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]
• 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: Van Nguyen , Alan Demers , David Gries , Susan Owicki, A model and temporal proof system for networks of processes, Distributed Computing, v.1 n.1, p.7-25, Jan. 1986 [doi>10.1007/BF01843567]
• 25: PETERSON, J. Computation sequence sets. J. Comput. Syst. Sci. 13, i (Aug. 1976), 1-24.
• 26: James L. Peterson, Petri Nets, ACM Computing Surveys (CSUR), v.9 n.3, p.223-252, Sept. 1977 [doi>10.1145/356698.356702]
• 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: 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]
• 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.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Design languages
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Concurrency
      D.4.7 Organization and Design
          Subjects: Distributed systems

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Algebraic language theory

General Terms:
Design, Languages, Theory, Verification