A Formal Definition of Priority in CSP

Abstract

The process models of Ada and occam are formally based on the CSP process algebra. However, for fine-tuning real-time performance, they include “prioritized” constructs that have no counterparts in CSP. These constructs therefore lack any formal definition, a situation that leaves room for misunderstandings. We extend CSP with a formal definition of the notion of priority. The definition is then used to assess the transputer implementation of priority in occam and the definition of priority in Ada.