Pairwise Components and Automata Group
Department of Computer Science
American University of Beirut
My research area is in the overlap of distributed computing and formal methods. I am interested in the formulation of methodologies for the the design of large distributed systems that (1) establish formally stated \emph{correctness properties} for these systems, and (2) do not suffer from current drawbacks of formal methods: high computational complexity, or the need for large amounts of manual effort by the verification engineers.
My research addresses the problems arising from the composition of a large number of software modules running concurrently, chiefly state explosion. Given a system P1 || ... || Pn, I analyze the properties of each pair Pi || Pj of interacting processes. These pair-systems are small enough that state-explosion is not a problem. This method can be used both for program synthesis (produce the pairs Pi || Pj first, then combine them to produce the overall system) or for program analysis (extract pairs from overall system, analyze pairs, and then conclude correctness of overall system). I have used this approach to synthesis or verify the following examples: mutual exclusion, n-out-of-K mutual-exclusion, generalized dining and drinking philosophers, readers-writers, two-phase commit, extended (relaxed) transaction models, replicated data service (infinite-state), and an elevator control algorithm.
My approach of reduction to pair-systems is different from the traditional approach of compositional verification because the same process can occur in several pair-systems. In compositional verificaiton, the system is decomposed into disjoint sub-systems that are then analyzed separately, and the results then combined to verify the overall system. I am currently extending my approach from pair-systems to small subsystems, which can contain more than two processes, and which can overlap with each other. My group is currently implementing the pair-wise method in the (Tempo toolset).
By providing a method of decomposing a large complex system into small, manageable subsystems (or pair-systems), my research attacks the "essential complexity" of the software problem, as stated by Fred Brooks. If we use automata as a requirements notation, my work also has implications for problem decomposition, as discussed by Michael Jackson.
My research also addresses the problem of constructing a pair-system Pi || Pj, by building a model for it and then extracting Pi and Pj from this model. I am currently working on algorithms for constructing and modifying models so that they satsify a given specification. Among the applications of this work is the synthesis of component adapters. To complement and provide a foundation for my work on synthesis and analysis of large distributed systems, I also undertake research in the semantics of concurrency:
Some of my research is conducted in collaboration with the MIT Theory of Distributed Systems group.