ACSR: An algebra of communicating shared resources with dense time and priorities

Abstract

This paper describes a timed process algebra called ACSR. ACSR supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to accurately specify real systems, ACSR supports a dense time domain and a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. The paper also defines the compositionality of preemption and describes two fundamental ways to extend the priorities of individual events and actions to multiple events and actions without sacrificing compositionality.