Safety-Oriented Hybrid Verification of Medical Robotics

Abstract:

Motivation and goal The whole-system design and modeling of complex medical robotics in- volves analog sensors and actuators; discrete software controllers; piecewise, non-linear, discon- tinuous biological tissues/media; and probabilistic human administrators.

In the best case, the failure of such systems risks limb. In the worst, life.

The goal of our project is to explore and investigate paradigms for the whole-system design, modeling and formal verification of cyber-physical-biological systems.

Motivating application To ground this project in practice, the motivating application is MRgHIFU: an MR-guided robotic surgeon wielding a high-frequency ultrasound as a scalpel for noninvasive surgical ablation of cancerous tissue. We selected this system because (1) it has clear humani- tarian broader impacts, (2) it has demanding clinical safety requirements acting as a barrier to formal approval and clinical adoption, and (3) modeling and verification of the system and those requirements requires a complex synthesis of components with nonlinear behavior.

Research objectives Our specific research objective is the exploration and investigation of paradigms for the whole-system design, modeling and verification of cyber-physical-biological systems.

Scientific directions We are developing and investigating flow-driven-transducer networks as a paradigm for the design and modeling of cyber-physical-biological systems. Such networks formally model heterogenous systems with discrete, continuous and probabilistic components. Specific approaches being investigated include hybrid and timed automata, abstract-interpretive inference thereof and model-checking techniques for nonlinear differential equations.

Techniques and findings Findings to date include (1) a prototype core calculus for MATLAB— λM —to model higher-order controllers; (2) a formal framework for flow-driven transducer net- works; (3) abstract interpretive methods for hybrid specification synthesis; (4) probabilistic au- tomata to model healthcare workers; (5) characterizations of safety and liveness for cyber-physical- biological systems; and (6) an algorithm for synthesis of hybrid automata from higher-order con- trol code.

Keywords MRgHIFU, medical robotics, tumor ablation, hybrid systems, flow networks, model- checking, abstract interpretation, hybrid automata, formal verification

Award ID: 1035658

 

  • CPS Domains
  • Hybrid Models
  • Medical Devices
  • Control
  • Modeling
  • Health Care
  • Robotics
  • Validation and Verification
  • Foundations
  • National CPS PI Meeting 2012
  • 2012
  • Poster
  • Academia
  • CPS PI MTG 12 Posters & Abstracts
Submitted by Matthew Might on