Mechanical verification of concurrency control and recovery protocols
type: Item
instance of: scholarly article
zbMATH Open document ID: 0989.68089
author: Dmitri A. Chkliaev
publication date: 2001-12-13T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68M14
Mathematics Subject Classification ID: 68-02
zbMATH DE Number: 1682376
zbMATH Keywords: recovery protocols
zbMATH Keywords: distributed data processing systems
describes a project that uses: PVS
MaRDI profile type: Publication
title: Mechanical verification of concurrency control and recovery protocols
review text: This PhD Thesis is concerned with the formal verification of ConCurrency and Recovery Protocols (CCRP) in distributed data processing systems, using theorem proving.NEWLINENEWLINENEWLINEChapter 1 gives an overview of the thesis. It introduces the context of distributed data processing systems, which are distributed systems that manage data by transactions, such as banking systems or airline reservation systems. It explains the aim of concurrency and recovery protocols which try to avoid potential errors arising from concurrency and failures. The author gives a state of the art on the verification of the correctness of CCRPs and advocates the use of proof techniques.NEWLINENEWLINENEWLINEChapter 2 details the requirements of data processing systems such as atomicity, durability and serializability. It describes some basic techniques used to ensure these requirements in three classical protocols: Two phase locking, strict two phase locking and timestamp ordering.NEWLINENEWLINENEWLINEChapter 3 describes the main correctness properties (view and conflict serializability) in higher-order logic, their representation in PVS, the theorem prover of SRI (Stanford Research Institute), and the results of their proof by PVS on specifications of the above-mentioned protocols.NEWLINENEWLINENEWLINEIn Chapter 4, other properties (atomicity, durability and conflict serializability) are formalized in a wider context and checked by PVS on an experimental protocol.NEWLINENEWLINENEWLINEChapter 5 is dedicated to the verification of a combination of the non-blocking commitment protocol of Babaoglu and Toueg with a termination protocol.NEWLINENEWLINENEWLINEChapter 6 concludes by some feedback on the use of PVS on such problems and gives some directions for future work.
reviewed by: Thierry Jéron
description: scientific article; zbMATH DE number 1682376