Skip to main content

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

New Image

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.