scholarly journals Assertional Reasoning for Concurrent and Communicating BPEL-like Programs

2018 ◽  
Author(s):  
Longfei Zhu ◽  
Qiwen Xu ◽  
Huibiao Zhu
Keyword(s):  
Assertional Reasoning

FORMALIZATION AND PROOF OF CORRECTNESS OF THE CRASH RECOVERY ALGORITHM FOR AN OPEN AND SAFE NESTED TRANSACTION MODEL

2001 ◽  
Vol 10 (01n02) ◽  
pp. 1-50 ◽  
Author(s):  
SANJAY KUMAR MADRIA ◽  
S. N. MAHESHWARI ◽  
B. CHANDRA ◽  
BHARAT BHARGAVA
Keyword(s):  
Buffer Management ◽  
Operational Semantics ◽  
Proof Technique ◽  
Recovery Algorithm ◽  
Nested Transactions ◽  
Transaction Model ◽  
Proof Of Correctness ◽  
Assertional Reasoning ◽  
Crash Recovery

In this paper, we present, formalize and prove the correctness of recovery algorithm for our open and safe nested transaction model using I/O automaton model. Our nested transaction model uses the notion of a recovery point subtransaction in the nested transaction tree. It introduces a prewrite operation before each write operation to increase the potential concurrency. Our transaction model is termed as "open and safe" as prewrites allow early reads (before database writes on disk) without cascading aborts. The systems restart and buffer management operations are modelled as nested transactions to exploit possible concurrency during restart. Each non-access transaction, object, and the scheduler is modeled as I/O automaton. Each of these automata is specified with the help of some pre-and post-conditions. These pre-and post-conditions capture the operational semantics and the behavior of each automaton during recovery operations. Our proof technique makes use of assertional reasoning and provide many interesting invariant, thus gives a better understanding of our recovery algorithm.

Sign in / Sign up

Export Citation Format

Share Document