My research area is in the overlap of distributed computing, formal methods, and fsoftware engineering. 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. This work was initiated as part of my PhD thesis, under the supervision of Allen Emerson, and I have continued and developed it since graduating.
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 has implemented the pairwise reduction and analysis method ).
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. 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:
I am also working on method for writing formal specifications by using exmaple input-output pairs. This is in collaboration with Fadi Zaraket, Mohamad Noureddine, and Farah Al-Hariri.