2023-06-252025-02-052023-06-25https://hdl.handle.net/11420/15677Medizinische cyber-physikalische Systeme (MCPS) stehen vor zwei Herausforderungen: der Komplexität des patientenindividuellen Systems "Mensch" und des potenziell hohen Risikos. Je autonomer ein System ist, desto wichtiger ist die Adaption an den internen Zustand von Patienten und Patientinnen. Mit zunehmendem Interesse an autonomeren MCPS und deren potentiellen Vorteilen gewinnt auch der sichere Betrieb dieser Systeme an Bedeutung. Formal bewiesene und gleichzeitig nachvollziehbare Garantien für ein sicheres Systemverhalten könnten die Akzeptanz solcher MCPS in der klinischen Routine erhöhen.Formale Methoden und insbesondere die Technik des Model-Checking können diese Garantien im Prinzip geben. Allerdings läuft das klassische Model-Checking "offline" und erwartet vollständige Modelle; die Modelle physiologischer Prozesse sind dagegen komplex und unvollständig. Verlagert man die Verifikation von "offline" zu "online", sind vollständige Modelle nicht länger notwendig, denn man kann mit Sensordaten, die zur Laufzeit zur Verfügung stehen, fehlende Werte ersetzen. Für Zeitfenster in der nahen Zukunft wird es dadurch möglich, formal belastbare Garantien zu geben. Weiter hat ein verifikationsbewusstes MCPS dann die Chance, sich nicht nur an Patienten und Patientinnen, sondern auch an die Verifikation selbst zu adaptieren. Für das Model-Checking ändert sich dabei jedoch, dass es nun zeitlich beschränkt ablaufen muss.In diesem Vorhaben nehmen wir an, dass Model-Checking und MCPS eine Regelschleife bilden. Wir untersuchen, wie die wechselseitige Abhängigkeit ausgenutzt werden kann, um Model-Checking auch dort zu ermöglichen, wo Zeitschranken oder die Komplexität der Modelle der formalen Verifikation eigentlich entgegenstehen. In der Regelschleife kann das Model-Checking Eigenschaften, die sicherheitskritisch sind, priorisieren und andere Eigenschaften gegebenenfalls etwa mit geringer Konfidenz prüfen. Im Gegenzug kann das MCPS im nächsten Schritt entscheiden, ob es sein eigenes Verhalten anpasst (z.B. Geschwindigkeit reduziert), um eine "gründlichere" Verifikation zu ermöglichen.Wir entwickeln Methoden zur Analyse der Verifikationszeit, die zwischen Genauigkeit und Kosten abwägen können. Weiter definieren wir eine domänenspezifische Sprache, mit der die Priorisierung und Abstraktion von logischen Eigenschaften unterstützt und das Model-Checking konfiguriert werden kann. Der Entwurf eines verifikationsbewussten MCPS muss Model-Checking fest integrieren und die zusätzliche Interaktion in Echtzeit und synchronisiert umsetzen. Wir untersuchen Systemadaptation als multikriterielles Optimierungsproblem mit dem Ziel maximaler Systemeffizienz bei gleichzeitiger Garantie der Patientensicherheit. Alle Methoden entwickeln und evaluieren wir im Rahmen von zwei realen Anwendungsszenarien, der bewegungskompensierten Strahlentherapie und der robotischen Nadelplatzierung.Medical cyber-physical systems (MCPS) face two challenges: the complexity of the patient and a potentially high risk. Particularly, more autonomous systems often have to adapt to the patient's internal state. While there is growing interest in studying possible benefits of smarter and more autonomous MCPS for patients and physicians, safe operation is one key concern. Having rigorous and comprehensible guarantees for safe system behavior could therefore raise the acceptance of such systems in clinical practice.Formal methods and particularly the technique of model checking can in principle provide such guarantees. But classical model checking runs offline and requires complete models up-front; yet, models of physiological processes are complex and incomplete. If one shifts verification from offline to online, complete models are no longer required because one can use sensor data available at run time to fill in missing values so, that it becomes possible to give formal guarantees at least for relevant time windows in the near future. An MCPS aware of the verification thus has the chance to adapt, at run time, not only to the patient, but also to the verification itself. The online model checker, however, now becomes constrained by the time window available for verification.In this proposal we assume that model checker and MCPS form a control loop that executes repeatedly under (soft or hard) time constraints and investigate how their mutual dependency can be exploited to enable model checking where otherwise model complexity or time constraints would prevent formal verification. Embedded in a feedback loop, the model checker may need to prioritize critical properties over weaker guarantees where, e.g., lower confidence is acceptable. Considering the model checker's output, the MCPS may adapt to allow for "sufficient" model checking, e.g., by changing its speed.We develop a verification-time analysis that can weigh between precision and overhead. Further, we introduce a domain-specific language supporting the prioritization and abstraction of logical properties, to configure model checking accordingly. Verification-aware design of MCPS implies a tight integration and interaction with model checking in a real-time and synchronized fashion. We study system adaptation as a multi-criteria optimizing problem of maximizing system efficiency while maintaining patient safety. The methods are developed and evaluated in the context of two actual application scenarios: motion compensated radiation therapy and robotic needle placement.