{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:40:25Z","timestamp":1767984025404,"version":"3.49.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"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-10794-7_8","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:28Z","timestamp":1763189008000},"page":"143-161","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Safe Temperature Regulation: Formally Verified and\u00a0Real-World Validated"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5035-8559","authenticated-orcid":false,"given":"Carlos","family":"Isasa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3987-9919","authenticated-orcid":false,"given":"Noah","family":"Abou El Wafa","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2692-9742","authenticated-orcid":false,"given":"Claudio","family":"Gomes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4589-1500","authenticated-orcid":false,"given":"Peter Gorm","family":"Larsen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/j.rser.2017.10.044","volume":"83","author":"Z Afroz","year":"2018","unstructured":"Afroz, Z., Shafiullah, G., Urmee, T., Higgins, G.: Modeling techniques used in building HVAC control systems: a review. Renew. Sustain. Energy Rev. 83, 64\u201384 (2018). https:\/\/doi.org\/10.1016\/j.rser.2017.10.044","journal-title":"Renew. Sustain. Energy Rev."},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Bohrer, R., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, Paris, France, 16\u201317 January 2017, pp. 208\u2013221. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018616","DOI":"10.1145\/3018610.3018616"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Bohrer, R., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: VeriPhy: verified controller executables from verified cyber-physical system models. In: Grossman, D. (ed.) PLDI, pp. 617\u2013630. ACM, Philadelphia (2018). https:\/\/doi.org\/10.1145\/3192366.3192406","DOI":"10.1145\/3192366.3192406"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Buhagiar, A.J., Freitas, L., III, W.E.S., Larsen, P.G.: Digital twins for organ preservation devices. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022, Part IV. LNCS, vol. 13704, pp. 22\u201336. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19762-8_3","DOI":"10.1007\/978-3-031-19762-8_3"},{"key":"8_CR5","volume-title":"Thermodynamics: An Engineering Approach","author":"YA Cengel","year":"2011","unstructured":"Cengel, Y.A., Boles, M.A., Kano\u011flu, M.: Thermodynamics: An Engineering Approach, vol. 5. McGraw-Hill, New York (2011)"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1016\/j.arcontrol.2020.09.001","volume":"50","author":"J Drgo\u0148a","year":"2020","unstructured":"Drgo\u0148a, J., et al.: All you need to know about model predictive control for buildings. Annu. Rev. Control. 50, 190\u2013232 (2020). https:\/\/doi.org\/10.1016\/j.arcontrol.2020.09.001","journal-title":"Annu. Rev. Control."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Feng, H., Gomes, C., Thule, C., Lausdahl, K., Sandberg, M., Larsen, P.G.: The incubator case study for digital twin engineering (2021). https:\/\/arxiv.org\/abs\/2102.10390","DOI":"10.23919\/ANNSIM52504.2021.9552135"},{"key":"8_CR8","unstructured":"Feng, H., Gomes, C., Larsen, P.G.: Model-based monitoring and state estimation for digital twins: the Kalman filter (2023). https:\/\/arxiv.org\/abs\/2305.00252"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Frahm, M., Langner, F., Zwickel, P., Matthes, J., Mikut, R., Hagenmeyer, V.: How to derive and implement a minimalistic RC model from thermodynamics for the control of thermal parameters for assuring thermal comfort in buildings. In: 2022 Open Source Modelling and Simulation of Energy Systems (OSMSES), pp.\u00a01\u20136. IEEE, Aachen, Germany (2022). https:\/\/doi.org\/10.1109\/osmses54027.2022.9769134","DOI":"10.1109\/osmses54027.2022.9769134"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera\u00a0X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Garcia, L., Mitsch, S., Platzer, A.: HyPLC: hybrid programmable logic controller program translation for verification. In: Bushnell, L., Pajic, M. (eds.) ICCPS, pp. 47\u201356 (2019). https:\/\/doi.org\/10.1145\/3302509.3311036","DOI":"10.1145\/3302509.3311036"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Isasa, C., Abou El Wafa, N., Platzer, A., Larsen, P.G., Gomes, C.: Artifact for Safe Temperature Regulation: Formally Verified and Real-World Validated. https:\/\/doi.org\/10.6084\/m9.figshare.28869218","DOI":"10.6084\/m9.figshare.28869218"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Jeannin, J., et al.: Formal verification of ACAS X, an industrial airborne collision avoidance system. In: Girault, A., Guan, N. (eds.) EMSOFT, pp. 127\u2013136. IEEE Press, Amsterdam, Netherlands (2015). https:\/\/doi.org\/10.1109\/EMSOFT.2015.7318268","DOI":"10.1109\/EMSOFT.2015.7318268"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Kabra, A., Mitsch, S., Platzer, A.: Verified train controllers for the federal railroad administration train kinematics model: balancing competing brake and track forces. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4409\u20134420 (2022). https:\/\/doi.org\/10.1109\/TCAD.2022.3197690","DOI":"10.1109\/TCAD.2022.3197690"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Kapuria, A., Cole, D.G.: Formal verification of a nuclear plant thermal dispatch operation using system decomposition. In: 2024 IEEE 6th International Conference on Trust, Privacy and Security in Intelligent Systems, and Applications (TPS-ISA), pp. 543\u2013548 (2024). https:\/\/doi.org\/10.1109\/TPS-ISA62245.2024.00074","DOI":"10.1109\/TPS-ISA62245.2024.00074"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17164-2_1","volume-title":"Programming Languages and Systems","author":"J Liu","year":"2010","unstructured":"Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1\u201315. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_1"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 33\u201374 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0241-z","DOI":"10.1007\/s10703-016-0241-z"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0","DOI":"10.1007\/978-3-319-63588-0"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246\u2013265. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10373-5_13"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Platzer, A., Tan, Y.K.: Differential equation invariance axiomatization. J. ACM 67(1), 6:1\u20136:66 (2020). https:\/\/doi.org\/10.1145\/3380825","DOI":"10.1145\/3380825"},{"key":"8_CR21","unstructured":"Serway, R.A., Faughn, J.S.: College Physics, 5th edn. Saunders College Publishing, Philadelphia (1999)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-030-30942-8_10","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"A Sogokon","year":"2019","unstructured":"Sogokon, A., Mitsch, S., Tan, Y.K., Cordwell, K., Platzer, A.: Pegasus: a framework for sound continuous invariant generation. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 138\u2013157. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_10"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Mitsch, S., Platzer, A.: Verifying switched system stability with logic. In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control. HSCC 2022. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3501710.3519541","DOI":"10.1145\/3501710.3519541"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Wright, T., Gomes, C., Woodcock, J.: Formally verified self-adaptation of an incubator digital twin. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022, Part IV. LNCS, vol. 13704, pp. 89\u2013109. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19762-8_7","DOI":"10.1007\/978-3-031-19762-8_7"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54108-7_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"L Zou","year":"2014","unstructured":"Zou, L., et al.: Verifying Chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262\u2013280. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_14"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:37Z","timestamp":1767967177000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}