在 Uppaal 中建模 R$^3$ 针 steering

Sascha Lehmann; Antje Rogalla; Maximilian Neidhardt; Anton Reinecke; Alexander Schlaefer; Sibylle Schupp

doi:10.4204/EPTCS.355.4

在 Uppaal 中建模 R$^3$ 针 steering

系统与控制 2022-03-21 v1 形式语言与自动机理论计算机科学与博弈论系统与控制

作者: Sascha Lehmann , Antje Rogalla , Maximilian Neidhardt , Anton Reinecke , Alexander Schlaefer , Sibylle Schupp

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

医疗网络物理系统具有安全关键性,因此需要在其正确行为方面进行持续验证,因为运行时的系统故障可能导致严重的(甚至致命的)人身伤害。然而,创建可验证模型常与其他应用需求相冲突,最显著的是数据精度和模型准确性,因为高效的模型检测倾向于离散数据(而非连续数据)和抽象模型以缩减状态空间。在本文中,我们处理软组织中绕过潜在障碍的医疗针 steering 任务。我们设计了针运动的可验证模型(在 Uppaal Stratego 中实现)以及用于在线针 steering 的嵌入该模型的框架。我们通过限制数据类型(在需要时从 R^3 缩减为 Z^3)以及运动和环境模型(缩减允许的局部动作和全局路径集合)来缓解该冲突。在实验中,我们成功单独应用静态模型,以及在环境复杂度不同且包含虚拟和真实针设置的场景中应用动态框架,根据场景和针的不同,最多可达 100% 的目标被抵达。

关键词

医疗网络物理系统针 steering Uppaal 可验证模型模型检测软组织

引用

@article{arxiv.2203.09884,
  title  = {Modeling R$^3$ Needle Steering in Uppaal},
  author = {Sascha Lehmann and Antje Rogalla and Maximilian Neidhardt and Anton Reinecke and Alexander Schlaefer and Sibylle Schupp},
  journal= {arXiv preprint arXiv:2203.09884},
  year   = {2022}
}

备注

In Proceedings MARS 2022, arXiv:2203.09299

在 Uppaal 中建模 R$^3$ 针 steering

摘要

关键词

引用

备注

相关论文