2134/4165
Rafat Alshorman
Rafat
Alshorman
Walter Hussak
Walter
Hussak
Multi-step transactions specification and verification in a mobile database community
Loughborough University
2009
untagged
Information and Computing Sciences not elsewhere classified
2009-02-04 12:35:57
Conference contribution
https://repository.lboro.ac.uk/articles/conference_contribution/Multi-step_transactions_specification_and_verification_in_a_mobile_database_community/9403769
Executions 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.