Skip to main content
SpringerLink
Log in

Verification and Analysis for Ethernet Protocols with NuSMV

  • Conference paper
  • First Online:
Computer, Informatics, Cybernetics and Applications

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

  • 798 Accesses

Abstract

Verifying the correctness of computer systems is becoming necessary for most of systems, especially safety–critical systems. Symbolic model checking is one of the effective ways to do automatic model checking. In this chapter, we verified some properties of Ethernet protocols, especially CSMA/CD protocol, using NuSMV tool. NuSMV is proved to be a suitable tool for its input a transition based model of processes by communicating to each other through shared and global variables. The methods we proposed to analyze Ethernet protocols, such as synchronization modeling and time delay modeling, can also be extended to analyze similar related networking protocols and their properties.

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 429.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 549.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 549.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. Huth M, Ryan M (2000) Logic in computer science, Cambridge University Press, London

    Google Scholar 

  2. NuSMV project (2011) http://nusmv.fbk.eu/index.html

  3. Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without bdds. In: Proceedings of 5th international conference on tools and algorithms for construction and analysis of systems (TACAS’99), pp. 193–207

    Google Scholar 

  4. Zhao Y, Yang Z, Xie J, Liu Q (2009) Formal model and analysis of sliding window protocol based on NuSMV. J Comput 4(6):519–526

    Google Scholar 

  5. Marrero W, Clarke E, Jha S (1997) Model checking for security protocols. Carnegie Mellon University technical report CM U-SCS 97–139

    Google Scholar 

  6. Tanenbaum A (1996) Computer netowrks 3rd edn. Prentice Hall, New Jersey

    Google Scholar 

  7. Weinberg H, Zuck L (1992) Timed ethernet: real-time formal specification of ethernet. In: Proceding of the. 3rd CONCUR, Lect Notes Comput Sci vol 630

    Google Scholar 

Download references

Acknowledgments

The work was partially supported by the Natural Science Foundation of Zhejiang under Grant No. Y1100824 and Zhejiang Public Interest Project of Technology Bureau under Grand No. 2010C31088.

Author information

Authors and Affiliations

  1. College of Computer and Information Engineering, Zhejiang Gongshang University, No.18 Xuezheng Str., Hangzhou, China

    Yujia Ge & Xiaofei Feng

  2. Department of Computer Science, Iowa State University, Ames, IA, USA

    Fangcheng Tang

Authors
  1. Yujia Ge
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Xiaofei Feng
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fangcheng Tang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yujia Ge .

Editor information

Editors and Affiliations

  1. Chinese Academy of Engineering, Beijing, China, People's Republic

    Xingui He

  2. Zhejiang Gongshang University, Beijing, China, People's Republic

    Ertian Hua

  3. Zhejiang Gongshang University, Hangzhou, China, People's Republic

    Yun Lin

  4. , School of Automation, Wuhan University of Technology, East District of Wuhan University, Luoshi Road 122, Wuhan, 4300, China, People's Republic

    Xiaozhu Liu

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer Science+Business Media B.V.

About this paper

Cite this paper

Ge, Y., Feng, X., Tang, F. (2012). Verification and Analysis for Ethernet Protocols with NuSMV. In: He, X., Hua, E., Lin, Y., Liu, X. (eds) Computer, Informatics, Cybernetics and Applications. Lecture Notes in Electrical Engineering, vol 107. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-1839-5_33

Download citation

  • DOI: https://doi.org/10.1007/978-94-007-1839-5_33

  • Published:

  • Publisher Name: Springer, Dordrecht

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

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

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation