Seminars

Certifying the Concurrent State Table Implementation in a Surgical Robotic System
Yanni Kouskoulas - Johns Hopkins University, Applied Physics Laboratory

09/02/2011, 1:30PM, GHC-6501

Abstract

Robotic surgery has transitioned from a futuristic dream to a modern reality, with most of the growth occurring in the last few years. This talk focuses on the application of formal methods to the reduction of defects in software used to control a surgical robot, called the "Surgical Assistant Workstation" (SAW).

The SAW's architecture depends on optimistic concurrency, allowing it to react to stimuli from the physical world that are not synchronized with its processing. Thus, the system may contain many threads accessing the same data structures in shared memory, without blocking and without the use of locks.

Because testing is not very effective at debugging concurrent algorithms, we applied 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. HLRG improves our ability to analyze concurrent programs by simplifying the process of reasoning about temporal properties of data structures, while fully analyzing the behavior and possible interleavings of threads in concurrent, lock-free algorithms.

Biography

Yanni Kouskoulas works at the Johns Hopkins University Applied Physics Laboratory, as the group Chief Scientist in the Applied Information Sciences Department.

 His most recent research interests revolve around the practical application of mathematical techniques to support different types of reasoning, both in the construction of systems and in their design. This includes the application of formal methods to the construction of reliable systems, and the use of statistical approaches (e.g. Bayesian networks) to encode reasoning processes that help make accurate decisions in the presence of uncertainty.

 He received his Ph.D.(E.E.) from the University of Michigan in 2000, with a background in statistics and electromagnetics.