Modeling and testing a family of surgical robots: an experience report
Modeling and testing a family of surgical robots: an experience report
复制标题
DOI：
10.1145/3236024.3275534
复制
发表时间：
2018-10
期刊：
影响因子：
--
通讯作者：
Niloofar Mansoor;Jonathan A. Saddler;Bruno Vieira Resende e Silva;H. Bagheri;Myra B. Cohen;S. Farritor
中科院分区：
文献类型：
--
作者：
Niloofar Mansoor;Jonathan A. Saddler;Bruno Vieira Resende e Silva;H. Bagheri;Myra B. Cohen;S. Farritor
关键安全应用通常使用可靠性案例来验证指定的属性是不变的，或者证明了一个反示例，以显示如何违反该属性。但是，大多数可靠性案例都考虑到单个产品。同时，已经研究了软件产品线（相关软件产品的家族），其目的是建模可变性和通用性，并为分析和测试构建基于家庭的技术。但是，对于软件产品线建造端到端的可靠性案例（在属性进行了建模，找到一个反示例，然后通过测试将其作为真正的阳性验证）几乎没有工作，而我们不知道一个新兴的安全 - 机器人手术的安全领域。在本文中，我们研究了一个结合硬件和软件的外科机器人家族，并且可配置高度，代表了1300多个独特的机器人。同时，它们被视为关键安全性，应具有相关的可靠性案例。我们进行案例研究，以了解如何将轻量级的正式分析，功能建模和测试结合在一起，以提供端到端管道，以发现潜在的违反重要安全性能的行为。在此过程中，我们了解到，研究界存在一些有趣且开放的挑战，如果解决的话，这将导致更可靠的安全性网络物理系统。
Safety-critical applications often use dependability cases to validate that specified properties are invariant, or to demonstrate a counter example showing how that property might be violated. However, most dependability cases are written with a single product in mind. At the same time, software product lines (families of related software products) have been studied with the goal of modeling variability and commonality, and building family based techniques for both analysis and testing. However, there has been little work on building an end to end dependability case for a software product line (where a property is modeled, a counter example is found and then validated as a true positive via testing), and none that we know of in an emerging safety-critical domain, that of robotic surgery. In this paper, we study a family of surgical robots, that combine hardware and software, and are highly configurable, representing over 1300 unique robots. At the same time, they are considered safety-critical and should have associated dependability cases. We perform a case study to understand how we can bring together lightweight formal analysis, feature modeling, and testing to provide an end to end pipeline to find potential violations of important safety properties. In the process, we learned that there are some interesting and open challenges for the research community, which if solved will lead towards more dependable safety-critical cyber-physical systems.