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.