文章基本信息

标题：Formal Verification of Distributed Checkpointing Using Event-B
本地全文：下载
作者：Girish Chandra ; Raghuraj Suryavanshi ; Divakar Yadav 等
期刊名称：International Journal of Computer Science & Information Technology (IJCSIT)
印刷版ISSN：0975-4660
电子版ISSN：0975-3826
出版年度：2015
卷号：7
期号：5
页码：59
出版社：Academy & Industry Research Collaboration Center (AIRCC)
摘要：The development of complex system makes challenging task for correct software development. Due to faultyspecification, software may involve errors. The traditional testing methods are not sufficient to verify thecorrectness of such complex system. In order to capture correct system requirements and rigorousreasoning about the problems, formal methods are required. Formal methods are mathematical techniquesthat 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 databasesystems. In a distributed database system, the database is stored at different sites that are connectedtogether through the network. Checkpoint is a recovery point which contains the state information aboutthe site. In order to do recovery of a distributed transaction a global checkpoint number (GCPN) isrequired. A global checkpoint number decides which transaction will be included for recovery purpose. Alltransactions whose timestamp are less than global checkpoint number will be marked as before checkpointtransaction (BCPT) and will be considered for recovery purpose. The transactions whose timestamp aregreater than GCPN will be marked as after checkpoint transaction (ACPT) and will be part of next globalcheckpoint number.
关键词：Formal Methods; Formal Specifications; Formal Verification; Event-B; Distributed Transaction; Checkpointing;Local checkpoint number; Global checkpoint number.