Certifying the Safe Design of a Virtual Fixture …

1 Certifying the Safe Design of a Virtual Fixture ControlAlgorithm for a Surgical Robot Yanni KouskoulasJohns Hopkins UniversityApplied Physics LabDavid RenshawCarnegie Mellon UniversityComputer Science PlatzerCarnegie Mellon UniversityComputer Science KazanzidesJohns Hopkins UniversityDept. of Computer ScienceABSTRACTWe applied quantified differential-dynamic logic (QdL) toanalyze a control algorithm designed to provide directionalforce feedback for a surgical robot. We identified problemswith the algorithm, proved that it was in general unsafe,and described exactly what could go wrong. We then ap-plied QdLto guide the development of a new algorithm thatprovides safe operation along with directional force KeYmaeraD (a tool that mechanizes QdL), we createda machine-checked proof that guarantees the new algorithmis safe for all possible and Subject [Logics and the Meaning of Progams]: Speci-fying and Verifying and Reasoning about Programs; [Artificial Intelligence]: RoboticsKeywordsQuantified differential dynamic logic, medical robotics, for-mal verification1.

2 INTRODUCTIONI magine an operating room in the near future where a sur-geon works diligently to excise a tumor at the base of a pa-tient s skull. The physician might employ newly developedrobotic technology to more clearly visualize the surgery andmore precisely guide the surgical instrument to make theincisions. The ultimate goal: surgery that is safer and moreeffective than before, providing better patient robotic machinery to make this future a reality areslowly being developed, but the systems are complex, and This material is based upon work supported by the Na-tional Science Foundation under NSF CAREER AwardCNS-1054246 and NSF EXPEDITION to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies arenot made or distributed for profit or commercial advantage and that copiesbear this notice and the full citation on the first page.

3 To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a 13,April 8 11, 2013, Philadelphia, Pennsylvania, 2013 ACM 978-1-4503-1567-8/13/04 ..$ be prone to subtle, unexpected errors. It is easy to seehow safety critical such systems are; a bug in the implemen-tation or error in the algorithm that controls the surgicaltool might cause it to make the wrong incision, with devas-tating consequences for the usual approach today for ensuring the safety of com-plex systems is careful Design , thoughtful examination of thealgorithms, and testing. This approach was applied in [16],where the authors built the system and tested the final prod-uct with a surgical procedure on a cadaver.

4 Testing is useful,but only shows the presence of bugs, not their paper describes the analysis of one safety propertyof a skull-base surgery (SBS) robot algorithm, describedin [16], to help ensure its safe and predictable than taking a testing approach, we apply formalmethods to analyze the control algorithm of interest. Thisrigorous analysis ensures that the algorithm and the hard-ware that it controls behave predictably and safely forallpossible inputs, rather than only for finitely many test guarantee we seek is much more comprehensive, and canlead to much safer and more predictable contribution of this work is that it helps explorehow to usefully apply newly developed formal approachesto practical systems.

5 This has two benefits: first, it helpsguide the development and refinement of logics and tools,by identifying what is necessary to put these techniques intowidespread use; second, it helps the development of practi-cal robotic systems by introducing new formal methods asa powerful and maturing set of Design BACKGROUNDThe SBS robot in [16] restricts movement of a surgicaltool to be within a preoperatively defined surgical site (seeFig. 1), provides force feedback to the surgeon, to indicatewhen he or she is approaching these boundaries, and aids infine control of the tool by damping small configure this robot, a surgeon describes an operatingvolume in which to work by a series of planes oriented andpositioned in space, called Virtual fixtures.

6 Each planarboundary extends infinitely, and the intersection of the vol-ume on the safe side of each plane is designed to excludethe areas of anatomy with which the surgeon does not wishto interact. We are considering planar boundaries becausethat is what was used in the original surgery, the surgeon holds the tool, (think of itFigure 1: Cooperatively controlled robot enforcing virtualfixtures to restrict a tool-tip to moving within a small a scalpel, even though it may be another tool with thesame form factor) and applies it to the surgical task at hand,moving it about. The robot is attached to the tool through arigid mechanical linkage, so as the surgeon exerts forces andtorques on the tool, the robot can sense them, and can alsoexert forces on the tool opposing or aiding the surgeon smovements.

7 This interaction between the SBS robot andsurgeon is called cooperative control algorithm provides three behaviors throughdifferent modes of operation: within the center of the safevolume it allows free movement of the tool; close to the sur-face at the edge of the safe volume it creates an increasingresistance to movement that lets the surgeon know that heor she is close to a Virtual boundary; and at the bound-ary it opposes the movement of the tool, preventing it fromcrossing the , this will produce an invisible boundary thatfeels soft or mushy. As the tool pushes towards the bound-ary, the resistance will become progressively firmer; eventu-ally the tool will slow to a stop and stick when it reachesthe limit of its allowed physics of the robot are created by an admittancecontrol Design , a circuit that converts sensed forces andtorques to velocity through a multiplicative factor.

8 If thesurgeon exerts force fon the tool tip, located at Cartesianposition p, the control circuit translates the input force intoa velocity p at the tool tip, given by: p =K( p)G( f) f(1)where overbars indicate vectors, prime indicates a deriva-tive with respect to time, andKandGare 3 3 matrices(when just the position is controlled).A more detailed version of the admittance control equa-tion can be found in [16], but for our purposes this is anadequate the scale factor, which in the ac-tual system is a matrix with non-linear (exponential) termsdescribed in [7]. It allows the surgeon to switch betweenmoving rapidly over large areas, and doing precise work in asmall area with fine control, without interrupting the work-flow.

9 In our study, we simplifyGand consider it a ( p)is a gain term, used to provide force feedback andenforce the Virtual fixtures as described above. Its ele-ments change form abruptly depending on the position ofthe tip of the tool, of movement are defined in terms ofD, a designparameter that indicates a cutoff distance from the bound-ary in its safe direction, as in Fig. 2. In the free region, , the points whose distancedfrom the boundary sat-isfyd>D,Kis the identity matrix. In the slow region,dDVirtual Fixture boundaryFigure 2: The robot determines which mode it is in depend-ing on the distance from the Virtual Fixture 0 d D, the system provides force feedback op-posing movement in proportion to how close the tool is tothe boundary.

10 Past the edges of the boundary in the unsafezone,Kbecomes zero; our tool should not reach past theboundary during normal operation, if our algorithm is the experiments [16], Eqn. 1 was effective in pre-venting the tool from penetrating the safety boundary, buthad the undesirable property that once the tool was nearthe boundary, motion inalldirections was attenuated, in-cluding motions away from the boundary. This led to thedevelopment of a new control law, where in the slow region(0 d D), the velocity of the tool is attenuated by sub-tracting a fraction of the component in the direction normalto the boundary. The amount subtracted is proportional tohow close to the boundary the tool is at any given point.