Verifying concurrent system specifications in COSY

In this paper we illustrate the use of the COSY formalism [LTS79] for specifying, analysing and verifying highly parallel and distributed systems. We shall do this through a non-trivial example, the concurrent resource release mechanism which forms the central part of a novel, non-computational, concurrent and distributed solution to the problem of allocating reusable resources from a limited pool among a large number of concurrent users, the …