Formal verification of SyncML protocol for ubiquitous data coherence

Abstract

In this paper, we have verified and specified synchronization protocol (SyncML). In wireless network environment and cloud system, SyncML protocol to maintain data consistency. Previous studies for protocol verification has demonstrated very limited area that selective utilizing of theorem proving or model checking approach. Thus, consistent with weak synchronization protocol was not discussed. In this study, a mixture of proof and model checking through the synchronization protocol verification method was tested for the entire area. To this end, we has formal specified finite state model for behavior and structure of the protocol. In addition, on the stability and finality of the synchronization protocol properties was defined as temporal logic and higher-order logic. On the other hand, data consistency and mutual exclusion property was proved through a sequential computation. In the process of model checking technology was used as a rule of inference. This study has two features and significance. © 2013 Springer Science+Business Media.