Loughborough University
Browse
Hussak_Multi-step_transactions_specification.pdf (238.12 kB)

Multi-step transactions specification and verification in a mobile database community

Download (238.12 kB)
conference contribution
posted on 2009-02-04, 12:35 authored by Rafat Alshorman, Walter HussakWalter Hussak
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.

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 - 6

Publisher

© IEEE

Version

  • VoR (Version of Record)

Publication date

2008

Notes

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

9781424417513

Language

  • en

Usage metrics

    Loughborough Publications

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC