Reasoning about distributed message passing systems

DSpace/Manakin Repository

Reasoning about distributed message passing systems

Show simple item record Meenakshi, B. 2009-09-10T07:08:26Z 2009-09-10T07:08:26Z 2009-09-10T07:08:26Z 2004
dc.description.abstract 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. en_US
dc.subject Modal Logic en_US
dc.subject Distributed Systems en_US
dc.subject Model Checking en_US
dc.subject Communication Patterns en_US
dc.title Reasoning about distributed message passing systems en_US Ph.D en_US
dc.type.institution University of Madras en_US
dc.description.advisor Ramanujam, R.
dc.description.pages vi; 161p. en_US
dc.type.mainsub Computer Science en_US

Files in this item

Files Size Format View
UNMTH81.pdf 925.5Kb PDF View/Open

This item appears in the following Collection(s)

Show simple item record

Search DSpace

Advanced Search


My Account