{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T15:46:51Z","timestamp":1759160811343,"version":"3.38.0"},"reference-count":58,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2025,2,3]],"date-time":"2025-02-03T00:00:00Z","timestamp":1738540800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"funder":[{"name":"FOCETA","award":["956123"],"award-info":[{"award-number":["956123"]}]}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["SIMULATION"],"published-print":{"date-parts":[[2025,3]]},"abstract":"<jats:p> Effective management of depth of anesthesia (DoA) is crucial for patient safety in healthcare. Anesthesiologists typically adjust anesthetic dosages to maintain desired sedation, analgesia (pain relief), and muscle relaxation states. In this paper, we present a digital twin (DT) architecture for the formal modeling and verification of an infusion pump controller for DoA management. The DT incorporates a virtual patient model, an autonomous DoA controller adjusting the infusion rate of the anesthetic agent, i.e., propofol, a test-case manager, and a runtime verification monitor. Data exchange occurs via Ethernet frames. Challenges arise from noise in the Bispectral Index monitoring system readings and infusion rate measurements in clinical scenarios. To mitigate noise impact, we design a feedback controller that is robust against noise. We reason about DT performance by evaluating control specifications using a temporal-logic language within the context of our runtime verification tool. <\/jats:p>","DOI":"10.1177\/00375497241311617","type":"journal-article","created":{"date-parts":[[2025,2,3]],"date-time":"2025-02-03T10:32:22Z","timestamp":1738578742000},"page":"341-360","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":1,"title":["Digital twin for the formal analysis of a depth of anesthesia controller"],"prefix":"10.1177","volume":"101","author":[{"given":"Mohamed","family":"AbdElSalam","sequence":"first","affiliation":[{"name":"Siemens EDA, Egypt"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, VERIMAG, France"}]},{"given":"Antoine","family":"Delacourt","sequence":"additional","affiliation":[{"name":"Siemens Industry Software SAS, France"}]},{"given":"Weicheng","family":"He","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, VERIMAG, France"}]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[{"name":"Aristotle University of Thessaloniki, Greece"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2358-4270","authenticated-orcid":false,"given":"Nikolaos","family":"Kekatos","sequence":"additional","affiliation":[{"name":"School of Informatics, Aristotle University of Thessaloniki, Greece"}]},{"given":"Ricardo","family":"Nolasco Ruiz","sequence":"additional","affiliation":[{"name":"RGB Medical Devices, Spain"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[{"name":"Bar-Ilan University, Israel"}]},{"given":"Matthieu","family":"Ponchant","sequence":"additional","affiliation":[{"name":"Siemens Industry Software SAS, France"}]},{"given":"Ismail","family":"Ryad","sequence":"additional","affiliation":[{"name":"Siemens EDA, Egypt"}]},{"given":"Anastasios","family":"Temperekidis","sequence":"additional","affiliation":[{"name":"Aristotle University of Thessaloniki, Greece"}]},{"given":"Changshun","family":"Wu","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, VERIMAG, France"}]}],"member":"179","published-online":{"date-parts":[[2025,2,3]]},"reference":[{"key":"bibr1-00375497241311617","first-page":"3","volume":"8","author":"Grieves M","year":"2016","journal-title":"Florida Inst Tech"},{"key":"bibr2-00375497241311617","unstructured":"Grieves M. Digital twin: manufacturing excellence through virtual factory replication\u2014A whitepaper by Dr. Michael Grieves, 2015."},{"key":"bibr3-00375497241311617","unstructured":"Grieves MW. Virtually intelligent product systems: digital and physical twins. In: Complex systems engineering: theory and practice, https:\/\/api.semanticscholar.org\/CorpusID:202478997"},{"key":"bibr4-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/j.jmsy.2019.10.001"},{"key":"bibr5-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/j.cirpj.2020.02.002"},{"key":"bibr6-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/j.cirp.2017.04.040"},{"key":"bibr7-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2970143"},{"key":"bibr8-00375497241311617","first-page":"100383","volume":"30","author":"Sharma A","year":"2022","journal-title":"J Ind Inf Integr"},{"key":"bibr9-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-38756-7_4"},{"key":"bibr10-00375497241311617","doi-asserted-by":"publisher","DOI":"10.3389\/fgene.2018.00031"},{"key":"bibr11-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1007\/s00170-017-0233-1"},{"key":"bibr12-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1186\/s12938-018-0455-y"},{"key":"bibr13-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1093\/bja\/ael120"},{"key":"bibr14-00375497241311617","doi-asserted-by":"publisher","DOI":"10.4103\/0019-5049.103956"},{"volume-title":"Bispectral index","year":"2023","author":"Mathur S","key":"bibr15-00375497241311617"},{"key":"bibr16-00375497241311617","doi-asserted-by":"publisher","DOI":"10.3390\/s101210896"},{"key":"bibr17-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1097\/00000539-200005000-00021"},{"key":"bibr18-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/S0195-5616(99)50059-4"},{"key":"bibr19-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1093\/bja\/aeu313"},{"key":"bibr20-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1093\/bja\/aeu312"},{"key":"bibr21-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.03.061"},{"key":"bibr22-00375497241311617","first-page":"1","volume-title":"International doctoral workshop on mathematical and engineering methods in computer science","author":"Basu A","year":"2011"},{"first-page":"12","volume-title":"2018 IEEE workshop on monitoring and testing of cyber-physical systems (MT-CPS)","author":"Havelund K","key":"bibr23-00375497241311617"},{"key":"bibr24-00375497241311617","unstructured":"Siemens EDA PAVE360 backplane, https:\/\/eda.sw.siemens.com\/en-US\/ic\/veloce\/ (accessed 19 July 2024)."},{"volume-title":"Feedback systems: an introduction for scientists and engineers","year":"2021","author":"\u00c5str\u00f6m KJ","key":"bibr25-00375497241311617"},{"key":"bibr26-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1007\/1-84628-148-2"},{"volume-title":"Depth of anaesthesia assessment based on time and frequency features of simplified electroencephalogram (EEG)","year":"2015","author":"Li T.","key":"bibr27-00375497241311617"},{"key":"bibr28-00375497241311617","unstructured":"Gomes C, Thule C, Broman D, et al. Co-simulation: state of the art. In: arXiv preprint arXiv:1702.00686, 2017."},{"key":"bibr29-00375497241311617","unstructured":"Gomes C, Thule C, Larsen PG, et al. Co-simulation of continuous systems: a tutorial. In: arXiv preprint arXiv:1809.08463, 2018."},{"volume-title":"Proceedings of the 9th international modelica conference","author":"Blockwitz T","key":"bibr30-00375497241311617"},{"first-page":"17","volume-title":"Modelica conferences","author":"Junghanns A","key":"bibr31-00375497241311617"},{"first-page":"19","volume-title":"International conference on hardware\/software codesign and systems synthesis","author":"Cai L","key":"bibr32-00375497241311617"},{"key":"bibr33-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0117-6"},{"key":"bibr34-00375497241311617","first-page":"90","volume-title":"Runtime verification: 18th international conference, RV 2018","author":"Havelund K","year":"2018"},{"first-page":"46","volume-title":"18th annual symposium on foundations of computer science","author":"Pnueli A.","key":"bibr35-00375497241311617"},{"first-page":"657","volume-title":"Information processing 83, Proceedings of the IFIP 9th world computer congress (ed REA Mason)","author":"Lamport L.","key":"bibr36-00375497241311617"},{"key":"bibr37-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"bibr38-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1145\/2885498"},{"key":"bibr39-00375497241311617","doi-asserted-by":"publisher","DOI":"10.20485\/jsaeijae.10.2_197"},{"key":"bibr40-00375497241311617","unstructured":"Erickson A, Stickley J. UVM-connect primer, https:\/\/verificationacademy.com\/courses\/uvm-connect (2022, accessed 19 July 2024)."},{"key":"bibr41-00375497241311617","first-page":"163","volume-title":"International conference on modelling and simulation for autonomous systems","author":"Temperekidis A","year":"2022"},{"key":"bibr42-00375497241311617","unstructured":"AbdElSalam M, Ali L, Bensalem S, et al Digital Twin prototype for traffic sign recognition of a learning-enabled autonomous vehicle. In: CEUR workshop proceedings. Companion proceedings of the 16th IFIP WG 8.1 working conference on the practice of enterprise modeling and the 13th enterprise design and engineering working conference, Vienna, Austria, 2023, pp. 10\u201321. https:\/\/ceur-ws.org\/Vol-3645\/dte3.pdf"},{"first-page":"304","volume-title":"International conference on runtime verification","author":"Temperekidis A","key":"bibr43-00375497241311617"},{"key":"bibr44-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/j.simpat.2020.102243"},{"key":"bibr45-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/j.simpat.2018.12.005"},{"key":"bibr46-00375497241311617","first-page":"111905","volume":"111","author":"Hansen ST","year":"2023","journal-title":"J Syst Softw"},{"key":"bibr47-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1002\/spe.3305"},{"key":"bibr48-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1016\/j.cmpbup.2021.100014"},{"key":"bibr49-00375497241311617","doi-asserted-by":"publisher","DOI":"10.4018\/978-1-6684-7791-5.ch007"},{"key":"bibr50-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1097\/00000542-200003000-00017"},{"key":"bibr51-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47609-4"},{"key":"bibr52-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1007\/BF01618421"},{"key":"bibr53-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1093\/bja\/81.5.771"},{"key":"bibr54-00375497241311617","doi-asserted-by":"publisher","DOI":"10.1177\/2050312118822629"},{"first-page":"131","volume-title":"Software verification and formal methods for ML-enabled autonomous systems","author":"Bensalem S","key":"bibr55-00375497241311617"},{"first-page":"256","volume-title":"International conference on bridging the gap between AI and reality","author":"Bensalem S","key":"bibr56-00375497241311617"},{"first-page":"249","volume-title":"Verification, model checking, and abstract interpretation","author":"Havelund K","key":"bibr57-00375497241311617"},{"first-page":"148","volume-title":"Runtime verification","author":"Omer M","key":"bibr58-00375497241311617"}],"container-title":["SIMULATION"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/00375497241311617","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/00375497241311617","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/00375497241311617","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,4]],"date-time":"2025-03-04T18:19:16Z","timestamp":1741112356000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/00375497241311617"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,3]]},"references-count":58,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["10.1177\/00375497241311617"],"URL":"https:\/\/doi.org\/10.1177\/00375497241311617","relation":{},"ISSN":["0037-5497","1741-3133"],"issn-type":[{"type":"print","value":"0037-5497"},{"type":"electronic","value":"1741-3133"}],"subject":[],"published":{"date-parts":[[2025,2,3]]}}}