一句话：将轻量级形式分析、特征建模与测试结合，为高可配置手术机器人产品族构建端到端安全属性违规检测流水线。
安全攸关系统通常需要保障案例来验证属性不变或给出反例，但多数案例针对单一产品；软件产品线研究虽关注可变性与共性建模，却缺少端到端的保障案例，尤其在机器人手术这一新兴安全攸关领域。本文以由软硬件组成、高度可配置、可表示 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.
@inproceedings{paperbot4635,
title = {Modeling and testing a family of surgical robots: an experience report},
author = {Niloofar Mansoor and Jonathan A. Saddler and Bruno Silva and Hamid Bagheri and Myra B. Cohen and Shane Farritor},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3275534}
}