Skip to main content
SpringerLink
Log in

Formal Verification of SyncML Protocol for Ubiquitous Data Coherence

  • Conference paper
  • First Online:
Ubiquitous Information Technologies and Applications

Part of the book series: Lecture Notes in Electrical Engineering ((LNEE,volume 214))

  • 2158 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. http://www.syncml.org

  2. Kahn, P.: SyncML: Synchronizing and managing your mobile data, PH PTR (2003)

    Google Scholar 

  3. Fournet, C.: Modular code based cryptographic verification, ACM CCCS (2011)

    Google Scholar 

  4. Meng, B.: Automatic verification of deniable authentication protocol in a probabilistic polynomial calculus, Asian Network for Scientific Information (2011)

    Google Scholar 

  5. Sorin, D.J., et al.: Specifying and verifying a broadcast and a multicast snooping cache coherence protocol, vol. 13, no. 6 (2002)

    Google Scholar 

  6. Berezin, S.: Model Checking and Theorem Proving: a Unified Framework, Ph.D. Thesis, Carnegie Mellon University (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Knowledge and Information Division, Korea Institute of Science and Technology Evaluation and Planning, 11F dongwon Industry Bldg, 68 Mabang-gil Seocho-gu, Seoul, South Korea

    Seungsu Chun, Seungryong Lee & Donghoon Oh

Authors
  1. Seungsu Chun
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Seungryong Lee
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Donghoon Oh
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Seungsu Chun .

Editor information

Editors and Affiliations

  1. and Education, Computer Science and Engineering, Korea University of Technology, Chungjeolno, Byeongchun 1600, CheonAn, 330-861, Korea, Republic of (South Korea)

    Youn-Hee Han

  2. , Division of Computer Science and Enginee, SoonChunHyang University, Sinchang, Chungnam, 336-745, Korea, Republic of (South Korea)

    Doo-Soon Park

  3. , Dept of Computer Science, City University of Hong Kong, Tat Chee Avenue, Kowloon, 83, Hong Kong SAR

    Weijia Jia

  4. , Division of Computer Engineering, Mokwon University, Do-An-Buk-Ro 88, Daejeon, 302-729, Korea, Republic of (South Korea)

    Sang-Soo Yeo

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer Science+Business Media Dordrecht

About this paper

Cite this paper

Chun, S., Lee, S., Oh, D. (2013). Formal Verification of SyncML Protocol for Ubiquitous Data Coherence. In: Han, YH., Park, DS., Jia, W., Yeo, SS. (eds) Ubiquitous Information Technologies and Applications. Lecture Notes in Electrical Engineering, vol 214. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-5857-5_45

Download citation

  • DOI: https://doi.org/10.1007/978-94-007-5857-5_45

  • Published:

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-94-007-5856-8

  • Online ISBN: 978-94-007-5857-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation