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.
QiQTaoFHuT, et al. Enabling technologies and tools for digital twin. J Manuf Syst2021; 58: 3–21.
5.
JonesDSniderCNassehiA, et al. Characterising the digital twin: a systematic literature review. CIRP J Manuf Sci Technol2020; 29: 36–52.
6.
SchleichBAnwerNMathieuL, et al. Shaping the digital twin for design and production engineering. CIRP Ann2017; 66: 141–144.
7.
RasheedASanOKvamsdalT.Digital twin: values, challenges, and enablers from a modeling perspective. IEEE Access2020; 8: 21980–22012.
8.
SharmaAKosasihEZhangJ, et al. Digital twins: state of the art theory and practice, challenges, and open research questions. J Ind Inf Integr2022; 30: 100383.
9.
GrievesMVickersJ.Digital twin: mitigating unpredictable, undesirable emergent behavior in complex systems. In: KahlenF-JFlumerfeltSAlvesA (eds) Transdisciplinary perspectives on complex systems: New findings and approaches. Cham: Springer, 2017, pp. 85–113.
10.
BruynseelsKSantoni de SioFVan den HovenJ.Digital twins in health care: ethical implications of an emerging engineering paradigm. Front Genet2018; 9: 31.
11.
TaoFChengJQiQ, et al. Digital twin-driven product design, manufacturing, and service with big data. Int J Adv Manuf Technol2018; 94: 3563–3576.
12.
ChaseJGPreiserJCDicksonJL, et al. Next-generation, personalised, model-based critical care medicine: a state-of-the-art review of in silico virtual patient models, methods, and cohorts, and how to validate them. Biomed Eng Online2018; 17: 1–29.
13.
BruhnJMylesPSSneydR, et al. Depth of anaesthesia monitoring: what’s available, what’s validated and what’s next?Br J Anaesth2006; 97: 85–94.
14.
RaniDDHarsoorS.Depth of general anaesthesia monitors. Indian J Anaesth2012; 56: 437.
15.
MathurSPatelJGoldsteinS, et al. Bispectral index. St. Petersburg, FL: Statpearls Publishing, 2023.
16.
MusizzaBRibaricS.Monitoring the depth of anaesthesia. Sensors2010; 10: 10896–10935.
17.
KissinI.Depth of anesthesia and bispectral index monitoring. Anesth Analg2000; 90: 1114–1117.
18.
ShortCEBufalariA.Propofol anesthesia. Vet Clin North Am Small Anim Pract1999; 29: 747–778.
19.
PanditJAndradeJBogodD, et al. 5th National Audit Project (NAP5) on accidental awareness during general anaesthesia: summary of main findings and risk factors. Br J Anaesth2014; 113: 549–559.
20.
PanditJAndradeJBogodD, et al. 5th National Audit Project (NAP5) on accidental awareness during general anaesthesia: protocol, methods, and analysis of data. Br J Anaesth2014; 113: 540–548.
21.
KarerGNovak-JankovičVStecherA, et al. Modelling of BIS-Index dynamics for total intravenous anesthesia simulation in Matlab-Simulink. IFAC-PapersOnLine2018; 51: 355–360.
22.
BasuABensalemSBozgaM, et alRigorous system design: the BIP approach. In: International doctoral workshop on mathematical and engineering methods in computer science, Znojmo, Czech Republic, 25–28 October2011. Cham: Springer, pp. 1–19.
23.
HavelundKPeledDUlusD.DejaVu: a monitoring tool for first-order temporal logic. In: 2018 IEEE workshop on monitoring and testing of cyber-physical systems (MT-CPS), Porto, Portugal, 10–13 April 2018. New York: IEEE, pp. 12–13.
LiT.Depth of anaesthesia assessment based on time and frequency features of simplified electroencephalogram (EEG). PhD Thesis, University of Southern Queensland, 2015.
28.
GomesCThuleCBromanD, et al. Co-simulation: state of the art. In: arXiv preprint arXiv:1702.00686, 2017.
29.
GomesCThuleCLarsenPG, et al. Co-simulation of continuous systems: a tutorial. In: arXiv preprint arXiv:1809.08463, 2018.
30.
BlockwitzTOtterMAkessonJ, et alFunctional mockup interface 2.0: the standard for tool independent exchange of simulation models. In: Proceedings of the 9th international modelica conference, München, 3–5 September 2012.
31.
JunghannsAGomesCSchulzeC, et al. The functional mock-up interface 3.0-new features enabling new applications. In: Modelica conferences, 2021, pp. 17–26.
32.
CaiLGajskiD. Transaction level modeling: an overview. In: International conference on hardware/software codesign and systems synthesis, Newport Beach, CA, 1–3 October 2003. New York: IEEE, pp. 19–24.
33.
HavelundKRosuG.Efficient monitoring of safety properties. Int J Softw Tools Technol Transf2004; 6: 158–173.
34.
HavelundKPeledD.Runtime verification: from propositional to first-order temporal logic. In: Runtime verification: 18th international conference, RV 2018, Limassol, Cyprus, 10–13 November 2018. Cham: Springer, 2018, pp. 90–112.
35.
PnueliA.The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, RI, 31 October–1 November 1977. New York: IEEE Computer Society, pp. 46–57.
36.
LamportL.What good is temporal logic? In: Information processing 83, Proceedings of the IFIP 9th world computer congress (ed REA Mason), Paris, 19–23 September 1983. London: North-Holland/IFIP, pp. 657–668.
37.
AlpernBSchneiderFB.Defining liveness. Inf Process Lett1985; 21: 181–185.
38.
NouriABozgaMMolnosA, et al. Astrolabe: a rigorous approach for system-level performance modeling and analysis. ACM Trans Embedded Comput Syst2016; 15: 1–26.
39.
AbdElSalamMKhalilKStickleyJ, et al. Verification of advanced driver assistance systems and autonomous vehicles with hardware emulation-in-the-loop: a case study with multiple ECUs. Int J Automotive Eng2019; 10: 197–204.
TemperekidisAKekatosNKatsarosP, et alTowards a digital twin architecture with formal analysis capabilities for learning-enabled autonomous systems. In: International conference on modelling and simulation for autonomous systems, Prague, Czech Republic, 20–21 October2022. Cham: Springer, pp. 163–181.
42.
AbdElSalamMAliLBensalemS, et alDigital 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–21. https://ceur-ws.org/Vol-3645/dte3.pdf
43.
TemperekidisAKekatosNKatsarosP.Runtime verification for FMI-based co-simulation. In: International conference on runtime verification, Tbilisi, Georgia, 28–30 September 2022. Cham: Springer, pp. 304–313.
44.
HatledalLIChuYStyveA, et al. Vico: an entity-component-system based co-simulation framework. Simul Model Pract Theory2021; 108: 102243.
45.
ThuleCLausdahlKGomesC, et al. Maestro: the INTO-CPS co-simulation framework. Simul Model Pract Theory2019; 92: 45–61.
46.
HansenSTThuleCGomesC, et al. Co-simulation at different levels of expertise with Maestro2. J Syst Softw2023; 111: 111905.
47.
GilSMikkelsenPHGomesC, et al. Survey on open-source digital twin frameworks–A case study approach. Softw Pract Exp2024; 54: 929–960.
48.
ShengliW.Is human digital twin possible?Comput Methods Programs Biomed Update2021; 1: 100014.
49.
CoşgunAE.Digital twin and human digital twin for practical implementation in industry 5.0. In: Global perspectives on robotics and autonomous systems: development and applications. Hershey, PA: IGI Global, 2023, pp. 168–183.
50.
ScuttlerJIhmsenH.Population pharmacokinetics of propofol. Anesthesiology2000; 92: 727–738.
51.
AbsalomARMasonKP.Total intravenous anesthesia and target controlled infusions. Cham: Springer, 2017.
52.
SiglJCChamounNG.An introduction to bispectral analysis for the electroencephalogram. J Clin Monit1994; 10: 392–404.
53.
ThorntonCSharpeR.Evoked responses in anaesthesia. Br J Anaesth1998; 81: 771–781.
54.
van der SluijsAFvan Slobbe-BijlsmaERGoossensA, et al. Reducing errors in the administration of medication with infusion pumps in the intensive care department: a lean approach. SAGE Open Med2019; 7: 2050312118822629.
55.
BensalemSChengC-HHuangX, et al. Formal specification for learning-enabled autonomous systems. In: Software verification and formal methods for ML-enabled autonomous systems, Haifa, Israel, 31 July–1 and 11 August 2022. Cham: Springer, pp. 131–143.
56.
BensalemSKatsarosPNičkovićD, et al. Continuous engineering for trustworthy learning-enabled autonomous systems. In: International conference on bridging the gap between AI and reality, Crete, Greece, 23–28 October 2023. Cham: Springer, pp. 256–278.
57.
HavelundKKatsarosPOmerM, et al. TP-DejaVu: combining operational and declarative runtime verification. In: Verification, model checking, and abstract interpretation, London, 15–16 January 2024. Cham: Springer, pp. 249–263.
58.
OmerMPeledD. Runtime verification prediction for traces with data. In: Runtime verification, Thessaloniki, Greece, 3–6 October 2023. Cham: Springer, pp. 148–167.
