"Automated needle steering in soft tissue" is an open problem in both surgery robotics and formal verification. Challenges that are common to both fields include the interaction between needle and tissue, which depends on the coupled effects of needle deflection, friction and force, and tissue deformation; navigation, collision avoidance, and path planning, which are faced with inhomogeneous, partially unknown tissue; and also adaptive updates and feedback, which are required in real time.
This website makes available artifacts from projects for different subproblems of the formal verification of automated needle steering: formal models of needle-issue interaction; new techniques for the simulation and model checking of needle-tissue interaction as well as analyses and synthesis of safe paths; software and experimental data; publications and instructional videos. Much of the theoretical contributions are based on the theories of timed automata and timed games, which are frameworks for simple, yet rigorous descriptions of continuous-time hybrid systems with restricted first-order differential equations.
Partners:
Institute of Medical Technology and Intelligent Systems
[https://mtec.et8.tuhh.de]
Additional partners:
Institute for Continuum and Material Mechanics
[https://www.tuhh.de/icm/en/about-us.html],
Institute for Structural Dynamics
[https://cgi.tu-harburg.de/~dynwww/cgi-bin/]
Funding:
i3M4 WTM i3-LAB, DFG SCHU 2479/9-1
We thank the authors of Uppaal and its variants Uppaal-SMC and Uppaal-Stratego, which are used in a number of experiments and form the basis of several extensions.
