Formal Development of a Distributed Logging Mechanism Supporting Disconnected Updates

Y. Qian

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


    In mobile computing environments, logging systems are often used to record updates during device disconnection and logs are used in data synchronization on reconnection. Portable devices often have resource constraints and log truncation must be used to avoid log overflow. However, this method makes data synchronization vulnerable, due to information loss in truncating log files. Characteristic-entry logs record merely the most recent data access of each operation type per data item. They capture the minimum information needed to semantically resolve conflicting updates. They have been implemented in the MemorySafe system of Philips, a prototype distributed system supporting disconnected updates. In this paper, we present a formal model of characteristic-entry logs and investigate the relation between normal logs and characteristic-entry logs. We rigorously prove that characteristic-entry logs can be used in data synchronization, effectively in the same way as normal logs.
    Original languageEnglish
    Title of host publicationFormal methods and software engineering : 5th International Conference on Formal Engineering Methods, ISFEM 2003, Singapore, November 5-7, 2003 : proceedings
    EditorsJ.S. Dong, Jim Woodcock
    Place of PublicationBerlin
    ISBN (Print)3-540-20461-X
    Publication statusPublished - 2003

    Publication series

    NameLecture notes in computer science


    Dive into the research topics of 'Formal Development of a Distributed Logging Mechanism Supporting Disconnected Updates'. Together they form a unique fingerprint.

    Cite this