Skip to main content
SpringerLink
Log in
Book cover

Brazilian Symposium on Formal Methods

SBMF 2009: Formal Methods: Foundations and Applications pp 134–152Cite as

Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B

  • Conference paper

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

Abstract

Event-B is a formal method used for specifying and reasoning about systems. Rodin is a toolset for developing system models in Event-B. Our experiment which is outlined in this paper is aimed at applying Event-B and Rodin to a flash-based filestore. Refinement is a useful mechanism that allows developers to sharpen models step by step. Two uses of refinement, feature augmentation and structural refinement, were employed in our development. Event decomposition and machine decomposition are structural refinement techniques on which we focus in this work. We present an outline of a verified refinement chain for the flash filestore. We also outline evidence of the applicability of the method and tool together with some guidelines.

This work was part of the EU research project ICT 214158 DEPLOY (Industrial deployment of system engineering methods providing high dependability and productivity) www.deploy-project.eu.

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. Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996)

    MATH  Google Scholar 

  2. Abrial, J.-R.: A system development process with Event-B and the Rodin platform. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 1–3. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Abrial, J.-R.: Modelling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2009) (to be published)

    Google Scholar 

  4. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Abrial, J.-R., Hallerstede, S.: Refinement, decomposition and instantiation of discrete models: Application to Event-B. Fundamentae Infomatica, 1001–1026 (2006)

    Google Scholar 

  6. Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Butler, M., Yadav, D.: An Incremental development of the Mondex system in Event-B. Formal Aspects of Computing 20(1), 61–77 (2008)

    Article  Google Scholar 

  8. Butler, M., Abrial, J.-R., Damchoom, K., Edmunds, A.: Applying Event-B and Rodin to the filestore. VSRNet, ABZ 2008 (2008)

    Google Scholar 

  9. Butler, M.: Rodin deliverable D31: Public versions of plug-in tools. Technical report, University of Southampton, UK (2007)

    Google Scholar 

  10. Butterfield, A., Freitas, L., Woodcock, J.: Mechanising a formal model of flash memory. Science of Computer Programming 74(4), 219–237 (2009)

    Article  MATH  Google Scholar 

  11. Damchoom, K., Butler, M., Abrial, J.-R.: Modelling and proof of a tree-structured file system in Event-B and Rodin. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 25–44. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Ferreira, M.A., Silva, S.S., Oliveira, J.N.: Verifying Intel Flash File System Core Specification. Technical report, University of Minho (2008)

    Google Scholar 

  13. Freitas, L., Woodcock, J., Fu, Z.: POSIX file store in Z/Eves: An experiment in the verified software repository. Science of Computer Programming 74(4), 238–257 (2009)

    Article  MATH  Google Scholar 

  14. Hoare, T., Misra, J.: Verified software: theories, tools, experiments; Vision of a Grand Challenge project (2005)

    Google Scholar 

  15. Hughes, J.: Specifying a visual file system in Z. Technical report, Department of Computing Science, University of Glasgow (1989)

    Google Scholar 

  16. Cemicondutor, H., et al.: Open NAND Flash Interface Specification, Revision 2.0. Technical report, ONFI (February 2008), http://www.onfi.org

  17. Intel Flash File System Core Reference Guide, version 1. Technical report 304436001, Intel Coorporation (October 2004)

    Google Scholar 

  18. Jackson, M.A.: System Development. Prentice Hall, Englewood Cliffs (1983)

    MATH  Google Scholar 

  19. Joshi, R., Holzmann, G.J.: A mini challenge: Build a verifiable filesystem. In: Verified Software: Theories, Tools, Experiments (2005)

    Google Scholar 

  20. Kang, E., Jackson, D.: Formal modeling and analysis of a flash filesystem in Alloy. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 294–308. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Morgan, C., Sufrin, B.: Specification of the Unix filing system. IEEE Transaction on Software Engineering 10, 128–142 (1984)

    Article  Google Scholar 

  22. Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Southampton, United Kingdom

    Kriangsak Damchoom & Michael Butler

Authors
  1. Kriangsak Damchoom
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Butler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Informática e Matemática Aplicada, Universidade Federal do Rio Grande do Norte, Campus Universitário, CEP: 59078-900, Lagoa Nova Natal, RN, Brasil

    Marcel Vinícius Medeiros Oliveira

  2. Department of Computer Science, University of York, Heslington, YO1 7BZ, York, UK

    Jim Woodcock

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Damchoom, K., Butler, M. (2009). Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. In: Oliveira, M.V.M., Woodcock, J. (eds) Formal Methods: Foundations and Applications. SBMF 2009. Lecture Notes in Computer Science, vol 5902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10452-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-10452-7_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-10451-0

  • Online ISBN: 978-3-642-10452-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation