Mechanical verification of concurrency control and recovery protocols (Q2760869)

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.