Collaborative Research: CSR-EHCS(CPS), TM: Teleolog: Certified Software for Medical Robotics

医疗保健占美国国内生产总值的16%。医疗设备形式的技术以及卫生信息学对于提高护理质量和可靠性以及降低成本至关重要。医疗设备越来越多地由软件控制，软件故障往往会危及生命。医疗设备是在物理和虚拟世界中运行的网络物理系统的实例。科学上的挑战是证明组合的网络物理系统对其预期目的是安全的。teleologg项目承担了验证SRI M7机器人远程手术系统安全性的挑战。m7医疗机器人允许外科医生通过操纵主控制器来调动通过网络连接的从站的两个机器人手臂来进行远程手术。该项目采用一种明确的、基于证据的方法，这种方法严重依赖于形式化的验证技术，用于建模和分析电子和物理组件、人类用户、软件控制，以及这些组件之间的交互。认证工作重新设计M7软件，为系统的安全性和弹性开发正式的保证案例。在M7认证过程中开发的模型、格式、工具和认证技术可以应用于其他网络物理系统的认证。该项目还开发了课程材料、案例研究和培训包，用于教育学生设计和分析网络物理系统、循证软件认证和弹性工程。

Healthcare is 16% of the United States Gross Domestic Product. Technology in the form of medical devices as well as health informatics is critical to improving the quality and reliability of care and the reduction of cost. Medical devices are increasingly controlled by software, and failures in the software can often be life-threatening.Medical devices are instances of cyber-physical systems that operate in both the physical and virtual world. The scientific challenge is to demonstrate that the combined cyber-physical system is safe for its intended purpose. The Teleolog project takes on the challenge of certifying the safety of SRI's M7 system for robotic telesurgery. TheM7 medical robot allows a surgeon to perform telesurgery by manipulating the master controls in order to mobilize two robot arms at the slave station connected through a network. The project takes an explicit, evidence-based approach that leans heavily on formal verification technology for modeling and analyzing the electronic and physical components, the human user, the software control, as well as the interaction between these components. The certification effort reengineers the M7 software to develop a formal assurance case for the safety and resiliency of the system. The models, formats, tools, and certification techniques developed during the certification of M7 can be employed in the certification of other cyber-physical systems. The project also develops course material, case studies, and training kits for educating students in the design and analysis of cyber-physical systems, evidence-based software certification, and resiliency engineering.