Department of Computer Science
Modern distributed transactional information are large and fairly complex due to their underlying mechanisms for transaction support. These systems, classified as business critical systems, take advantage of data distribution and are expected to exhibit high degree of dependability. Any failure in these systems may lead to financial losses in addition to the potential loss of the trust of customers. Formal rigorous reasoning about the algorithms and mechanisms beneath such systems is required to precisely understand the behaviour of such systems at the design level. In such systems, formal verification aims at guaranteeing that such systems are free of programming bugs/errors and proving the correctness of intended algorithm/protocol underlying a software system with respect to a certain property. Our current research focus is on following themes.
Distributed systems are often difficult to understand, build and reason about due to their complex execution paths and unanticipated behaviours. A formal rigorous reasoning is usually required to precisely understand the model of distributed systems and get them right. In this line of work, we are working on refinement based approach for the construction of formal models of distributed systems. Our approach is based on Event-B, a formal technique for development of model of distributed systems. This formal technique consists of rigorous description of the problem in the abstract model and introducing the solution or design details in refinement steps. Through the refinement, we verify that the detailed design of a system in the refinement conforms to the initial abstract specifications. Existing B tools provide a strong proof support to aid reasoning about the safety properties by generating the proof obligations and providing an environment to discharge the proof obligations. We are currently using Rodin platform for Event-B, Pro-B model checker, Click_n_Prove B Tools.
The safety and live-ness are two important issues in the design and development of distributed systems. The safety properties express that something bad will not happen during system execution. A liveness property expresses that something good will eventually happens during the execution. To understand the safety and liveness properties of a system, we construct models of a proposed system using Event-B. With respect to the safety properties, the existing B tools generate proof obligations for consistency and refinement checking. These proof obligations may be discharged by using automatic/interative provers of B Tools. To ensure livness in the models of distributed systems, it is useful to state that the model of the system under development is non-divergent and enabledness preserving. In order to show that the new event in the refinement do not take control forever, i.e., models are non-divergent, we are currently focussing how useful a construction of an invariant property on variant is. To ensure that concrete models also make progress and do not block more often than its abstraction, it is necessary to prove that if an abstract model makes a progress due to the activation of events then the concrete model also make a progress due to the activation of the events in the refinement.
Database replication is traditionally envisaged as a way of increasing fault-tolerance and availability. A significant work has been done on the management of replicated data dealing various aspects, such as, fault-tolerance, consistency and performance. Most replica control mechanisms are usually complex, under-specified and difficult to reason about. Group communication has been proposed as a powerful mechanism for the management of replicated data. The existing work on the development of formal specifications of group communications services, ordering and reliability properties is often complicated, difficult to understand and sometime ambiguous. Application of formal methods to this problem to provide clear specifications and formal verification of the critical properties is rare. It is desirable that the models of distributed systems are precise and reasonably compact, and one expects that all the aspects of the system must be considered in the proofs. In this line of work, we are currently investigating various data replication techniques and application of various group communication primitives, by incremental construction of the models via a series of refinement steps using Event-B.
