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. The M7 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.
