Checking Deadlock-Freedom of Parametric Component-Based Systems

TL;DR

This paper introduces an automated symbolic method to verify deadlock-freedom in parametric component-based systems by computing inductive invariants, extending previous approaches to more general architectures.

Contribution

It generalizes the computation of structural trap invariants from bounded to parametric systems with complex architectures, supported by new theoretical results.

Findings

Method successfully computes trap invariants for parametric systems.

Theoretical foundations include new results in first-order monadic logic.

Preliminary examples demonstrate the method's applicability.

Abstract

We propose an automated method for computing inductive invariants applied to check deadlock-freedom for parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from a monadic interaction formula characterizing the system architecture. The paper presents the theoretical foundations of the method including new results for the first order monadic logic and proves its soundness. It also provides preliminary illustrations on examples.