{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:02:52Z","timestamp":1742389372775},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642104510"},{"type":"electronic","value":"9783642104527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10452-7_11","type":"book-chapter","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T03:37:26Z","timestamp":1257305846000},"page":"153-169","source":"Crossref","is-referenced-by-count":7,"title":["An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model"],"prefix":"10.1007","author":[{"given":"Miguel Alexandre","family":"Ferreira","sequence":"first","affiliation":[]},{"given":"Jos\u00e9 Nuno","family":"Oliveira","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Escher Technologies - Products, http:\/\/www.eschertech.com\/products"},{"key":"11_CR2","unstructured":"Spin - Formal Verification, http:\/\/spinroot.com"},{"key":"11_CR3","series-title":"Series in Computer Science","volume-title":"Algebra of Programming","author":"R. Bird","year":"1997","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1997), C.A.R. Hoare, series editor"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08766-4","volume-title":"The Vienna Development Method: The Meta-Language","author":"D. Bj\u00f8rner","year":"1978","unstructured":"Bj\u00f8rner, D., Jones, C.B.: The Vienna Development Method: The Meta-Language. LNCS, vol.\u00a061. Springer, Heidelberg (1978)"},{"key":"11_CR5","first-page":"23","volume-title":"WORDS","author":"J. Coleman","year":"2005","unstructured":"Coleman, J., Jones, C., Oliver, I., Romanovsky, A., Troubitsyna, E.: RODIN (Rigorous open Development Environment for Complex Systems). In: WORDS, pp. 23\u201326. IEEE Computer Society, Los Alamitos (2005)"},{"key":"11_CR6","unstructured":"Intel Corporation. Intel $^{\\textrm{\\textregistered}}$ Flash File System Core Reference Guide. Technical report 304436-001, Intel Corporation (2004)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-88194-0_5","volume-title":"Formal Methods and Software Engineering","author":"K. Damchoom","year":"2008","unstructured":"Damchoom, K., Butler, M., Abrial, J.: 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.\u00a05256, pp. 25\u201344. Springer, Heidelberg (2008)"},{"key":"11_CR8","unstructured":"Ferreira, M.: Verifying Intel $^{\\textrm{\\textregistered}}$ Flash File System Core. Master\u2019s thesis, Minho University (January 2009)"},{"key":"11_CR9","unstructured":"Ferreira, M., Silva, S., Oliveira, J.N.: Verifying Intel Flash File System Core Specification. In: Fourth VDM\/Overture Workshop (CS-TR-1099) (May 2008)"},{"key":"11_CR10","unstructured":"Ferreira, M.A.: Implementing the Overture Automatic Proof System (submitted for publication, 2009)"},{"key":"11_CR11","unstructured":"Ferreira, M.A., Oliveira, J.N.: Verifying the (generic) flash memory implementation of abstract mappings (in preparation, 2009)"},{"key":"11_CR12","volume-title":"Modelling Systems: Practical Tools and Techniques in Software Development","author":"J. Fitzgerald","year":"1998","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, Cambridge (1998)"},{"key":"11_CR13","volume-title":"Validated Designs for Object-oriented Systems","author":"J. Fitzgerald","year":"2005","unstructured":"Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-oriented Systems. Springer, New York (2005)"},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1361213.1361214","volume":"43","author":"J. Fitzgerald","year":"2008","unstructured":"Fitzgerald, J., Larsen, P.G., Sahara, S.: VDMTools: advances in support for formal modeling in VDM. SIGPLAN Notices\u00a043(2), 3\u201311 (2008)","journal-title":"SIGPLAN Notices"},{"key":"11_CR15","first-page":"3","volume-title":"ICECCS 2007","author":"L. Freitas","year":"2007","unstructured":"Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z\/Eves: an experiment in the verified software repository. In: ICECCS 2007, Washington, DC, USA, pp. 3\u201314. IEEE Computer Society, Los Alamitos (2007)"},{"key":"11_CR16","series-title":"Math. Lib.","volume-title":"Categories, Allegories","author":"P.J. Freyd","year":"1990","unstructured":"Freyd, P.J., \u0160\u010dedrov, A.: Categories, Allegories. Math. Lib., vol.\u00a039. North-Holland, Amsterdam (1990)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-93900-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Galloway","year":"2009","unstructured":"Galloway, A., L\u00fcttgen, G., M\u00fchlberg, J.T., Siminiceanu, R.: Model-checking the linux virtual file system. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 74\u201388. Springer, Heidelberg (2009)"},{"key":"11_CR18","first-page":"169","volume-title":"From LCF to HOL: a short history","author":"M. Gordon","year":"2000","unstructured":"Gordon, M.: From LCF to HOL: a short history, pp. 169\u2013185. MIT Press, Cambridge (2000)"},{"key":"11_CR19","unstructured":"The VDM\u00a0Tool Group. The VDM++ to Java Code Generator. Technical report, CSK Systems (January 2008)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Hesselink, W.H., Lali, M.I.: Formalizing an Hierarchical File System. Submitted to FM 2009 (2009)","DOI":"10.1016\/j.entcs.2009.12.018"},{"issue":"1","key":"11_CR21","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. J. ACM\u00a050(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69149-5_1","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T. Hoare","year":"2008","unstructured":"Hoare, T., Misra, J.: Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 1\u201318. Springer, Heidelberg (2008)"},{"key":"11_CR23","unstructured":"IEEE and The\u00a0Open Group. Standard for information technology - POSIX $^{\\textrm{\\textregistered}}$ . Base Definitions, Issue 6. IEEE Std 1003.1-2001. The Open Group Tech. Std. (2004)"},{"key":"11_CR24","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"11_CR25","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall International, Englewood Cliffs (1990)","edition":"2"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-69149-5_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"R. Joshi","year":"2008","unstructured":"Joshi, R., Holzmann, G.J.: A Mini Challenge: Build a Verifiable File system. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 49\u201356. Springer, Heidelberg (2008)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-87603-8_23","volume-title":"Abstract State Machines, B and Z","author":"E. Kang","year":"2008","unstructured":"Kang, E., Jackson, D.: Formal Modeling and Analysis of a Flash Filesystem in Alloy. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 294\u2013308. Springer, Heidelberg (2008)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Larsen, P.G., Batle, N., Fitzgerald, J., Lausdahl, K., Ferreira, M., Verhoef, M.: The Overture Initiative Integrating all VDM tools (in preparation, 2009)","DOI":"10.1145\/1668862.1668864"},{"issue":"3","key":"11_CR29","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s00165-008-0068-5","volume":"21","author":"P.G. Larsen","year":"2009","unstructured":"Larsen, P.G., Fitzgerald, J.S., Riddle, S.: Practice-oriented courses in formal methods using VDM++. Formal Asp. Comput.\u00a021(3), 245\u2013257 (2009)","journal-title":"Formal Asp. Comput."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Larsen, P.G., Lausdahl, K., Batle, N.: Combinatorial Testing for VDM++. Submitted for publication (2009)","DOI":"10.1109\/SEFM.2010.32"},{"key":"11_CR31","unstructured":"Leberre, D., Delorme, F.: An eclipse plugin for the alloy4 tool, http:\/\/code.google.com\/p\/alloy4eclipse\/"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-88643-3_4","volume-title":"GTTSE 2007","author":"J.N. Oliveira","year":"2008","unstructured":"Oliveira, J.N.: Transforming Data by Calculation. In: L\u00e4mmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2007. LNCS, vol.\u00a05235, pp. 134\u2013195. Springer, Heidelberg (2008)"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-642-03153-3_5","volume-title":"LerNet ALFA Summer School 2008","author":"J.N. Oliveira","year":"2009","unstructured":"Oliveira, J.N.: Extended Static Checking by Calculation using the Pointfree Transform. In: Bove, A., et al. (eds.) LerNet ALFA Summer School 2008. LNCS, vol.\u00a05520, pp. 195\u2013251. Springer, Heidelberg (2009)"},{"issue":"8","key":"11_CR34","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/142137.142153","volume":"27","author":"N. Plat","year":"1992","unstructured":"Plat, N., Larsen, P.G.: An overview of the ISO\/VDM-SL standard. SIGPLAN Notices\u00a027(8), 76\u201382 (1992)","journal-title":"SIGPLAN Notices"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Schierl, A., Schellhorn, G., Haneberg, D., Reif, W.: Abstract Specification of the UBIFS File System for Flash Memory. Submitted to FM 2009 (2009)","DOI":"10.1007\/978-3-642-05089-3_13"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A Brief Overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"11_CR37","series-title":"American Math. Soc.","volume-title":"A Formalization of Set Theory without Variables","author":"A. Tarski","year":"1987","unstructured":"Tarski, A., Givant, S.: A Formalization of Set Theory without Variables. American Math. Soc., vol.\u00a041. AMS Colloq. Pub., Providence (1987)"},{"key":"11_CR38","unstructured":"Vermolen, S.: Automatically Discharging VDM Proof Obligations using HOL. Master\u2019s thesis, Radboud University, Computer Science Department (2007)"},{"key":"11_CR39","unstructured":"Weiser, M.: Program slicing. In: 5th Int. Conf. on Software Eng., San Diego, California (March 1981)"},{"issue":"4","key":"11_CR40","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1145\/1189256.1189259","volume":"24","author":"J. Yang","year":"2006","unstructured":"Yang, J., Twohey, P., Engler, D.R., Musuvathi, M.: Using model checking to find serious file system errors. ACM Trans. Comput. Syst.\u00a024(4), 393\u2013423 (2006)","journal-title":"ACM Trans. Comput. Syst."}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10452-7_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:56:05Z","timestamp":1606168565000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10452-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642104510","9783642104527"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10452-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}