Zeitbeschränktes Model-Checking und verifikationsbewusster Systementwurf für medizinische cyber-physikalische Systeme

• Antragstellerinnen / Antragsteller: Professor Dr.-Ing. Alexander Schlaefer; Professorin Dr. Sibylle Schupp
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik ; Medizinische Physik, Biomedizinische Technik
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 442823242

Medizinische 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.

• DFG-Verfahren: Sachbeihilfen