Medicine-by-wire: Practical considerations on formal techniques for dependable medical systems
Medicine-by-wire: Practical considerations on formal techniques for dependable medical systems
复制标题
线控医疗：可靠医疗系统正式技术的实际考虑
DOI：
10.1016/j.scico.2020.102545
复制
发表时间：
2020
影响因子：
1.3
通讯作者：
Freitas L
中科院分区：
文献类型：
--
作者：
Freitas L
我们认为医学的未来是高度自动化的。通过提高临床医生效率以及新的计算辅助治疗和诊断，可以改善护理服务。在其他安全关键行业，例如航空电子设备和汽车，认证是可靠性驱动的。相比之下，医疗认证是临床试验驱动的，我们认为随着医疗设备和软件复杂性的增加，这将变得越来越成问题。所谓可靠性，我们指的是字典中的概念：可靠和值得信赖。因此，故障要么是通过设计来避免的，要么是在一定程度上负责的。这涉及验证（意图）与验证（结果）问题。尽管正确性并不意味着安全，但根据我们的经验，我们确实相信，正确地争取正确性（验证）的过程确实可以揭示安全性；是否按预期满足要求/假设（验证）。医疗器械试验可以充分保证安全性，如当地监管负担所定义。然而，这种复杂系统的性质意味着某些错误可能无法通过试验检测到，因此需要付出额外的努力来减少错误。我们的目的是，至少对于软件来说，探索方法之间的对比：构建正确性与试验正确性。此外，系统的安全性和有效性水平因不同国家的监管领域而异。一个关键的挑战是如何在工程团队内使用形式化方法的验证任务和系统开发任务之间实现成功的交互，而无需事先了解形式化技术。本文描述了应用形式化技术的实用流程，并以认证前临床前开发期间的三种医疗器械为例进行了说明。这意味着，这些技术不仅适用于现实系统，而且还被开发团队本身采用（即不能完全由正式的专家驱动）。我们展示了在开始、中期和最终发展阶段应用形式主义的差异。特别是，我们描述了潜在的社会技术挑战以及我们如何为每个示例案例开发缓解方法。本文不是关于医疗自动化的通用技术，因为考虑到医疗问题的多样性/动态性，我们认为这是不切实际/可能的。
We see the future of medicine as highly automated. Improvement in care-provision will be achieved by both increased clinician efficiency, as well as new computing assisted treatments and diagnoses. In other safety-critical industries, such as avionics and automotive, certification is dependability-driven. In contrast, medical certification is clinical-trial driven, which we argue will become increasingly problematic with increasing medical device and software complexity. By dependability, we mean the dictionary notion: reliable and trustworthy. Thus, failures are either avoided by design, or are accountable to a measured extent. This touches upon the verification (intent) versus validation (outcome) problem. Even though correctness does not imply safety, we do believe from our experiences that, the process of striving for correctness (verification) done right does shed light on safety; on whether the requirements/assumptions were addressed as intended (validation).Medical device trials can lead to adequate assurances of safety, as defined by the local regulatory burden. Nevertheless, the nature of such complex systems means that certain errors may not be detected by trials and so additional efforts to reduce errors is needed. Our intent is, at least for software, to explore the contrast between approaches: correctness-by-construction versus correct-by-trial. Additionally, these levels of safety and effectiveness of systems vary across regulatory domains in different countries. A key challenge is how to achieve a successful interaction between verification tasks using formal methods and system development tasks within engineering teams without prior knowledge of formal techniques.This paper describes a pragmatic process for the application of formal techniques, which is illustrated for three medical devices during pre-clinical development prior to certification. That means, the techniques are not only applied to realistic systems, but are also taken up by development teams themselves (i.e.cannot be entirely formal expert driven). We demonstrate differences in applying formalisms at the start, midpoint and final development stages. In particular, we describe the underlying socio-technical challenges and how we developed mitigation methods for each exemplar case. This paper is not about a general technique for medical automation, as we do not believe this is practical/possible given the varied/dynamic nature of medical problems.
登录
查看更多内容
DOI：
--
发表时间：
1972
期刊：
影响因子：
--
作者：
P. Naur
通讯作者：
P. Naur
使用纽卡斯尔婴儿透析和超滤系统 (Nidus) 对体重 <8 公斤的婴儿进行血液透析：与腹膜透析和传统血液透析的比较
DOI：
--
发表时间：
2014
期刊：
Pediatric nephrology (Berlin, West)
影响因子：
--
作者：
M. Coulthard;J. Crosier;C. Griffiths;Jon H. Smith;M. Drinnan;Michael Whitaker;R. Beckwith;J. Matthews;P. Flecknell;H. Lambert
通讯作者：
H. Lambert
Escher Verification Studio Perfect Developer 和 Escher C Verifier
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Judith Carlton;David Crocker
通讯作者：
David Crocker
盒式结构开发方法与CSP相结合进行软件开发
DOI：
--
发表时间：
2005
期刊：
International Workshop Automated Verification Critical Systems
影响因子：
--
作者：
Philippa J. Hopcroft;G. Broadfoot
通讯作者：
G. Broadfoot
DO-178C/ED-12C 航空电子行业新软件标准：目标、变化和挑战
DOI：
--
发表时间：
2012
期刊：
影响因子：
--
作者：
Sven Nordhoff
通讯作者：
Sven Nordhoff