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