{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T19:22:49Z","timestamp":1767986569668,"version":"3.49.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,7,12]],"date-time":"2012-07-12T00:00:00Z","timestamp":1342051200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10664-012-9215-y","type":"journal-article","created":{"date-parts":[[2012,7,11]],"date-time":"2012-07-11T10:40:38Z","timestamp":1342003238000},"page":"39-68","source":"Crossref","is-referenced-by-count":10,"title":["Contributions of model checking and CoFI methodology to the development of space embedded software"],"prefix":"10.1007","volume":"19","author":[{"given":"Rodrigo Pastl","family":"Pontes","sequence":"first","affiliation":[]},{"given":"Paulo Claudino","family":"V\u00e9ras","sequence":"additional","affiliation":[]},{"given":"Ana Maria","family":"Ambrosio","sequence":"additional","affiliation":[]},{"given":"Em\u00edlia","family":"Villani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,7,12]]},"reference":[{"key":"9215_CR1","doi-asserted-by":"crossref","DOI":"10.1002\/0470114754","volume-title":"An introduction to categorical data analysis","author":"A Agresti","year":"2007","unstructured":"Agresti A (2007) An introduction to categorical data analysis, 2nd edn. Wiley, Hoboken, 372 p","edition":"2"},{"key":"9215_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DA (1994) Theory of timed automata. Theor Comput Sci 126:183\u2013235","journal-title":"Theor Comput Sci"},{"issue":"4","key":"9215_CR3","doi-asserted-by":"crossref","first-page":"146","DOI":"10.2514\/1.15529","volume":"3","author":"AM Ambrosio","year":"2006","unstructured":"Ambrosio AM, Martins E, Vijaykumar NL, Carvalho SV (2006) A conformance testing process for space applications software services. J Aerosp Comput Inf Commun (JACIC), USA 3(4):146\u2013158","journal-title":"J Aerosp Comput Inf Commun (JACIC), USA"},{"key":"9215_CR4","doi-asserted-by":"crossref","unstructured":"Ambrosio AM, Francisco MFM, Martins E (2008) An independent software verification and validation process for space applications. Proceedings of the 9th Conference on Space Operations (SpaceOps). Heidelberg (Germany)","DOI":"10.2514\/6.2008-3517"},{"key":"9215_CR5","unstructured":"Anjos JMS, Gripp J, Pontes RP, Villani E (2011) Applying the CoFI testing methodology to a multifunctional robot end-effector. Proceedings of the 5th Latin-American Symposium on Dependable Computing (LADC)\u2014Industrial Track, S\u00e3o Jos\u00e9 dos Campos (Brasil)"},{"key":"9215_CR6","doi-asserted-by":"crossref","unstructured":"Arias R, Kucinskis FN, Alonso JDD (2008) Lessons learned from an onboard ECSS PUS object-oriented implementation. Proceedings of the 9th Conference on Space Operations (SpaceOps). Heildeberg, Germany","DOI":"10.2514\/6.2008-3524"},{"key":"9215_CR7","unstructured":"Behrmann G et al (2005) A Tutorial on UPPAAL. Proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT\u201c04). LNCS v. 3185"},{"key":"9215_CR8","doi-asserted-by":"crossref","unstructured":"Chan W, Anderson RJ, Beame P, Burns S, Modugno F, Notkin D, Reese JD (1998) Model checking large software specifications corrections. IEEE Transactions on Software Engineering, vol.24, no. 7, pp 498\u2013520","DOI":"10.1109\/32.708566"},{"key":"9215_CR9","doi-asserted-by":"crossref","unstructured":"Cofer D, Whalen M, Miller S, Collins R (2008) Software model checking for avionics systems. Proceedings of 27th digital Avionics Systems Conference. ISSN: 0-7803-7367-7\/02, pp 5.D.5-1\u20135.D.5-8","DOI":"10.1109\/DASC.2008.4702862"},{"key":"9215_CR10","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/j.entcs.2004.12.005","volume":"111","author":"M Conrad","year":"2005","unstructured":"Conrad M, Fey I, Sadeghipour S (2005) Systematic model-based testing of embedded automotive software. Electron Notes Theor Comput Sci 111:13\u201326","journal-title":"Electron Notes Theor Comput Sci"},{"key":"9215_CR11","doi-asserted-by":"crossref","first-page":"1487","DOI":"10.1016\/j.infsof.2009.06.010","volume":"51","author":"AC Dias-Neto","year":"2009","unstructured":"Dias-Neto AC, Travassos GH (2009) Model-based testing approaches selection for software projects. Inf Softw Technol 51:1487\u20131504","journal-title":"Inf Softw Technol"},{"key":"9215_CR12","doi-asserted-by":"crossref","first-page":"1286","DOI":"10.1016\/j.infsof.2010.07.001","volume":"52","author":"R Dorofeeva","year":"2010","unstructured":"Dorofeeva R, El-Fakih K, Maag S, Cavalli AR, Yevtushenko N (2010) FSM-based conformance testing methods: a survey annotated with experimental evaluation. Inf Softw Technol 52:1286\u20131297","journal-title":"Inf Softw Technol"},{"key":"9215_CR13","unstructured":"ECSS (2003) Ground systems and operations\u2014telemetry and telecommand and packet utilization. ECSS-E-70-41A, ESA Publications"},{"key":"9215_CR14","unstructured":"ECSS (2008) Description, implementation and general requirements. ECSS-S-ST-00C, ESA Publications"},{"key":"9215_CR15","unstructured":"Garc\u00eda F, Sanchez A (2006) Formal verification of safety and liveness properties for logic controllers. A tool comparison. Proceedings of 3rd International Conference on Electrical and Electronics Engineering, pp 1\u20133"},{"key":"9215_CR16","unstructured":"Gl\u00fcck PR, Holzmann GJ (2001) Using SPIN model checking for flight software verification. Proceedings of the Aerospace Conference, pp 105\u2013113"},{"issue":"6","key":"9215_CR17","doi-asserted-by":"crossref","first-page":"720","DOI":"10.1007\/s10664-009-9107-y","volume":"14","author":"G G\u00fcle\u015fir","year":"2009","unstructured":"G\u00fcle\u015fir G, van den Berg K, Bergmans L, Ak\u015fit M (2009) Experiment evaluation of a tool for the verification and transformation of source code in event-driven systems. Empir Softw Eng 14(6):720\u2013777","journal-title":"Empir Softw Eng"},{"key":"9215_CR18","doi-asserted-by":"crossref","unstructured":"Hendriks M, Verhoef M (2006) Timed automata based analysis of embedded system architectures. Proceedings of the 20th Int. Parallel and Distributed Processing Symposium","DOI":"10.1109\/IPDPS.2006.1639422"},{"issue":"4","key":"9215_CR19","doi-asserted-by":"crossref","first-page":"564","DOI":"10.2514\/1.11950","volume":"41","author":"N Leveson","year":"2005","unstructured":"Leveson N (2005) Role of software in spacecraft accidents. J Spacecrafts Rockets 41(4):564\u2013575","journal-title":"J Spacecrafts Rockets"},{"key":"9215_CR20","unstructured":"Lions JL (1996) Ariane 501 Inquiry Board report. Press Release N\u00ba 33, ESA, 1996. Available at: < http:\/\/esamultimedia.esa.int\/docs\/esa-x-1819eng.pdf >. Accessed in: October 3rd 2010"},{"issue":"4","key":"9215_CR21","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1023\/A:1008930105477","volume":"8","author":"E Martins","year":"1999","unstructured":"Martins E, Sabi\u00e3o SB, Ambrosio AM (1999) ConData: a tool for automating specification-based test case generation for communication systems. Softw Qual J 8(4):303\u2013319","journal-title":"Softw Qual J"},{"key":"9215_CR22","unstructured":"JK Microsystems (2009) eRTOS. Available at: < http:\/\/www.jkmicro.com\/products\/ertos.html >. Accessed in: May 3rd 2009"},{"key":"9215_CR23","doi-asserted-by":"crossref","unstructured":"Morais MHE, Ambrosio AM (2010) A new model-based approach for analysis and refinement of requirement specification to space operations. Proceedings of the 10th Conference on Space Operations (SpaceOps). Huntsville (Alabama, USA)","DOI":"10.2514\/6.2010-2231"},{"key":"9215_CR24","doi-asserted-by":"crossref","unstructured":"Notebaert O (2006) Benefits of the standardization efforts for onboard data interfaces and services. Proceedings of the 8th Conference on Space Operations (SpaceOps). Rome, Italy","DOI":"10.2514\/6.2006-5678"},{"key":"9215_CR25","doi-asserted-by":"crossref","unstructured":"Ogawa H, Kumeno F, Honiden S (2008) Model checking process with goal oriented requirement analysis. Proceedings of 15th Asian-Pacific Software Engineering Conference, pp 377\u2013384","DOI":"10.1109\/APSEC.2008.71"},{"key":"9215_CR26","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/j.infsof.2003.09.005","volume":"46","author":"A Paradkar","year":"2004","unstructured":"Paradkar A (2004) Towards model-based generation of self-priming and self-checking conformance tests for interactive systems. Inf Softw Technol 46:315\u2013322","journal-title":"Inf Softw Technol"},{"key":"9215_CR27","doi-asserted-by":"crossref","unstructured":"Partharasathy G et al (2003) A comparison of BDDs, BMC, and sequential SAT for model checking. Proc. of the 8th IEEE International Workshop on High-Level Design Validation and Test Workshop, pp 157\u2013163","DOI":"10.1109\/HLDVT.2003.1252490"},{"key":"9215_CR28","doi-asserted-by":"crossref","unstructured":"Pingree PJ, Mikk E, Holzmann GJ, Smith MH, Dams D (2002) Validation of mission critical software design and implementation using model checking. Proceedings of the 21st Digital Avionics Systems Conference, p 6.A.4-1","DOI":"10.1109\/DASC.2002.1067982"},{"key":"9215_CR29","unstructured":"Pontes RP (2011) Contribui\u00e7\u00f5es do Model Checking e da Metodologia CoFI para o software embarcado espacial. 257 f. Master Thesis, Instituto Tecnol\u00f3gico de Aeron\u00e1utica (ITA), S\u00e3o Jos\u00e9 dos Campos-SP"},{"key":"9215_CR30","unstructured":"Pontes RP, Essado M, V\u00e9ras PC, Ambrosio AM, Villani E (2009) A comparative analysis of two verification techniques for DEDS: model checking versus model-based testing. Proceedings of 4th IFAC Workshop on Discrete Event System Design (DEDes), pp 70\u201375, Valencia (Spain)"},{"key":"9215_CR31","unstructured":"Pontes RP, Essado M, V\u00e9ras PC, Ambrosio AM, Villani E (2009) Model based refinement of requirement specification: a comparison of two V&V approaches. Proceedings of 20th International Congress of Mechanical Engineering, Gramado (RS, Brazil)"},{"key":"9215_CR32","doi-asserted-by":"crossref","unstructured":"Pontes RP, Martins E, Ambrosio AM, Villani E (2010) Embedded critical software testing for aerospace applications based on PUS. Proceedings of XXVIII Simp\u00f3sio Brasileiro de Redes de Computadores e Sistemas Distribu\u00eddos (SBRC)\/XI Workshop de Testes e Toler\u00e2ncia a Falhas (WTF), Gramado\u2014RS, Brazil","DOI":"10.5753\/wtf.2010.23100"},{"key":"9215_CR33","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/j.entcs.2004.02.086","volume":"116","author":"W Prenninger","year":"2005","unstructured":"Prenninger W, Pretschner A (2005) Abstractions for model-based testing. Electron Notes Theor Comput Sci 116:59\u201371","journal-title":"Electron Notes Theor Comput Sci"},{"key":"9215_CR34","doi-asserted-by":"crossref","unstructured":"Romero EL et al (2005) Comparing two testbench methods for hierarchical functional verification of a bluetooth baseband adaptor. Proc. of the 3rd IEEE\/ACM\/IFIP Int. Conf. on Hardware\/Software Codesign and System Synthesis, pp 327\u2013332","DOI":"10.1145\/1084834.1084914"},{"key":"9215_CR35","doi-asserted-by":"crossref","unstructured":"Rozier KY (2010) Linear temporal logic symbolic model checking. Comput Sci Rev. doi: 10.1016\/j.cosrev.2010.06.002","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"9215_CR36","doi-asserted-by":"crossref","unstructured":"Schuele T, Schneider K (2004) Global vs. local model checking: a comparison of verification techniques for infinite state systems. Proceedings of the 2nd International Conference on Software Engineering and Formal Methods","DOI":"10.1109\/SEFM.2004.1347504"},{"key":"9215_CR37","unstructured":"Seveg E et al (2004) Evaluating and comparing simulation verification vs. formal verification approach on block level design. Proc of the 11th IEEE Int Conf on Electronics, Circuits and Systems (ICECS), pp 515\u2013518"},{"key":"9215_CR38","doi-asserted-by":"crossref","unstructured":"Sreemani T, Atlee JM (1996) Feasibility of model checking software requirements: a case study. Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS), Gaithersburg, MD, USA, pp 77\u201388","DOI":"10.1109\/CMPASS.1996.507877"},{"key":"9215_CR39","doi-asserted-by":"crossref","unstructured":"Tafazoli M (2009) A study of on-orbit spacecraft failures. Acta Astronautica 64:195\u2013205","DOI":"10.1016\/j.actaastro.2008.07.019"},{"key":"9215_CR40","doi-asserted-by":"crossref","unstructured":"Tiwari A, Sinha P, Ramachandran U (2003) On the run-time verification of autonomy software. Proceedings of the 28th Annual NASA Goddard Software Engineering Workshop","DOI":"10.1109\/SEW.2003.1270726"},{"key":"9215_CR41","unstructured":"Wong WE, Debroy V, Restrepo A (2009) The role of software in recent catastrophic accidents. IEEE Reliability Society 2009 Annual Technology Report"},{"key":"9215_CR42","doi-asserted-by":"crossref","unstructured":"V\u00e9ras PC, Villani E, Ambr\u00f3sio AM, Pontes RP, Vieira M, Madeira H (2010) Benchmarking software requirements documentation for space application. Proceedings of the 29th International Conference on Computer Safety, Reliability and Security (SAFECOMP), Viena","DOI":"10.1007\/978-3-642-15651-9_9"},{"key":"9215_CR43","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-4625-2","volume-title":"Experimentation in software engineering: an introduction","author":"C Wohlin","year":"2000","unstructured":"Wohlin C et al (2000) Experimentation in software engineering: an introduction. Kluwer, Dordrecht, 204p"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-012-9215-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10664-012-9215-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-012-9215-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,24]],"date-time":"2023-06-24T06:31:43Z","timestamp":1687588303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10664-012-9215-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,12]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["9215"],"URL":"https:\/\/doi.org\/10.1007\/s10664-012-9215-y","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,12]]}}}