Port Protocols for Deadlock-Freedom of Component Systems

TL;DR

This paper introduces port protocols as a minimalistic approach to verify deadlock-freedom in component systems without analyzing entire global or local behaviors.

Contribution

It proposes a novel method using port protocols to verify system properties efficiently, bypassing traditional global and local behavior analysis.

Findings

Port protocols effectively verify deadlock-freedom.

The approach reduces analysis complexity.

It enables property verification with minimal behavior models.

Abstract

In component-based development, approaches for property verification exist that avoid building the global system behavior of the component model. Typically, these approaches rely on the analysis of the local behavior of fixed sized subsystems of components. In our approach, we want to avoid not only the analysis of the global behavior but also of the local behaviors of the components. Instead, we consider very small parts of the local behaviors called port protocols that suffice to verify properties.