Algorithmic Analysis of Infinite-State Concurrent Systems

Опубликовано 7 сентября 2016, 17:14

With the establishment of the multi-core processors and distributed applications, concurrency has become commonplace in application software. The design and implementation of concurrent software is notoriously error-prone. In large, this is due to the non-deterministic interactions among concurrently executing processes. Unfortunately, verification of concurrent systems is notoriously hard as well. In part, this is due to the fact that many important concurrent systems are naturally infinite-state. Algorithmic analysis of infinite-state models is complicated -- most interesting properties are undecidable for sufficiently expressive classes of infinite-state models. In this talk, we give an overview of algorithmic analysis techniques for two important classes of infinite-state models: FIFO Systems and Parameterized Systems. FIFO systems consist of a set of finite-state machines that communicate via unbounded, perfect, FIFO channels. We study the problem of computing the set of reachable states of a FIFO system composed of piecewise components. We show that this set is piecewise in general. We also give effective algorithms to calculate the reachable states of a single-channel and classes of multi-channel piecewise FIFO systems. Parameterized systems are a common model of computation for concurrent systems consisting of an arbitrary number of homogeneous processes. We study the reachability problem in parameterized systems in which each process is infinite-state as well. We describe a framework that combines Abstract Interpretation with a backward-reachability algorithm. Our key idea is to create an abstract domain in which each element represents the lower bound on the number of processes at a control location and employs a numeric abstract domain to capture arithmetic relations among variables of the processes. We also provide an extrapolation operator for the domain to guarantee sound termination of the backward-reachability algorithm.