EFSM specication Exercise 2: Arbiter

Arbiter is a mechanism for allocating resources eciently in concurrent systems. The purpose of this exercise is to model an arbiter which allocates resources to two processes P and Q in such a way that every process eventually gets the requested resource. The following constraints apply for resource sharing between processes:

R is a nite set of resources. for r R there exists tr N, denoting the maximum utilization time. a process can request the arbiter for any resource in R. arbiter will accept all requests from P and Q. every resource requested by a process should be allocated to it by the arbiter. a process which received a resource r at time t must return it to the arbiter before time t + tr.

Give an EFSM specication for the system.