论文标题
建模r $^3 $在Uppaal中转向
Modeling R$^3$ Needle Steering in Uppaal
论文作者
论文摘要
医疗网络物理系统是安全至关重要的，因此需要持续验证其正确的行为，因为运行时间内的系统故障可能会造成严重（甚至是致命的）个人损害。但是，创建可验证的模型通常与其他应用程序需求发生冲突，最值得注意的是数据精度和模型准确性，因为有效的模型检查会促进离散数据（超过连续）和摘要模型，以减少状态空间。在本文中，我们在潜在障碍物周围的软组织中处理医疗针头的任务。我们设计了一个可验证的针头运动模型（在Uppaal Stratego中实现），并设计了一个嵌入在线针头转向模型的框架。我们通过对两种数据类型施加界限来减轻冲突，在需要时从r^3减少到z^3，以及运动和环境模型，从而减少了允许的本地动作和全局路径。在实验中，我们成功地仅应用静态模型，以及在不同环境复杂性以及虚拟和真实针头设置的情况下的动态框架，根据场景和针头，达到了100％的目标。
Medical cyber-physical systems are safety-critical, and as such, require ongoing verification of their correct behavior, as system failure during run time may cause severe (or even fatal) personal damage. However, creating a verifiable model often conflicts with other application requirements, most notably regarding data precision and model accuracy, as efficient model checking promotes discrete data (over continuous) and abstract models to reduce the state space. In this paper, we approach the task of medical needle steering in soft tissue around potential obstacles. We design a verifiable model of needle motion (implemented in Uppaal Stratego) and a framework embedding the model for online needle steering. We mitigate the conflict by imposing boundedness on both the data types, reducing from R^3 to Z^3 when needed, and the motion and environment models, reducing the set of allowed local actions and global paths. In experiments, we successfully apply the static model alone, as well as the dynamic framework in scenarios with varying environment complexity and both a virtual and real needle setting, where up to 100% of targets were reached depending on the scenario and needle.
