Certifying the Concurrent State Table Implementation in a Surgical Robotic System (Extended Version)

Last modified: Sat Oct 8 19:53:58 2011 GMT.

Authors

Yanni Kouskoulas
Ming Fu
Zhong Shao
Peter Kazanzides

Abstract

This paper describes the application of formal methods to the reduction of defects in software used to control a surgical robot. We use a recently developed program logic called History for Local Rely/Guarantee (HLRG) to verify that the software implementation behaves according to the intended design. HLRG enables precise description of a system's functionality, its desired behavior, and facilitates rigorous, mathematical proofs about properties of the system via sound inference rules. During this process, we found a subtle bug in the system, corrected it, and were able to formally prove that within the component we were analyzing, with respect to two critical properties, the system had no flaws in its design or implementation.

Published

A shorter summary of this paper appeared in Proc. 3rd Joint Workshop on High Confidence Medical Devices, Software, and Systems & Medical Device Plug-and-Play Interoperability, Chicago, USA. June 2011. [PDF]

colophon