A Software Environment for the Specification and Analysis of Problems of Coordination and Concurrency.

In today's distributed computing environment, the coordination of concurrent processes and the coordination of resource sharing are of critical importance. Consequently, much effort has been focused on the modeling of problems of coordination and concurrency. In this paper we describe a software environment (SPANNER) for the specification and analysis of such problems. In the SPANNER environment, one can formally produce a specification of a distributed computing problem, and then verify its "correctness" through reachability analysis and simulation. SPANNER is based on a finite state machine model called the selection/resolution model. We illustrate the capabilities of SPANNER by specifying and analyzing two classical coordination problems: 1) the dining philosophers; and 2) Dijkstra's concurrent programming problem. In addition to discussing these specific problems, our intention is also to focus on some of the more recently implemented capabilities of the SPANNER system such as process types and cluster variables. [ABSTRACT FROM AUTHOR]