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.
|Title of host publication||Formal methods and software engineering : 5th International Conference on Formal Engineering Methods, ISFEM 2003, Singapore, November 5-7, 2003 : proceedings|
|Editors||J.S. Dong, Jim Woodcock|
|Place of Publication||Berlin|
|Publication status||Published - 2003|
|Name||Lecture notes in computer science|