Formal Verification of Medical CPS

The use of robots in operating rooms improves safety and decreases patient recovery time and surgeon fatigue, but it introduces new potential hazards that can lead to severe injury or even the loss of human life. Thus, safety has been perceived as a crucial system property since the early days by the industry, the medical community, and the regulatory agents. In this article, we discuss the application of the mathematically rigorous technique known as Formal Verification to analyze the safety properties of a laser incision case study, and we assess its safe and predictable operation. Like all formal methods approaches, our analysis has three distinct components: a method to create a model of the system, a language to specify the properties, and a strategy to prove rigorously that the behavior of the model fulfills the desired properties. The model of the system takes the form of a hybrid automaton consisting of a discrete control part that operates in a continuous environment. The safety constraints are formalized as reachability properties of the hybrid automaton model, while the verification strategy exploits the capabilities of the tool Ariadne to address the verification problem and answer the related questions ranging from safety to efficiency and effectiveness.