Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke. Combining symbolic execution with model checking to verify parallel numerical programs. ACM Trans. Softw. Eng. Method., 17(2):1–34, 2008. (This is a revised and expanded version of a paper that appeared in ISSTA '06.). [ DOI | .pdf ]
We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. This method requires that a sequential version of the program be provided, to serve as the specification for the parallel one. The key idea is to use model checking, together with symbolic execution, to establish the equivalence of the two programs. In this approach the path condition from symbolic execution of the sequential program is used to constrain the search through the parallel program. To handle floating-point operations, three different types of equivalence are supported. Several examples are presented, demonstrating the approach and actual errors that were found. Limitations and directions for future research are also described.
Jamieson M. Cobleigh, George S. Avrunin, and Lori A. Clarke. Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Method., 17(2):1–52, 2008. (This is a revised and expanded version of a paper that appeared in ISSTA '06.). [ DOI | .pdf ]
Finite-state verification techniques are often hampered by the state-explosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning, where a system under analysis is partitioned into subsystems and these subsystems are analyzed individually. By composing the results of these analyses, it can be determined whether or not the system satisfies a property. Because each subsystem is smaller than the whole system, analyzing each subsystem individually may reduce the overall cost of verification. Often the behavior of a subsystem is dependent on the subsystems with which it interacts, and thus it is usually necessary to provide assumptions about the environment in which a subsystem executes. Because developing assumptions has been a difficult manual task, the evaluation of assume-guarantee reasoning has been limited. Using recent advances for automatically generating assumptions, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. In this study, we considered all two-way decompositions for a set of systems and properties, using two different verifiers, FLAVERS and LTSA. By increasing the number of repeated tasks in these systems, we evaluated the decompositions as they were scaled. We found that in only a few cases can assume-guarantee reasoning verify properties on larger systems than monolithic verification can, and in these cases the systems that can be analyzed are only a few sizes larger. Although these results are discouraging, they provide insight about research directions that should be pursued and highlight the importance of experimental evaluation in this area.
Stephen F. Siegel and George S. Avrunin. Verification of halting properties for MPI programs using nonblocking operations. In Franck Capello, Thomas Herault, and Jack Dongarra, editors, Recent Advances in Parallel Virtual Machine and Message Passing Interface: 14th European PVM/MPI Users' Group Meeting, volume 4757 of Lecture Notes in Computer Science, pages 326–334, Paris, September 2007. Springer-Verlag. [ DOI | .pdf ]
We show that many important properties of certain MPI programs can be verified by considering only a class of executions in which all communication takes place synchronously. In previous work, we showed that similar results hold for MPI programs that use only blocking communication (and avoid certain other constructs, such as MPI_ANYSOURCE); in this paper we show that the same conclusions hold for programs that also use the nonblocking functions MPI_ISEND, MPI_IRECV, and MPI_WAIT. These facts can be used to dramatically reduce the number of states explored when using model checking techniques to verify properties such as freedom from deadlock in such programs.
Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In Mauro Pezzé, editor, Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 157–168, July 2006. [ DOI | .pdf ]
We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. The method requires that a sequential version of the program be provided, to serve as the specification for the parallel one. The key idea is to use model checking, together with symbolic computation, to establish the equivalence of the two programs.
Jamieson M. Cobleigh, George S. Avrunin, and Lori A. Clarke. Breaking up is hard to do: An investigation of decomposition for assume-guarantee reasoning. In Mauro Pezzé, editor, Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 97–108, Portland, ME, July 2006. [ DOI | .pdf ]
Finite-state verification techniques are often hampered by the state-explosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning. Using recent advances in assume-guarantee reasoning that automatically generate assumptions, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. In this study, we considered all two-way decompositions for a set of systems and properties, using two different verifiers, FLAVERS and LTSA. By increasing the number of repeated tasks, we evaluated the decompositions as the systems were scaled. In only a few cases could assume-guarantee reasoning verify properties on larger systems than monolithic verification and, in these cases, assume-guarantee reasoning could only verify these properties on systems a few sizes larger than monolithic verification. This discouraging result, although preliminary, raises doubts about the usefulness of assume-guarantee reasoning.
Jianbin Tan, George S. Avrunin, and Lori A. Clarke. Managing space for finite-state verification. In Proceedings of the 28th International Conference on Software Engineering, pages 152–161, Shanghai, May 2006. [ DOI | .pdf ]
Finite-state verification (FSV) techniques attempt to prove properties about a model of a system by examining all possible behaviors of that model. This approach suffers from the so-called state-explosion problem, where the size of the model or the analysis costs may be exponentially large with respect to the size of the system. Approaches that use symbolic data structures to represent the examined state space appear to provide an important optimization. In this paper, we investigate applying two symbolic data structures, Binary Decision Diagrams (BDDs) and Zero-suppressed Binary Decision Diagrams (ZDDs), in two FSV tools, LTSA and FLAVERS. We describe an experiment showing that these two symbolic approaches can improve the performance of both FSV tools and are more efficient than two other algorithms that store the state space explicitly. Moreover, the ZDD-based approach often runs faster and can handle larger systems than the BDD-based approach.
Jianbin Tan, George S. Avrunin, Lori A. Clarke, Shlomo Zilberstein, and Stefan Leue. Heuristic-guided counterexample search in FLAVERS. In Matthew Dwyer, editor, Proceedings of the 12th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 201–210, Newport Beach, CA, November 2004. [ DOI | .pdf ]
One of the benefits of finite-state verification (FSV) tools, such as model checkers, is that a counterexample is provided when the property cannot be verified. Not all counterexamples, however, are equally useful to the analysts trying to understand and localize the fault. Often counterexamples are so long that they are hard to understand. Thus, it is important for FSV tools to find short counterexamples and to do so quickly. Commonly used search strategies, such as breadth-first and depth-first search, do not usually perform well in both of these dimensions. In this paper, we investigate heuristic-guided search strategies for the FSV tool FLAVERS and propose a novel two-stage counterexample search strategy. We describe an experiment showing that this two-stage strategy, when combined with appropriate heuristics, is extremely effective at quickly finding short counterexamples for a large set of verification problems.
Jianbin Tan, George S. Avrunin, and Lori A. Clarke. Heuristic-based model refinement for FLAVERS. In Proceedings of the Twenty-Sixth International Conference on Software Engineering, pages 635–644, May 2004. [ .pdf ]
FLAVERS is a finite-state verification approach that allows an analyst to incrementally add constraints to improve the precision of the model of the system being analyzed. Except for trivial systems, however, it is impractical to compute which constraints should be selected to produce precise results for the least cost. Thus, constraint selection has been a manual task, guided by the intuition of the analyst. In this paper, we investigate several heuristics for selecting task automaton constraints, a kind of constraint that tends to reduce infeasible task interactions. We describe an experiment showing that one of these heuristics is extremely effective at improving the precision of the analysis results without significantly degrading performance.
Stephen F. Siegel and George S. Avrunin. Improving the precision of INCA by eliminating solutions with spurious cycles. IEEE Trans. Softw. Eng., 28(2):115–128, 2002. (This is a revised and expanded version of a paper that originally appeared in ISSTA 2000.). [ DOI | .pdf ]
The Inequality Necessary Condition Analyzer (INCA) is a finite-state verification tool that has been able to check properties of some very large concurrent systems. INCA checks a property of a concurrent system by generating a system of inequalities that must have integer solutions if the property can be violated. There may, however, be integer solutions to the inequalities that do not correspond to an execution violating the property. INCA thus accepts the possibility of an inconclusive result in exchange for greater tractability. We describe here a method for eliminating one of the two main sources of these inconclusive results.
George S. Avrunin, James C. Corbett, and Matthew B. Dwyer. Benchmarking finite-state verifiers. Software Tools for Technology Transfer, 2(4):317–320, 2000. [ DOI | .pdf ]
A variety of largely automated methods have been proposed for finite-state verification of software systems. Although anecdotal accounts of success are widely reported, there is very little empirical data on the relative strengths and weaknesses of those methods across a broad range of analysis questions and systems. But this information is critical for the transfer of the technology from research to practice. We review some of the problems involved in obtaining this information and suggest several ways in which the community can facilitate empirical evaluation of finite-state verification tools.
George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Păsăreanu, and Stephen F. Siegel. Comparing finite-state verification techniques for concurrent software. Technical Report UM-CS-1999-069 (revised February 2000), Department of Computer Science, University of Massachusetts, November 1999. [ .ps ]
Finite-state verification provides software developers with a powerful tool to detect errors. Many different analysis techniques have been proposed and implemented, and the limited amount of empirical data available shows that the performance of these techniques varies enormously from system to system. Before this technology can be transferred from research to practice, the community must provide guidance to developers on which methods are best for different kinds of systems. We describe a substantial case study in which several finite-state verification tools were applied to verify properties of the Chiron user interface system, a real Ada program of substantial size. Our study provides important data comparing these different analysis methods, and points out a number of difficulties in conducting fair comparisons of finite-state verification tools.
Gleb Naumovich, George S. Avrunin, and Lori A. Clarke. An efficient algorithm for computing MHP information for concurrent Java programs. In O. Nierstrasz and M. Lemoine, editors, Software Engineering—ESEC/FSE '99. 7th European Software Engineering Conference held jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, number 1687 in LNCS, pages 338–354, Toulouse, September 1999. [ DOI | .pdf ]
Information about which statements in a concurrent program may happen in parallel (MHP) has a number of important applications. It can be used in program optimization, debugging, program understanding tools, improving the accuracy of data flow approaches, and detecting synchronization anomalies, such as data races. In this paper we propose a data flow algorithm for computing a conservative estimate of the MHP information for Java programs that has a worst-case time bound that is cubic in the size of the program. We present a preliminary experimental comparison between our algorithm and a reachability analysis algorithm that determines the “ideal” static MHP information for concurrent Java programs. This initial experiment indicates that our data flow algorithm precisely computed the ideal MHP information in the vast majority of cases we examined. In the two out of 29 cases where the MHP algorithm turned out to be less than ideally precise, the number of spurious pairs was small compared to the total number of ideal MHP pairs.
Gleb Naumovich, George S. Avrunin, and Lori A. Clarke. Data flow analysis for checking properties of concurrent Java programs. In Proceedings of the Twenty-First International Conference on Software Engineering, pages 399–410, Los Angeles, May 1999. [ DOI | .pdf ]
In this paper we show how the FLAVERS data flow analysis technique, originally formulated for programs with the rendezvous model of concurrency, can be applied to concurrent Java programs. The general approach of FLAVERS is based on modeling a concurrent program as a flow graph and using a data flow analysis algorithm over this graph to check statically if a property holds on all executions of the program. The accuracy of this analysis can be improved by supplying additional information, represented as finite state automata, to the data flow analysis algorithm.In this paper we present a straightforward approach for modeling Java programs that uses the accuracy improving mechanism to represent the possible communications among threads in Java programs, instead of representing them directly in the flow graph model. We also discuss a number of error-prone thread communication patterns that can arise in Java and describe how FLAVERS can be used to check for the presence of these.
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the Twenty-First International Conference on Software Engineering, pages 411–420, Los Angeles, May 1999. [ DOI | .pdf ]
Model checkers and other finite-state verification tools allow developers to detect certain kinds of errors automatically. Nevertheless, the transition of this technology from research to practice has been slow. While there are a number of potential causes for reluctance to adopt such formal methods, we believe that a primary cause is that practitioners are unfamiliar with specification processes, notations, and strategies. In a recent paper, we proposed a pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification. Since then, we have carried out a survey of available specifications, collecting over 500 examples of property specifications. We found that most are instances of our proposed patterns. Furthermore, we have updated our pattern system to accommodate new patterns and variations of existing patterns encountered in this survey. This paper reports the results of the survey and the current status of our pattern system.
Gleb Naumovich and George S. Avrunin. A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. In Proceedings of 6th International Symposium on the Foundations of Software Engineering, pages 24–34, November 1998. [ DOI | .pdf ]
Information about which pairs of statements in a concurrent program can execute in parallel is important for optimizing and debugging programs, for detecting anomalies, and for improving the accuracy of data flow analysis. In this paper, we describe a new data flow algorithm that finds a conservative approximation of the set of all such pairs. We have carried out an initial comparison of the precision of our algorithm and that of the most precise of the earlier approaches, Masticola and Ryder's non-concurrency analysis, using a sample of 159 concurrent Ada programs that includes the collection assembled by Masticola and Ryder. For these examples, our algorithm was almost always more precise than non-concurrency analysis, in the sense that the set of pairs identified by our algorithm as possibly happening in parallel is a proper subset of the set identified by non-concurrency analysis. In 132 cases, we were able to use reachability analysis to determine exactly the set of pairs of statements that may happen in parallel. For these cases, there were a total of only 10 pairs identified by our algorithm that cannot actually happen in parallel.
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Mark Ardis, editor, Proceedings of FMSP '98, the Second Workshop on Formal Methods in Software Practice, pages 7–15, Clearwater Beach, FL, March 1998. [ DOI | .pdf ]
Finite-state verification (e.g., model checking) provides a powerful means to detect errors that are often subtle and difficult to reproduce. Nevertheless, the transition of this technology from research to practice has been slow. While there are a number of potential causes for reluctance in adopting such formal methods in practice, we believe that a primary cause rests with the fact that practitioners are unfamiliar with specification processes, notations, and strategies. Recent years have seen growing success in leveraging experience with design and coding patterns. We propose a pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification.
Gleb Naumovich, George S. Avrunin, Lori A. Clarke, and Leon J. Osterweil. Applying static analysis to software architectures. In Mehdi Jazayeri and Helmut Schauer, editors, Software Engineering—ESEC/FSE '97, volume 1301 of Lecture Notes in Computer Science, pages 77–93, Zurich, September 1997. Springer Verlag. [ DOI | .pdf ]
In this paper we demonstrate how static concurrency analysis techniques can be used to verify application-specific properties of an architectural description. Specifically, we use two concurrency analysis tools, INCA, a flow equation based tool, and FLAVERS, a data flow analysis based tool, to detect errors or prove properties of a Wright architectural description of the gas station problem. Although both these tools are research prototypes, they illustrate the potential of static analysis for verifying that architectural descriptions adhere to important properties, for detecting problems early in the lifecycle, and for helping developers understand the changes that need to be made to satisfy the properties being analyzed.
George S. Avrunin. Symbolic model checking using algebraic geometry. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 26–37, New Brunswick, NJ, July 1996. Springer-Verlag. [ DOI | .ps ]
In this paper, I show that methods from computational algebraic geometry can be used to carry out symbolic model checking using an encoding of Boolean sets as the common zeros of sets of polynomials. This approach could serve as a useful supplement to symbolic model checking methods based on Ordered Binary Decision Diagrams and may provide important theoretical insights by bringing the powerful mathematical machinery of algebraic geometry to bear on the model checking problem.
A. T. Chamillard, Lori A. Clarke, and George S. Avrunin. An empirical comparison of static concurrency analysis techniques. Technical Report 96-84, Department of Computer Science, University of Massachusetts, 1996. Revised May 1997. [ .ps ]
This paper reports the results of an empirical comparison of several static analysis tools for evaluating properties of concurrent systems and also reports the results of our attempts to build predictive models for each of the tools based on program and property characteristics. Although this area seems well-suited to empirical investigation, we encountered a number of significant issues that make designing a sound and unbiased study surprisingly difficult. These experimental design issues are also discussed in this paper.
George S. Avrunin. Concurrent and real-time systems. In Quality-Enhancing Software Technologies. Microelectronics and Computer Technology Corporation (MCC), 1996.
James C. Corbett and George S. Avrunin. Using integer programming to verify general safety and liveness properties. Formal Methods in System Design, 6:97–123, January 1995. [ DOI | .ps ]
Analysis of concurrent systems is plagued by the state explosion problem. The constrained expression analysis technique uses necessary conditions, in the form of linear inequalities, to verify certain properties of concurrent systems, thus avoiding the enumeration of the potentially explosive number of reachable states of the system. This technique has been shown to be capable of verifying simple safety properties, like freedom from deadlock, that can be expressed in terms of the number of certain events occurring in a finite execution, and has been successfully used to analyze a variety of concurrent software systems. We extend this technique to the verification of more complex safety properties that involve the order of events and to the verification of liveness properties, which involve infinite executions.
James C. Corbett and George S. Avrunin. Towards scalable compositional analysis. In David Wile, editor, Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 53–61, New Orleans, December 1994. ACM Press. [ DOI | .pdf ]
Due to the state explosion problem, analysis of large concurrent programs will undoubtedly require compositional techniques. Existing compositional techniques are based on the idea of replacing complex subsystems with simpler processes with the same interfaces to their environments, and using the simpler processes to analyze the full system. Most algorithms for proving equivalence between two processes, however, require enumerating the states of both processes. When part of a concurrent system consists of many highly coupled processes, it may not be possible to decompose the system into components that are both small enough to enumerate and have simple interfaces with their environments. In such cases, analysis of the systems by standard methods will be infeasible.In this paper, we describe a technique for proving trace equivalence of deterministic and divergence-free systems without enumerating their states. (For deterministic systems, essentially all the standard notions of process equivalence collapse to trace equivalence, so this technique also establishes failures equivalence, observational equivalence, etc.) Our approach is to generate necessary conditions for the existence of a trace of one system that is not a trace of the other; if the necessary conditions cannot be satisfied the systems are equivalent. We have implemented the technique and used it to establish the equivalence of some systems with state spaces too large for enumeration to be practical.
Victor Yodaiken and George S. Avrunin. Real-time state machines and circuit verification with modal functions. Technical Report 93-04, Department of Computer Science, University of Massachusetts at Amherst, 1993.
Recent work on automated verification of circuits has highlighted the problems of concise representation, composition, and manipulation of state machines with large state sets. In this paper, we show how state machines that capture both the real-time behavior and connective structure of circuits can be defined, parameterized, composed, and refined, using modal functions. Our work is currently focused on "by hand" methods of verification as a step towards automated methods.
George S. Avrunin, Ugo A. Buy, James C. Corbett, Laura K. Dillon, and Jack C. Wileden. Automated analysis of concurrent systems with the constrained expression toolset. IEEE Trans. Softw. Eng., 17(11):1204–1222, November 1991. [ DOI | .pdf ]
The constrained expression approach to analysis of concurrent software systems has several attractive features, including the facts that it can be used with a variety of design and programming languages and that it does not require a complete enumeration of the set of reachable states of the concurrent system. This paper reports on the construction of a toolset automating the main constrained expression analysis techniques and the results of experiments with that toolset. The toolset is capable of carrying out completely automated analyses of a variety of concurrent systems, starting from source code in an Ada-like design language and producing system traces displaying the properties represented by the analyst's queries. It has been successfully used with designs that involve hundreds of concurrent processes.
George S. Avrunin, Ugo A. Buy, James C. Corbett, Laura K. Dillon, and Jack C. Wileden. Experiments with an improved constrained expression toolset. In Proceedings of the Symposium on Testing, Analysis, and Verification (TAV4), pages 178–187. ACM SIGSOFT, October 1991. [ DOI | .pdf ]
At TAV3, we described a prelimiminary version of the constrained expression toolset, and reported on the results of our initial experiments with it. Through those experiments we discovered shortcomings in some of the tools that limited the size of the examples that we could analyze. We have since redesigned and reimplemented several components of the toolset, with performance improvements of more than two orders of magnitude in some cases. The improved toolset has been successfully used with designs that involve hundreds of concurrent processes. In this paper, we describe several experiments with the new version of the toolset, including preliminary experiments with a technique for analyzing sys- tems that include an essentially arbitrary number of identical components.
George S. Avrunin, Ugo A. Buy, and James C. Corbett. Integer programming in the analysis of concurrent systems. In Kim Guldstand Larsen and Arne Skou, editors, Computer Aided Verification, 3rd International Workshop Proceedings, volume 575 of Lecture Notes in Computer Science, pages 92–102, Aalborg, Denmark, July 1991. Springer-Verlag. [ DOI ]
George S. Avrunin, Ugo Buy, and James Corbett. Automatic generation of inequality systems for constrained expression analysis. Technical Report 90-32, Department of Computer and Information Science, University of Massachusetts, Amherst, 1990.
George S. Avrunin, Laura K. Dillon, and Jack C. Wileden. Experiments with automated constrained expression analysis of concurrent software systems. In Richard A. Kemmerer, editor, Proceedings of the ACM SIGSOFT '89 Third Symposium on Software Testing, Analysis and Verification, pages 124–130, December 1989. [ DOI | .pdf ]
It is unlikely that any single approach to analysis of concurrent software systems will meet all the needs of software developers throughout the development process. Thus, experimental evaluation of different analysis techniques is needed to determine their relative strengths and practical limitations. Such evaluation requires automated tools implementing the analysis techniques. This paper describes a prototype toolset automating the constrained expression approach to the analysis of concurrent software systems. The results of preliminary experiments with the toolset are reported and the implications of these experiments are discussed.
Laura K. Dillon, George S. Avrunin, and Jack C. Wileden. Constrained expressions: Toward broad applicability of analysis methods for distributed software systems. ACM Trans. Prog. Lang. Syst., 10(3):374–402, July 1988. [ DOI | .pdf ]
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.
Jack C. Wileden and George S. Avrunin. Toward automating analysis support for developers of distributed software. In Proceedings of the Eighth International Conference on Distributed Computing Systems, pages 350–357. IEEE Computer Society Press, June 1988. [ DOI | .pdf ]
George S. Avrunin. A prototype inequality generator. Software Development Laboratory Memo 88-1, Department of Computer and Information Science, University of Massachusetts, Amherst, June 1988.
George S. Avrunin. Experiments in constrained expression analysis. Technical Report 87-125, Department of Computer and Information Science, University of Massachusetts, Amherst, 1987.
George S. Avrunin, Laura K. Dillon, Jack C. Wileden, and William E. Riddle. Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems. IEEE Trans. Softw. Eng., SE-12(2):278–292, 1986. Reprinted in: S. M. Shatz and J.-P. Wang, eds., Tutorial: Distributed-Software Engineering, IEEE Computer Society Press, Washington, DC (1989), pp. 258–271.
George S. Avrunin and Jack C. Wileden. Describing and analyzing distributed software system designs. ACM Trans. Prog. Lang. Syst., 7(3):380–403, July 1985. [ DOI | .pdf ]
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.
George S. Avrunin and Jack C. Wileden. Algebraic techniques for the analysis of concurrent systems. In Proceedings of the Sixteenth Hawaii International Conference on Systems Sciences, pages 51–57, 1983.
This file was generated by bibtex2html 1.99.
![[Back]](/icons/back.gif){kind=icon}
Back to George Avrunin's home page