Dalam tesis ini dibuktikan secara formal serializability protokol speculative concurrency control yang dibuat oleh Bestavros dan Spyridon, yang mengadopsi keunggulan dari dua jenis protokol sebelumnya, yaitu protokol pesimistic concurrency control (lock-based) dan optimistic conccurency control (restart-based). Kerangka berpikir yang digunakan berawal dari spesifikasi speculative concurrency control, dengan memanfaatkan model basisdata waktu-nyata yang dikembangkan oleh Dang Van Hung dan Ekaterina Pavlova. Setelah itu dilakukan pembuktian serializability speculative concurrency control. Spesifikasi silakukan menggunakan Kalkulus Durasi (Duration Calculus) dan pembuktian dilakukan menggunakan Isabelle / DC.