Introduction
The Harmonics Mover software provides strategic decisions in online environments that depend on safety and other verifiable properties. In scenarios that change fast but need to make decisions confidently, our solution is to use Online Model Checking,
combining dependability of formal methods with dynamic responses from defined, rule-based strategies.
The current main application involves the problem of robotic radiation therapy, which we collaborated on together with the Institute of Medical Technology and Intelligent Systems.
Here, a patient is treated via a robot that must deliver radiation doses to a precise location in the body. However, the robot must compensate for the respiratory motion of the patient, which makes the successful and timely delivery of the does challenging. Our solution allows us to deliver the therapy faster than the reference approach while keeping safety concerns.
We describe here the overall workflow and how we implemented it as our Harmonics Mover software. We present the results and products of that research.
