Algorithmic Analysis of Infinite-State Concurrent Systems

June 29, 2009
Naghmeh Ghafari | University of Waterloo, Ontario

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.

Speaker Details

Naghmeh Ghafari received a Ph.D. (2009) in Computer Science from the University of Waterloo, Ontario, a M.A.Sc. (2003) in Computer Engineering from the University of Waterloo, and a B.A.Sc. (2000) in Electrical Engineering from the University of Tehran, Iran. Her research interests include formal analysis of concurrent and distributed systems, model-checking, and algorithmic analysis of infinite-state systems. She has been an instructor for Software Requirements Analysis course at the University of British Columbia, BC. Currently, she is a visiting scholar at the Integrated System Design Lab of the University of British Columbia. She was a recipient of the NSERC Doctorate Scholarship and the Ontario Graduate Scholarship.