Don't Hammer that Screw... FLS Talk by Ian Mitchell, UBC/CS

Speaker:  Ian Mitchell, Associate Professor, UBC Computer Science

Homepage:  http://www.cs.ubc.ca/~mitchell/

Title:  Don't Hammer that Screw: Formal Safety Analysis for Automated Delivery of Anesthesia contrasted with A Wizard of Oz Study of Shared Control Smart Wheelchairs for Cognitively Impaired Older Adults

Abstract:  In this talk I consider two cyber-physical systems in which it is highly desirable to make guarantees about the safety of proposed automation: feedback control of anesthetic delivery during surgery, and smart wheelchairs for cognitively impaired older adults which provide shared control with collision avoidance. While formal analysis of digital hardware and more recently embedded software has become standard industrial practice in high risk domains, similar analysis of systems evolving in continuous state spaces -- such as those above -- is still an open challenge.

The viability and discriminating kernels are mathematical constructs which can be used to prove the safety of such systems, but existing numerical schemes for approximating them suffer from complexity that is exponential in the state space dimension. In the first part of the talk I show that in some cases scalable classes of algorithms for reachable sets can be used to conservatively approximate the viability or discriminating kernel for possibly high-dimensional systems, demonstrate three implementations using different set representations, and use them to analyze the anesthesia delivery problem.

Whereas the anesthesia system will be used for short periods in an operating room by highly trained professionals, the smart wheelchair will be used in a constantly changing environment over long periods of time by a largely untrained population; consequently, I have set aside formal verification in this domain until we have a better grasp of the design space. In the second part of the talk I will instead describe a wizard of oz study involving cognitively impaired older adults living in long term care facilities in metro Vancouver. Through this study we are seeking to understand the needs and capabilities of the target population and to develop a robots-eye-view of the environment in which they live.

Bio: Ian M. Mitchell completed his doctoral work in engineering at Stanford University in 2002, spent a year as a postdoctoral researcher at the University of California at Berkeley, and is now an Associate Professor of Computer Science at the University of British Columbia. His research interests include development of algorithms and software for nonlinear differential equations, formal verification, and control and planning in cyber-physical and robotic systems.