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.


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 <>
Last modified: Thu Jan 27 13:36:13 1995