Certifying the Concurrent State Table Implementation in a Surgical Robotic System (Extended Version)
Last modified: Sat Oct 8 19:53:58 2011 GMT.
AbstractThis 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.
Copyright © 1996-2021 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science