Reasoning about distributed message passing systems

2004

Ph.D

University of Madras

This thesis is concerned with the use of formal methods towards automatic verification of distributed message passing systems with a fixed finite number of agents. Main concentration is on developing logics to reason about behaviours of these systems. Many protocols are systems which consist of repetitions of a fixed number of finite communication patterns. The behaviour of such systems is modeled using Layered Lamport Diagrams(LLDs). Model checking is a fully automatic way of doing formal verification where the program is modelled as a finite transition system and the specification is given as a formula in some logic, usually temporal logic. 'Automata Theoretic approach' is one, well-established way of doing model checking, in which it is mainly observed that one can construct a finite state automaton that accepts the set of all sequences(Models) that satisfy the given formula. This approach to solve the model checking problem is also useful to show that the satisfiability problem for temporal logics is decidable. This problem is decidable for finite state automata, and an algorithm is obtained for solving the satisfiability problem for the logic. The main aim of this thesis is to develop suitable models to describe behaviours of distributed message passing systems and to come up with suitable logics to reason about them. Also certain models are proposed for distributed systems and use these system models to solve the satisfiability problem of logic that is considered. It is targetted to come up with local event based models describing behaviours and suitable logics which talk about the way in which local computations evolve.