loading...
A Formal Specification of the Concurrency Control in Real-Time Databases
Takamatsu, Japan December 07-December 10
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.1999.809589Sixth Asia-Pacific Software Engineeri ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Ekaterina Pavlova, Dang Van Hung, "A Formal Specification of the Concurrency Control in Real-Time Databases," Asia-Pacific Software Engineering Conference, pp. 94, Sixth Asia-Pacific Software Engineering Conference (APSEC'99), 1999.
 
 
BibTex
x
 
@article{ 10.1109/APSEC.1999.809589,
author = {Ekaterina Pavlova and Dang Van Hung},
title = {A Formal Specification of the Concurrency Control in Real-Time Databases},
journal ={Asia-Pacific Software Engineering Conference},
volume = {0},
year = {1999},
issn = {1530-1362},
pages = {94},
doi = {http://doi.ieeecomputersociety.org/10.1109/APSEC.1999.809589},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Asia-Pacific Software Engineering Conference
TI - A Formal Specification of the Concurrency Control in Real-Time Databases
SN - 1530-1362
SP
EP
A1 - Ekaterina Pavlova,
A1 - Dang Van Hung,
PY - 1999
VL - 0
JA - Asia-Pacific Software Engineering Conference
ER -
 
Ekaterina Pavlova, St.-Petersburg State University
Dang Van Hung, UNU/IIST
In the paper we present a formal model of real-time database (RTDB) systems using Duration Calculus (DC). First, we give a formal specification of the correctness for the executions of transaction systems and the Two Phase Locking Concurrency Control Protocol (2PL-CCP). We also give a formal proof for the correctness of the 2PL-CCP using the DC proof system. Then, we present a formal description of the real-time database model by extending the model for untimed databases with state variables expressing temporal objects and with DC formulas to express their behavior. A formal description of correctness of the parallel executions of transaction systems in RTDBs is then given as the combination of the correctness for the untimed case and the time constraints for the transactions and their read data.
Citation:
Ekaterina Pavlova, Dang Van Hung, "A Formal Specification of the Concurrency Control in Real-Time Databases," apsec, pp.94, Sixth Asia-Pacific Software Engineering Conference (APSEC'99), 1999
Usage of this product signifies your acceptance of the Terms of Use.