Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2007: Formal Methods and Software Engineering pp 232–245Cite as

Model Checking in Practice: Analysis of Generic Bootloader Using SPIN

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4789))

Abstract

This work presents a case study of the use of model checking for analyzing an industrial software, the Generic Bootloader. Analysis of the software have been carried out using the automated verification system SPIN. A model of the software has been developed using the specification language PROMELA, and the properties expressed in the LTL have been verified against the model. We propose a new modeling technique that helps to model communication protocols efficiently. Formal analysis has also helped us to reveal a flaw in the implementation of the software which otherwise remain undetected through testing process.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. SPIN Model Checker. http://www.spinroot.com/

  2. de Renesse, R., Aghvami, A.H.: Formal verification of ad-hoc routing protocols using spin model checker. In: IEEE MELECON, IEEE Computer Society Press, Los Alamitos (2004)

    Google Scholar 

  3. Jensen, H., Larsen, K., Skou, A.: Modelling and analysis of a collision avoidance protocol using spin and uppaal. In: The Second Workshop on the SPIN Verification System, American Mathematical Society. Discrete Mathematics and Theoretical Computer Science, vol. 32 (1996)

    Google Scholar 

  4. Pike, L.: Formal verification of time triggered systems. PhD thesis, Indiana University (2005)

    Google Scholar 

  5. van Osch, M.J.P., Smolka, S.A.: Finite-state analysis of the can bus protocol. In: HASE 2001, p. 42. IEEE Computer Society, Washington, DC, USA (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Honeywell Technology Solutions Lab (HTSL), 151/1, Doraisanipalya, Bannerghatta Road, Bangalore 560 076, India

    Kuntal Das Barman

  2. TOR ANUMANA Technologies Pvt Ltd, 12, Lee Road, Kolkata 700020, India

    Debapriyay Mukhopadhyay

Authors
  1. Kuntal Das Barman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Debapriyay Mukhopadhyay
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael Butler Michael G. Hinchey María M. Larrondo-Petrie

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Das Barman, K., Mukhopadhyay, D. (2007). Model Checking in Practice: Analysis of Generic Bootloader Using SPIN. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds) Formal Methods and Software Engineering. ICFEM 2007. Lecture Notes in Computer Science, vol 4789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76650-6_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-76650-6_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-76648-3

  • Online ISBN: 978-3-540-76650-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation