Hussak_Multi-step_transactions_specification.pdf (238.12 kB)
Multi-step transactions specification and verification in a mobile database community
conference contribution
posted on 2009-02-04, 12:35 authored by Rafat Alshorman, Walter HussakWalter HussakExecutions of concurrent multi-step transactions
interleave steps in ways that improve the throughput of the
particular transactions processing system. In this paper, we use
temporal logic to specify and verify formally the correctness of
local and mobile transactions executing concurrently on a mobile
database. The correctness condition is that of serializability which
we specify in CTL (Computational Tree Logic). The reason
for using a temporal logic such as CTL, is that the method
can be extended to verifying infinite schedules modelling mobile
environments such as MDBCs (mobile database communities).
The verification is carried out using the symbolic model checking
NuSMV. We verify that a local scheduler based on timestamps
serializes local and mobile multi-step transactions.
History
School
- Science
Department
- Computer Science
Citation
HUSSAK, R. and HUSSAK, W., 2008. Multi-step transactions specification and verification in a mobile database community. IN: Proceedings, IEEE 3rd International Conference on Information and Communication Technologies: From Theory to Applications, ICTTA 2008, 7-11 April 2008, pp. 1 - 6Publisher
© IEEEVersion
- VoR (Version of Record)
Publication date
2008Notes
This is a conference paper [© IEEE]. It is also available from: http://ieeexplore.ieee.org. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.ISBN
9781424417513Language
- en