Dynamic Consistency in Process Algebra: From Paradigm to ACP

The coordination modelling language Paradigm addresses collaboration between components in terms of dynamic constraints. Within a Paradigm model, component dynamics are consistently specified at various levels of abstraction. The operational semantics of Paradigm is given. For a large, general subclass of Paradigm models a translation into process algebra is provided. Once expressed in process algebra, relying on a correctness result, Paradigm models are amenable to process algebraic reasoning and to verification via the mCRL2 toolset. Examples of a scheduling problem illustrate the approach.