{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:55:27Z","timestamp":1757627727581,"version":"3.44.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032009418"},{"type":"electronic","value":"9783032009425"}],"license":[{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-00942-5_14","type":"book-chapter","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T12:03:20Z","timestamp":1756296200000},"page":"261-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Specification-Driven Approach to\u00a0Embedded FDIR Code Generation"],"prefix":"10.1007","author":[{"given":"Federico","family":"Bonafini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Cavada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillermo","family":"Gomez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,28]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-12214-4_7","volume-title":"Model-Based Safety and Assessment","author":"B Bittner","year":"2014","unstructured":"Bittner, B., Bozzano, M., Cimatti, A., De Ferluc, R., Gario, M., Guiotto, A., Yushtein, Y.: An integrated process for FDIR design in aerospace. In: Ortmeier, F., Rauzy, A. (eds.) IMBSA 2014. LNCS, vol. 8822, pp. 82\u201395. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12214-4_7"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-031-15842-1_2","volume-title":"Model-Based Safety and Assessment","author":"A Bombardelli","year":"2022","unstructured":"Bombardelli, A., et al.: COMPASTA: extending TASTE with formal design and verification functionality. In: Seguin, C., Zeller, M., Prosvirnova, T. (eds.) IMBSA 2022. LNCS, vol. 13525, pp. 21\u201327. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15842-1_2"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-54862-8_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Bozzano","year":"2014","unstructured":"Bozzano, M., Cimatti, A., Gario, M., Tonetta, S.: Formal design of fault detection and identification components using temporal epistemic logic. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 326\u2013340. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_22"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Gario, M., Tonetta, S.: Formal design of asynchronous fault detection and identification components using temporal epistemic logic. Log. Methods Comput. Sci. 11(4) (2015)","DOI":"10.2168\/LMCS-11(4:4)2015"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Bombardelli, A., Cimatti, A., Griggio, A., Tonetta, S.: Another look at LTL modulo theory over finite and infinite traces. In: Jansen, N., et al. (eds.) Principles of Verification: Cycling the Probabilistic Landscape. LNCS, vol. 15260, pp. 419\u2013443. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-75783-9_17","DOI":"10.1007\/978-3-031-75783-9_17"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4):14:1\u201314:64 (2011)","DOI":"10.1145\/2000799.2000800"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-39878-3_5","volume-title":"Computer Safety, Reliability, and Security","author":"M Bozzano","year":"2003","unstructured":"Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: the FSAP\/NuSMV-SA safety analysis platform. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 49\u201362. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39878-3_5"},{"issue":"5","key":"14_CR8","doi-asserted-by":"publisher","first-page":"2163","DOI":"10.1109\/TSMCB.2004.835010","volume":"34","author":"M-O Cordier","year":"2004","unstructured":"Cordier, M.-O., Dague, P., L\u00e9vy, F., Montmain, J., Staroswiecki, M., Trav\u00e9-Massuy\u00e8s, L.: Conflicts versus analytical redundancy relations: a comparative analysis of the model based diagnosis approach from the artificial intelligence and automatic control perspectives. IEEE Trans. Syst. Man Cybern. Part B 34(5), 2163\u20132177 (2004)","journal-title":"IEEE Trans. Syst. Man Cybern. Part B"},{"key":"14_CR9","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd ed. MIT Press (2018)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Chen, J., Patton, R.J.: Robust Model-Based Fault Diagnosis for Dynamic Systems. The International Series on Asian Studies in Computer and Information Science, vol. 3. Kluwer (1999)","DOI":"10.1007\/978-1-4615-5149-2"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-030-32079-9_23","volume-title":"Runtime Verification","author":"A Cimatti","year":"2019","unstructured":"Cimatti, A., Tian, C., Tonetta, S.: NuRV: a nuXmv extension for runtime verification. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 382\u2013392. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_23"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"de\u00a0Kleer, J., Mackworth, A.K., Reiter, R.: Characterizing Diagnoses. In: AAAI, pp. 324\u2013330. AAAI Press\/The MIT Press (1990)","DOI":"10.1007\/3-540-53104-1_27"},{"issue":"6","key":"14_CR13","doi-asserted-by":"publisher","first-page":"3757","DOI":"10.1109\/TIE.2015.2417501","volume":"62","author":"Z Gao","year":"2015","unstructured":"Gao, Z., Cecati, C., Ding, S.X.: A survey of fault diagnosis and fault-tolerant techniques-part I: fault diagnosis with model-based and signal-based approaches. IEEE Trans. Industr. Electron. 62(6), 3757\u20133767 (2015)","journal-title":"IEEE Trans. Industr. Electron."},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Gertler, J.: Fault Detection and Diagnosis. In: Baillieul, J., Samad, T. (eds) Encyclopedia of Systems and Control, pp. 764\u2013749. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-030-44184-5_223","DOI":"10.1007\/978-3-030-44184-5_223"},{"issue":"3","key":"14_CR15","doi-asserted-by":"publisher","first-page":"636","DOI":"10.1109\/TCST.2009.2026285","volume":"18","author":"I Hwang","year":"2010","unstructured":"Hwang, I., Kim, S., Kim, Y., Seah, C.E.: A survey of fault detection, isolation, and reconfiguration methods. IEEE Trans. Control. Syst. Technol. 18(3), 636\u2013653 (2010)","journal-title":"IEEE Trans. Control. Syst. Technol."},{"issue":"4","key":"14_CR16","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/0005-1098(84)90098-0","volume":"20","author":"R Isermann","year":"1984","unstructured":"Isermann, R.: Process fault detection based on modeling and estimation methods - a survey. Autom. 20(4), 387\u2013404 (1984)","journal-title":"Autom."},{"issue":"1","key":"14_CR17","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.arcontrol.2004.12.002","volume":"29","author":"R Isermann","year":"2005","unstructured":"Isermann, R.: Model-based fault-detection and diagnosis - status and applications. Annu. Rev. Control. 29(1), 71\u201385 (2005)","journal-title":"Annu. Rev. Control."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Kiesbye, J., Grover, K., Ket\u00ednsk\u00fd, J.: Model checking for proving and improving fault tolerance of satellites. In: 2023 IEEE Aerospace Conference, pp. 1\u20139 (2023)","DOI":"10.1109\/AERO55745.2023.10115801"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"M\u00fcller, S., H\u00f6flinger, K., Smisek, M., Gerndt, A.: Towards an FDIR software fault tree library for onboard computers. In: 2020 IEEE Aerospace Conference, pp. 1\u201310 (2020)","DOI":"10.1109\/AERO47225.2020.9172756"},{"issue":"5","key":"14_CR20","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1016\/0005-1098(71)90028-8","volume":"7","author":"RK Mehra","year":"1971","unstructured":"Mehra, R.K., Peschon, J.: An innovations approach to fault detection and diagnosis in dynamic systems. Automatica 7(5), 637\u2013640 (1971)","journal-title":"Automatica"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"14_CR22","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"14_CR23","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/j.engappai.2017.10.012","volume":"68","author":"A Zolghadri","year":"2018","unstructured":"Zolghadri, A.: The challenge of advanced model-based FDIR for real-world flight-critical applications. Eng. Appl. Artif. Intell. 68, 249\u2013259 (2018)","journal-title":"Eng. Appl. Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-00942-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T04:41:23Z","timestamp":1757479283000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-00942-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,28]]},"ISBN":["9783032009418","9783032009425"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-00942-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,28]]},"assertion":[{"value":"28 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/FMICS2025.uni-muenster.de","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}