{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:10:34Z","timestamp":1743023434487,"version":"3.40.3"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031556074"},{"type":"electronic","value":"9783031556081"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-55608-1_14","type":"book-chapter","created":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T07:02:19Z","timestamp":1720508539000},"page":"583-615","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Exploring Frama-C Resources by Verifying Space Software"],"prefix":"10.1007","author":[{"given":"Rovedy Aparecida","family":"Busquim e Silva","sequence":"first","affiliation":[]},{"given":"Nanci Naomi","family":"Arai","sequence":"additional","affiliation":[]},{"given":"Luciana Akemi","family":"Burgareli","sequence":"additional","affiliation":[]},{"given":"Jose Maria","family":"Parente de Oliveira","sequence":"additional","affiliation":[]},{"given":"Jorge","family":"Sousa Pinto","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,10]]},"reference":[{"key":"14_CR1","unstructured":"Ag\u00eancia Espacial Brasileira (2022) Transporte Espacial. https:\/\/www.gov.br\/aeb\/pt-br\/programa-espacial-brasileiro\/transporte-espacial. Accessed 20 Sep 2022"},{"key":"14_CR2","unstructured":"Ag\u00eancia For\u00e7a A\u00e9rea: IAE realiza Opera\u00e7\u00e3o Santa Maria 1\/2021 no Centro de Lan\u00e7amento de Alc\u00e2ntara (CLA) (2021). https:\/\/www.fab.mil.br\/noticias\/mostra\/37556. Accessed 24 Jan 2022"},{"key":"14_CR3","unstructured":"Alberti M, Antignac T, Barany G et al Help of frama-c tool"},{"key":"14_CR4","unstructured":"Alberti M, Antignac T, Barany G et al (2021) FRAMA-C. https:\/\/frama-c.com\/. Accessed 15 Jan 2022"},{"key":"14_CR5","doi-asserted-by":"publisher","DOI":"10.1145\/3470569","author":"P Baudin","year":"2021","unstructured":"Baudin P, Bobot F, B\u00fchler D, Correnson L, Kirchner F, Kosmatov N, Maroneze A, Perrelle V, Prevosto V, Signoles J, Williams N (2021) The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun ACM. https:\/\/doi.org\/10.1145\/3470569","journal-title":"Commun ACM"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Black PE, Walia KS (2020) SATE VI Ockham sound analysis criteria. Tech. rep., national institute of standards and technology\u2014NIST. https:\/\/nvlpubs.nist.gov\/nistpubs\/ir\/2020\/NIST.IR.8304.pdf","DOI":"10.6028\/NIST.IR.8304"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Blanchard A, Kosmatov N, Loulergue F (2018) A lesson on verification of IoT software with Frama-C. In: Conference on high performance computing and simulation (HPCS). https:\/\/doi.org\/10.1109\/HPCS.2018.00018","DOI":"10.1109\/HPCS.2018.00018"},{"key":"14_CR8","unstructured":"Bonichon R, Yakobowski B Frama-C\u2019s metrics plug-in 24.0 (Chromium). https:\/\/www.frama-c.com\/download\/metrics-manual-24.0-Chromium.pdf"},{"key":"14_CR9","unstructured":"Brahmi A, Carolus MJ, Delmas D, Essoussi MH, Lacabanne P, Lamiel VM, Randimbivololona F, Souyris J (2020) Industrial use of a safe and efficient formal method based software engineering process in avionics. In: Conference on European congress embedded real time systems (ERTS)"},{"key":"14_CR10","unstructured":"Brazilian Space Agency (2022) The Brazilian Space Agency\u2013The bridge to the future. https:\/\/www.gov.br\/aeb\/pt-br\/centrais-de-conteudo\/publicacoes\/LivretoBrazilianSpaceAgency.pdf. Accessed 18 Jan 2022"},{"key":"14_CR11","unstructured":"B\u00fchler D, Cuoq P, Yakobowski B, Lemerre M, Maroneze A, Perrelle V, Prevosto V Eva\u2013the evolved value analysis plug-in 24.0 (Chromium). https:\/\/www.frama-c.com\/download\/eva-manual-24.0-Chromium.pdf"},{"key":"14_CR12","unstructured":"Bureau Veritas group (2016) Bureau Veritas releases a guide, co-written with the CEA, for enhancing the reliability and performance of embedded software. https:\/\/group.bureauveritas.com\/fr\/node\/387. Accessed 27 Sep 2022"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Carrijo DS, Oliva AP, de Castro Leite Filho W (2002) Hardware-in-loop simulation development. Int J Model Simul. https:\/\/doi.org\/10.1080\/02286203.2002.11442238","DOI":"10.1080\/02286203.2002.11442238"},{"key":"14_CR14","unstructured":"CEA List (2017) Dassault Aviation innovates in cybersecurity with Frama-C. https:\/\/www.cea-tech.fr\/cea-tech\/english\/Pages\/ec_2017\/dassault-aviation-innovates-in-cybersecurity-with-frama-c-smart-digital-systems.aspx. Accessed 15 Jan 2022"},{"key":"14_CR15","unstructured":"Chess B, West J (2007) Secure programming with static analysis. Addison-Wesley"},{"key":"14_CR16","unstructured":"Clarke EM, Grumberg O, Peled DA (2000) Model checking. The MIT Press"},{"key":"14_CR17","unstructured":"Correnson L, Cuoq P, Kirchner F, Maroneze A, Prevosto V, Puccetti A, Signoles J, Yakobowski B (2021) Frama-C user manual release 24.0 (Chromium). http:\/\/frama-c.com\/download\/user-manual-24.0-Chromium.pdf. Accessed 13 Apr 2023"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference on ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Cuoq P, Monate B, Pacalet A, Prevosto V, Regehr J, Yakobowski B, Yang X (2012) Testing static analyzers with randomly generated programs. In: International symposium on NASA formal methods (NFM). Springer. https:\/\/doi.org\/10.1007\/978-3-642-28891-3_12","DOI":"10.1007\/978-3-642-28891-3_12"},{"key":"14_CR20","unstructured":"Duprat S, Lamiel VM, Kirchner F, Correnson L, Delmas D (2016) Spreading static analysis with Frama-C in industrial contexts. In: Conference on European congress embedded real time software and systems (ERTS)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Dutle A, Moscato M, Titolo L, Mu\u00f1oz C, Anderson G, Bobot F (2021) Formal analysis of the compact position reporting algorithm. Form Asp Comput 33(1), 65\u201386. https:\/\/doi.org\/10.1007\/s00165-019-00504-0","DOI":"10.1007\/s00165-019-00504-0"},{"key":"14_CR22","unstructured":"ECSS: E-ST-40C space engineering\u2014software (2009)"},{"key":"14_CR23","unstructured":"ECSS: Q-HB-80-04A Space product assurance\u2014software metrication programme definition and implementation (2011)"},{"key":"14_CR24","unstructured":"ECSS: Q-ST-80C space product assurance\u2014software product assurance (2017)"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Eisenbarth T, Koschke R, Simon D (2001) Aiding program comprehension by static and dynamic feature analysis. In: IEEE international conference on software maintenance (ICSM). https:\/\/doi.org\/10.1109\/ICSM.2001.972777","DOI":"10.1109\/ICSM.2001.972777"},{"key":"14_CR26","unstructured":"Frama-C (2012) Frama-C news and ideas homepage, 2015 [Online]. https:\/\/frama-c.com\/2012\/01\/16\/Csmith-testing.html. Accessed 27 Sep 2022"},{"key":"14_CR27","unstructured":"Gansner ER, Koutsofios E, North S (2015) Drawing graphs with dot. https:\/\/www.graphviz.org\/pdf\/dotguide.pdf"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Gao D, Reiter MK, Song D (2004) Gray-box extraction of execution graphs for anomaly detection. In: ACM conference on computer and communications security (CCS). https:\/\/doi.org\/10.1145\/1030083.1030126","DOI":"10.1145\/1030083.1030126"},{"key":"14_CR29","unstructured":"Gentsch C (2020) Evaluation of open source static analysis security testing (SAST) tools for c. Tech. rep., DLR-German Aerospace Center, Jena. https:\/\/elib.dlr.de\/133945\/"},{"key":"14_CR30","doi-asserted-by":"publisher","DOI":"10.1145\/2927299.2927301","author":"B Gregg","year":"2016","unstructured":"Gregg B (2016) The flame graph: this visualization of software execution is a new necessity for performance profiling and debugging. ACM Queue. https:\/\/doi.org\/10.1145\/2927299.2927301","journal-title":"ACM Queue"},{"key":"14_CR31","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM. https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun ACM"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Hussein M, Nouacer R, Radermacher A (2017) Towards a safe software development environment. In: Euromicro conference on digital system design (DSD). https:\/\/doi.org\/10.1109\/DSD.2017.13","DOI":"10.1109\/DSD.2017.13"},{"key":"14_CR33","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2018.07.004","author":"M Hussein","year":"2018","unstructured":"Hussein M, Nouacer R, Radermacher A, Puccetti A, Gaston C, Rapin N (2018) An end-to-end framework for safe software development. Microprocess Microsyst. https:\/\/doi.org\/10.1016\/j.micpro.2018.07.004","journal-title":"Microprocess Microsyst"},{"key":"14_CR34","unstructured":"INNOSPACE: INNOSPACE (2023). http:\/\/www.innospc.com\/myboard\/sub04_02. Accessed 13 Apr 2023"},{"key":"14_CR35","unstructured":"Instituto de Aeron\u00e1utica e Espa\u00e7o: Projeto SIA (2018). https:\/\/www.iae.dcta.mil.br\/index.php\/todos-os-projetos\/todos-os-projetos-desenvolvidos\/projetos-sia. Accessed 13 Apr 2023"},{"key":"14_CR36","unstructured":"Instituto de Aeron\u00e1utica e Espa\u00e7o: VLS-1 (2019). https:\/\/iae.dcta.mil.br\/index.php\/todos-os-projetos\/todos-os-projetos-desenvolvidos\/projetos-vls1. Accessed 20 Jan 2022"},{"key":"14_CR37","unstructured":"International Organization for Standardization (2017) ISO\/IEC\/IEEE 24765 Systems and software engineering\u2014Vocabulary"},{"key":"14_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7","author":"F Kirchner","year":"2015","unstructured":"Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2015) Frama-C: a software analysis perspective. Form Asp Comput. https:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Form Asp Comput"},{"key":"14_CR39","doi-asserted-by":"publisher","unstructured":"Kumar N, Neema S, Das M, Mohan BR (2021) Program slicing analysis with KLEE, DIVINE and Frama-C. In: International conference on automation and computing (ICAC). https:\/\/doi.org\/10.23919\/ICAC50006.2021.9594142","DOI":"10.23919\/ICAC50006.2021.9594142"},{"key":"14_CR40","doi-asserted-by":"publisher","unstructured":"Maroneze A, Perrelle V, Kirchner F (2019) Advances in usability of formal methods for code verification with Frama-C. Electron Commun EASST. https:\/\/doi.org\/10.14279\/tuj.eceasst.77.1108. Interactive workshop on the industrial application of verification and testing (ETAPS)","DOI":"10.14279\/tuj.eceasst.77.1108"},{"key":"14_CR41","unstructured":"Ministry of Defense (2012) Defense white paper\u2013Livro Branco de Defesa Nacional. https:\/\/www.gov.br\/defesa\/pt-br\/arquivos\/estado_e_defesa\/livro_branco\/lbdna_2013a_inga_net.pdf. Accessed 18 Jan 2022"},{"key":"14_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-016-9332-8","author":"V Musco","year":"2017","unstructured":"Musco V, Monperrus M, Preux P (2017) A large-scale study of call graph-based impact prediction using mutation testing. Softw Qual J. https:\/\/doi.org\/10.1007\/s11219-016-9332-8","journal-title":"Softw Qual J"},{"key":"14_CR43","unstructured":"NASA (2022) NPR 7150.2D NASA software engineering requirements"},{"key":"14_CR44","doi-asserted-by":"publisher","DOI":"10.1016\/j.net.2014.12.009","author":"A Ourghanlian","year":"2015","unstructured":"Ourghanlian A (2015) Evaluation of static analysis tools used to assess software important to nuclear power plant safety. Nucl Eng Technol. https:\/\/doi.org\/10.1016\/j.net.2014.12.009","journal-title":"Nucl Eng Technol"},{"key":"14_CR45","doi-asserted-by":"publisher","unstructured":"Ramos F (2015) History and current status of SISNAV: a brief report. In: Simp\u00f3sio Brasileiro de Engenharia Inercial (SBEIN). https:\/\/doi.org\/10.13140\/RG.2.1.3529.0323","DOI":"10.13140\/RG.2.1.3529.0323"},{"key":"14_CR46","unstructured":"Romani M, Takahashi P, Lahoz C (2009) A process of code inspection for space software. In: Conf. on Int. astronautical congress"},{"key":"14_CR47","unstructured":"RTCA\/EUROCAE (2011) RTCA DO-178C software considerations in airborne systems and equipment certification"},{"key":"14_CR48","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1979.234183","author":"BG Ryder","year":"1979","unstructured":"Ryder BG (1979) Constructing the call graph of a program. IEEE Trans Softw Eng. https:\/\/doi.org\/10.1109\/TSE.1979.234183","journal-title":"IEEE Trans Softw Eng"},{"key":"14_CR49","unstructured":"Signoles J (2020) Abstract interpretation and properties of c programs. http:\/\/ejcp2019.icube.unistra.fr\/slides\/js.pdf. Accessed 10 Dec 2020"},{"key":"14_CR50","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2508559","author":"RAB Silva","year":"2016","unstructured":"Silva RAB, Arai NN, Burgareli LA, Oliveira JMP, Pinto JS (2016) Formal verification with Frama-C: a case study in the space software domain. IEEE Trans Reliab. https:\/\/doi.org\/10.1109\/TR.2015.2508559","journal-title":"IEEE Trans Reliab"},{"key":"14_CR51","unstructured":"Software & Systems Engineering Standards Committee (2009) IEEE 1044 standard classification for software anomalies"},{"key":"14_CR52","unstructured":"de\u00a0Souza J, Filho W (2012) Sistema de Navega\u00e7\u00e3o Inercial SISNAV - Mec\u00e2nica e Eletr\u00f4nica Embarcada. In: Simp\u00f3sio Brasileiro de Engenharia Inercial (SBEIN)"},{"key":"14_CR53","unstructured":"Stack Overflow (2019) Sparecode analysis in Frama-C. https:\/\/stackoverflow.com\/questions\/59240081\/sparecode-analysis-in-frama-c"},{"key":"14_CR54","unstructured":"TrustInSoft (2022) https:\/\/trust-in-soft.com. Accessed 15 Jan 2022"},{"key":"14_CR55","unstructured":"VESSEDIA (2022) https:\/\/cordis.europa.eu\/project\/id\/731453. Accessed 15 Jan 2022"}],"container-title":["Computer Science Foundations and Applied Logic","Guide to Software Verification with Frama-C"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-55608-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T07:06:56Z","timestamp":1720508816000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-55608-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031556074","9783031556081"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-55608-1_14","relation":{},"ISSN":["2731-5754","2731-5762"],"issn-type":[{"type":"print","value":"2731-5754"},{"type":"electronic","value":"2731-5762"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"10 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}