Specification and design of shared resource arbitration

The specification, modular design and verification of distributed communicating systems is demonstrated by an example. The scheduling of the access to a common shared resource by a finite number of devices with priorities is a well known problem from hardware and operating systems design. Using the concepts of stream processing continuous function a variety of formal requirement and design specifications for this problem are given and the design specifications are proven correct w.r.t the requirement specifications. From the design specifications one can immediately read off applicative programs implementing the requirement specifications. Special attention is paid to the aspect of modelling time.