Abstract
A fundamental issue in the automated analysis of concurrent systems is the efficient generation of the reachable state space. Since it is not possible to explore all the reachable states of a system if the number of states is very large or infinite, we need to develop techniques for minimizing the state space. This paper presents our approach to cluster subsets of states into equivalent classes. We assume that concurrent systems are specified as communicating state machines with arbitrary data space. We describe a procedure for constructing a minimal reachability state graph from communicating state machines. As an illustration of our approach, we analyze a producer-consumer program written in Ada.
| Original language | English |
|---|---|
| Pages | 123-134 |
| Number of pages | 12 |
| State | Published - 1994 |
| Event | Proceedings of the 9th Annual Conference on Computer Assurance, COMPASS'94 - Gaithersburg, MD, USA Duration: 27 Jun 1994 → 1 Jul 1994 |
Conference
| Conference | Proceedings of the 9th Annual Conference on Computer Assurance, COMPASS'94 |
|---|---|
| City | Gaithersburg, MD, USA |
| Period | 27/06/94 → 1/07/94 |