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.
Guaranteeing the safety of next-generation medical robotics This project has made significant contributions to the development of tools and techniques for the specification and verification of medical robotics. By verification, we are concerned with proving "safety" properties: that medical devices will never cause harm to patients. The project developed flow-driven transducer networks as framework for modeling these systems. Broader impact The motivating device for this explorations effort was a next-generation cancer-treatment device that used MR-guided high-intensity focused ultrasound (MRgHIFU) to thermally ablate tumors without invasive surgery. Helping to speed this device to market brings significant benefits to society as a whole. The development of techniques for verification of cyber-physical-biological systems also has clear positive spillover effects into reliability engineering in related fields including traditional robotics and aerospace. Intellectual merit The MRgHIFU device itself was chosen not only for its high humanitarian potential, but also because it is intellectually challenging to verify its safet propertes. The model of the broader cyber-physical-biological system which includes both device and patient includes highly non-linear bioheat equations such as Pennes. This project invested effort in the sound approximation of such components during model-checking of hybrid automata. Moreover, we provided a path out of the dominant cyberphysical verification paradigm by adapting verification to the dominant engineering paradigm. That is, we focused on developing a verification pipeline that fits with how practicing engineers actually work. Practicing programmers develop code and prototypes first, and tend to think about verification later (if ever). The dominant approach to verification, however, requires programmers to develop models and specification first, to verify these, and then to synthesize code. Our approach extracts models and specifications (as hybrid automata) from code and then proceeds to verify these. This allows programmers and engineers to think and design in the terms they know best. Outcomes Key outcomes from this project included: Development of flow-driven transducer networks for cyber-physical-biological systems. Development of analytic techniques for extracting hybrid automata from device control code. Adaptation of the aforementioned to a scaled-down MRgHIFU system. Model-checking techniques that work on low-level code (including GPUs).
