CPS: Medium: Safety-Oriented Hybrid Verification for Medical Robotics

这项研究的目的是开发设计、实施和验证医疗机器人的方法和工具。该方法是捕获具有网络、物理和生物组件的系统的计算工作流，验证该工作流，并从工作流模型综合系统。本研究的聚焦应用是MRI引导下的高频超声肿瘤消融术。MRI引导的超声肿瘤消融术带来了超出当前验证技术范围的挑战。医学充满了高度非线性的生物系统，这使得它们处于数学上严格的正确性检查和验证的前沿。例如，在这项研究中，确保正在接受治疗的癌症患者的安全性将需要对照彭斯生物热方程进行验证，彭斯生物热方程是一个包含数十个环境因素的非线性微分方程式。这项研究解决了这种复杂性，使用抽象层来高效、准确和安全地近似系统的每个组件的行为。为了确保控制器的忠实实现，本研究将研究直接从验证后的模型通过构造的方式正确地综合控制代码。该项目将帮助开发最合适的一系列正式方法，以应对医疗机器人领域的安全和正确性挑战。它通过提出弥合网络要素和实体要素之间差距的正式技术，直接处理方案和方案的方法和工具议程。它将通过新的研讨会、工作坊和课程培训跨学科领域的人才。最后但同样重要的是，该项目将对社会福祉产生直接的人道主义影响。

The objective of this research is to develop methods and tools for designing, implementing and verifying medical robotics. The approach is to capture the computational work-flow of systems with cyber, physical and biological components, to verify that work-flow and to synthesize systems from the work-flow model. The focusing application of this research is MRI-guided, high-frequency ultrasonic tumor ablation. MRI-guided ultrasonic tumor ablation poses challenges beyond the scope of current verification techniques. Medicine is filled with highly non-linear biological systems, which puts them at the frontier of mathematically rigorous correctness checking and verification. For instance, in this research, guaranteeing the safety of a cancer patient undergoing treatment will require verifying against Pennes bioheat equation, a non-linear differential equation with dozens of environmental factors. This research tackles such complexity using tiers of abstractions to efficiently, precisely and safely approximate the behavior of each component of a system. To ensure a faithful implementation of controllers, this research will investigate synthesizing the control code directly from the verified model in a correct by construction manner. The project will help develop the most appropriate family of formal methods for handling the safety and correctness challenges in the area of medical robotics. It directly addresses the CPS agenda of methods and tools by proposing formal techniques that bridge the gap between the cyber and physical elements. It will train manpower in cross-disciplinary areas through new seminars, workshops and courses. And, last but not least, the project will make a direct humanitarian impact on the well-being of society.