Models

Networks of timed automata for needle-tissue interaction

A network of 3 Uppaal models (see below) specifying safety and termination conditions, needle motion, and needle-tissue interaction.

Models for Formal Analysis of Real Systems (MARS)

MARS repository

  • Synthesizing strategies for needle steering in gelatin phantoms
  • Modeling R3 needle steering in Uppaal