Checking Deadlock-Freedom of Parametric Component-Based Systems

International audienceWe propose an automated method for computing inductive invariants used to proving deadlock freedom of 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 interaction formulae defining 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 reports on a preliminary experimental evaluation on several textbook examples. Modern computing systems exhibit dynamic and reconfigurable behavior. To tackle the complexity of such systems, engineers extensively use architectures that enforce, by construction, essential properties, such as fault tolerance or mutual exclusion. Architec-tures can be viewed as parametric operators that take as arguments instances of components of given types and enforce a characteristic property. For instance, client-server architectures enforce atomicity and resilience of transactions, for any numbers of clients and servers. Similarly, token-ring architectures enforce mutual exclusion between any number of components in the ring. Parametric verification is an extremely relevant and challenging problem in systems engineering. In contrast to the verification of bounded systems, consisting of a known set of components, there exist no general methods and tools succesfully applied to parametric systems. Verification problems for very simple parametric systems, even with finite-state components, are typically intractable [15,9]. Most work in this area puts emphasis on limitations determined mainly by three criteria (1) the topology of the architecture, (2) the coordination primitives, and (3) the properties to be verified. The main decidability results reduce parametric verification to the verification of a bounded number of instances of finite state components. Several methods try to determine a cutoff size of the system, i.e. the minimal size for which if a property holds, then it holds for any size, e.g. Suzuki [19], Emerson and Namjoshi [14]. Other methods identify systems with well-structured transition relations, for which symbolic enumeration of reachable states is feasible [1] or reduce to known decidable problems, such as reach-ability in vector addition systems [15]. Typically, these methods apply to systems with Institute of Engineering Univ. Grenoble Alpes The research leading to these results has received funding from the European Union Horizon 2020 research and innovation programme under grant agreement no. 700665 CITADEL (Criti-cal Infrastructure Protection using Adaptive MILS) and no. 730086 ERGO (European Robotic Goal-Oriented Autonomous Controller)