Verification of component-based systems with recursive architectures

We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the descrip-tion of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe al-gebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical sec-tion are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invari-ants allowing the proof of general safety properties. The invariants are defined using the WS kappa S fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection, thus reducing a verification problem to checking satisfiability of a WS kappa S formula.(c) 2022 Elsevier B.V. All rights reserved.