Time-Constrained Model Checking and Verification-Aware System Design for Medical Cyber-Physical Systems

• Applicants: Professor Dr.-Ing. Alexander Schlaefer; Professorin Dr. Sibylle Schupp
• Subject Area: Software Engineering and Programming Languages ; Automation, Mechatronics, Control Systems, Intelligent Technical Systems, Robotics ; Medical Physics, Biomedical Technology
• Term: since 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 442823242

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.

• DFG Programme: Research Grants