The SPANNER software environment for the specification and analysis of concurrent process coordination and resource sharing coordination is described. In the SPANNER environment, one can formally produce a specification of a distributed computing problem, and then verify its validity through reachability analysis and simulation. SPANNER is based on a finite-state machine model called the selection/resolution model. The capabilities of SPANNER are illustrated by the analysis of two classical coordination problems: (1) the dining philosophers; and (2) Dijkstra's concurrent programming problem. In addition, some of the more recently implemented capabilities of the SPANNER system are discussed, such as process types and cluster variables.
展开▼
