Towards reduction of Paradigm coordination models

TL;DR

This paper explores reducing Paradigm coordination models using global inertness and process algebra, enabling analysis of larger models while preserving key properties.

Contribution

It introduces a reduction technique for Paradigm models based on global inertness, facilitating automated verification and analysis of larger systems.

Findings

Reduction based on global inertness preserves properties.

Enables analysis of larger Paradigm models.

Process algebraic specifications support model equivalence.

Abstract

The coordination modelling language Paradigm addresses collaboration between components in terms of dynamic constraints. Within a Paradigm model, component dynamics are consistently specified at a detailed and a global level of abstraction. To enable automated verification of Paradigm models, a translation of Paradigm into process algebra has been defined in previous work. In this paper we investigate, guided by a client-server example, reduction of Paradigm models based on a notion of global inertness. Representation of Paradigm models as process algebraic specifications helps to establish a property-preserving equivalence relation between the original and the reduced Paradigm model. Experiments indicate that in this way larger Paradigm models can be analyzed.