Arcadia Papers: ABSTRACT
"Compositional Reachability Analysis of Ada Programs Using Process
Algebra", by Wei Jen Yeh and Michal Young in
Proceedings of the Fourth ACM SIGSOFT Symposium on Software Testing,
Analysis, and Verification,
Victoria, British Columbia, October 1991, ACM Press.
Abstract
State explosion is the primary obstacle to practical application of
reachability analysis techniques for detecting potential synchronization
faults (deadlocks, races, etc.) in concurrent systems. Process algebras
provide a useful theoretical framework for avoiding state explosion
by applying reductions at intermediate steps in a compositional analysis
of a large system. We report on an implementation and experience with a
tool that uses algebraic structure to perform modular, hierarchical
analysis of systems described in an Ada-based PDL, and report on
application to a collection of well-known example problems. Although
algebraic properties are fundamental to the approach, basic algebraic
operations are a small portion of the tool. Pre-analysis of the scope
structure and communication topology of the system under test, and
data flow analysis and controlled symbolic expansion of source code
are essential to avoiding state explosion in practice.
The Arcadia Project
<arcadia-www@ics.uci.edu>
Last modified: Thu Jan 27 13:36:13 1995