A formal specification of the concurrency control in real-time databases

Author

Pavlova, Ekaterina ; Van Hung, Dang

Author_Institution

St. Petersburg State Univ., Russia

fYear

1999

fDate

1999

Firstpage

94

Lastpage

101

Abstract

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 behaviour. 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

Keywords

concurrency control; formal specification; process algebra; real-time systems; theorem proving; transaction processing; 2PL-CCP; DC formulas; DC proof system; Duration Calculus; RTDB; Two Phase Locking Concurrency Control Protocol; concurrency control; formal description; formal model; formal proof; formal specification; parallel executions; read data; real time database model; real time databases; state variables; temporal objects; time constraints; transaction systems; untimed case; untimed databases; Calculus; Concurrency control; Database systems; Design methodology; Formal specifications; Logic; Protocols; Real time systems; Time factors; Transaction databases;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Conference, 1999. (APSEC '99) Proceedings. Sixth Asia Pacific

Conference_Location

Takamatsu

Print_ISBN

0-7695-0509-0

Type

conf

DOI

10.1109/APSEC.1999.809589

Filename

809589