{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T16:00:17Z","timestamp":1759939217333},"publisher-location":"Berlin, Heidelberg","reference-count":18,"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_8","type":"book-chapter","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T08:37:26Z","timestamp":1257323846000},"page":"101-117","source":"Crossref","is-referenced-by-count":15,"title":["Formalizing FreeRTOS: First Steps"],"prefix":"10.1007","author":[{"given":"David","family":"D\u00e9harbe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephenson","family":"Galv\u00e3o","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anamaria Martins","family":"Moreira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"SBC: Grandes Desafios da Pesquisa em Computa\u00e7\u00e3o no Brasil: 2006\u20132016 (2006), http:\/\/www.sbc.org.br"},{"issue":"4","key":"8_CR2","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C. Jones","year":"2006","unstructured":"Jones, C., O\u2019Hearn, P., Woodcock, J.: Verified software: a grand challenge. Computer\u00a039(4), 93\u201395 (2006)","journal-title":"Computer"},{"key":"8_CR3","unstructured":"Woodcock, J.: Grand challenge in software verification. In: Brazilian Symposium on Formal Methods, SBMF 2008 (2008)"},{"key":"8_CR4","volume-title":"Formal Models of Operating System Kernels","author":"I.D. Craig","year":"2007","unstructured":"Craig, I.D.: Formal Models of Operating System Kernels. Springer, Heidelberg (2007)"},{"key":"8_CR5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"8_CR6","volume-title":"The B-Method: An Introduction","author":"S. Schneider","year":"2001","unstructured":"Schneider, S.: The B-Method: An Introduction. Palgrave, Oxford (2001)"},{"key":"8_CR7","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"8_CR8","series-title":"Prentice-Hall International Series in Computer Science","volume-title":"The Z Notation: a Reference Manual","author":"J. Spivey","year":"1992","unstructured":"Spivey, J.: The Z Notation: a Reference Manual, 2nd edn. Prentice-Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs (1992)","edition":"2"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-540-87603-8_33","volume-title":"Abstract State Machines, B and Z","author":"A. Requet","year":"2008","unstructured":"Requet, A.: Bart: A tool for automatic refinement. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 345\u2013345. Springer, Heidelberg (2008)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Faultless system: Yes we can! Technical Report 629, Department of Computer Science, ETH Zurich (2009)","DOI":"10.1109\/MC.2009.283"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Jaffuel, E., Legeard, B.: LEIRIOS test generator: Automated test generation from B models. In: The 7th International B Conference, pp. 277\u2013280 (2007)","DOI":"10.1007\/11955757_29"},{"key":"8_CR12","unstructured":"Clearsy: Atelier B 4.0 (2009), http:\/\/www.atelierb.eu"},{"issue":"2","key":"8_CR13","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s00165-005-0079-4","volume":"18","author":"J. Bicarregui","year":"2006","unstructured":"Bicarregui, J., Hoare, C., Woodcock, J.: The verified software repository: a step towards the verifying compiler. Formal Aspects of Computing\u00a018(2), 143\u2013151 (2006)","journal-title":"Formal Aspects of Computing"},{"key":"8_CR14","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language (2008)"},{"key":"8_CR15","first-page":"429","volume-title":"ICSE Companion","author":"M. Dahlweid","year":"2009","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: Vcc: Contract-based modular verification of concurrent c. In: ICSE Companion, pp. 429\u2013430. IEEE, Los Alamitos (2009)"},{"key":"8_CR16","unstructured":"CEA: Frama-c: Software analyzers (2009), http:\/\/frama-c.cea.fr"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Andrade, W.L., Alves, E.L.G., Almeida, D.R., Machado, P.D.L.: Test case generation of embedded real-time systems with interruptions for FreeRTOS. In: Brazilian Symposium on Formal Methods, SBMF 2009 (2009)","DOI":"10.1007\/978-3-642-10452-7_5"}],"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_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:56:08Z","timestamp":1606186568000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10452-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642104510","9783642104527"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10452-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}