AIRCC's International Journal of Computer Science and Information Technology

Girish Chandra ¹, Raghuraj Suryavanshi ², Divakar Yadav ¹

Affiliations
1 Department of Computer Science and Engineering, Institute of Engineering and Technology, Lucknow, Uttar Pradesh 226021, IN
2 Department of Computer Science and Engineering, Pranveer Singh Institute of Technology, Kanpur, Uttar Pradesh 209305, IN

Abstract

The development of complex system makes challenging task for correct software development. Due to faulty specification, software may involve errors. The traditional testing methods are not sufficient to verify the correctness of such complex system. In order to capture correct system requirements and rigorous reasoning about the problems, formal methods are required. Formal methods are mathematical techniques that provide precise specification of problems with their solutions and proof of correctness. In this paper, we have done formal verification of check pointing process in a distributed database system using Event B. Event-B is an event driven formal method which is used to develop formal models of distributed database systems. In a distributed database system, the database is stored at different sites that are connected together through the network. Checkpoint is a recovery point which contains the state information about the site. In order to do recovery of a distributed transaction a global checkpoint number (GCPN) is required. A global checkpoint number decides which transaction will be included for recovery purpose. All transactions whose timestamp are less than global checkpoint number will be marked as before checkpoint transaction (BCPT) and will be considered for recovery purpose. The transactions whose timestamp are greater than GCPN will be marked as after checkpoint transaction (ACPT) and will be part of next global checkpoint number.

Keywords

Formal Methods, Formal Specifications, Formal Verification, Event-B, Distributed Transaction, Checkpointing, Local checkpoint Number, Global Checkpoint Number.

Full Text

   

Arun Kumar Singh ¹, Divakar Yadav ²

Affiliations
1 Department of Electronics Engg., IET, Lucknow, IN
2 Department of Computer Science and Engg., IET, Lucknow, IN

Abstract

A reliable broadcast is communication primitive used to develop fault tolerant distributed applications. It in due course delivers messages to all participating sites irrespective of their ordering. Total order broadcast impose restriction on message ordering and satisfies total order requirement.

A clear specifications, rigorous validation and verification is key to obtain better design of dependable services in such applications. With the help of formal methods one can specify and verify systems in systematic rather than ad hoc manner. It reveals ambiguities, incompleteness, and inconsistencies in a system by facilitating clear specification, rigorous validation and verification.

In this paper, we present a formal development of total order broadcast. The model have been developed and checked by using event-B techniques supported by the RODIN tool. Event-B is a formal technique that supports the incremental design of a distributed applications using notion of refinements.

Keywords

Total Order Broadcast, Event-B, Reliable Broadcast.

Full Text

   

Pooja Gupta ¹, A. K. Sharma ², Divakar Yadav ³

Affiliations
1 Department of Computer Science Engineering, MAIT, Rohini, New Delhi, IN
2 Department of Computer, YMCA University of Science and Technology, Faridabad, IN
3 Department of Computer Science and Information, JIITU, Noida, IN

Abstract

Focused Crawling aims to search the WWW in relevance to the user topic of interest, tends to provide more number of relevant documents in first top results, leading to the need of maintaining the index with more number of related web pages; using the relative measure of relevancy between the documents. This paper provides a novel technique for extracting the back-links of a web page and to evaluate their context score; that helps to update the document index with more number of relevant documents.

Keywords

Context Score, Back-Link, Relevant Pages, Common Keywords, WWW.

Full Text