On the Automated Verification of Parameterized Concurrent Systems with Unbounded Local Data

We present a sound and fully automated method for the verification of safety properties of parameterized systems with unbounded local data variables, a new class of infinite-state systems parametric in several dimensions. The method builds upon a specification and an assertional language based on the combination of multiset rewriting and constraints. We also consider a global synchronization mechanism that can be used to simulate brodcast communication. By a careful choice of constraints systems and rewrite rules, we isolate new classes of parameterized systems for which verification of safety properties is decidable, and we introduce abstractions, defined at the level of constraints, to handle examples outside these classes. As case-studies, we apply the method to verify fully automatically mutual exclusion properties for: several formulations of the ticket mutual exclusion algorithm parametric in the number of clients, servers, and in which both clients and servers have unbounded local data; the Li-Hudak's coherence protocol for distributed systems with shared virtual memory, and several cache coherence protocols for multiprocessor systems and caches an arbitrary number of lines