Design and Model-Based Safety Verification of a Volitional Sit-Stand Controller for a Powered Knee-Ankle Prosthesis

摘要 坐-站转换，即个体站立或坐下的动作，是一个重要的决定因素 也是福尔斯的共同来源。使用标准被动假肢的单侧截肢者 由于肌肉和关节的不对称性，他们在声音之间表现出更大的挑战 和截肢的两侧，往往导致衰弱的背部疼痛。动力膝踝假肢可以产生 足够的扭矩，以在坐立转换期间提供有意义的帮助，并且可以满足设计标准，例如 在截肢侧产生与健全侧匹配的平滑运动。这些假肢的控制器 可以被设计成允许用户驱动腿的控制。然而，高扭矩的产生并不直接 用户的命令会增加风险。这是特别值得关注的，因为这些腿必须 在受控的实验室环境之外采用。因此，任何动力假体必须证明符合设计要求， 和安全标准。虽然安全关键的医疗设备，如起搏器，受到广泛的影响， 测试和验证程序，在动力修复领域没有商定的标准， 定义和衡量安全。以前关于坐立控制器的工作只集中在测量有限的数量上 关于少数受试者的一个设计标准的结果，不保证 安全为代价的被称为形式化验证的一组技术提供了强大的工具来推理行为 由相互作用的机械、软件和生物模块组成的系统。给定一个 系统，形式验证允许我们在无限的可能性范围内探测系统的行为， 在典型的测试会话期间，无法在实验室中复制。这些方法可以指导现实世界 测试，并提醒系统设计人员有问题的执行区域。在这个项目中，我建议申请 设计具有可证明安全性的坐-站转换的意志控制器的形式验证技术 使用基于物理的模型和新的安全数学公式来保证。 密歇根大学机器人学院是美国同类学院中的顶尖学院之一， 理想的环境和基础设施，以成功完成这项研究。机器人研究所步态 实验室拥有动力假肢研究所需的所有必要设备，包括两台最先进的 假肢，并获得先进的计算资源，如五大湖高性能 计算集群。Gregg和Ozay博士已经证明了与本项目目标相关的专业知识，并将 提供指导，指导我的研究，我的培训和我的职业目标的实现。

ABSTRACT Sit-stand transitions, the motions executed by individuals to stand up or sit down, are an important determinant of overall mobility and a common source of falls. Unilateral amputees using standard passive prostheses are further challenged by sit-stand transitions due to muscle and joint asymmetries they exhibit between the sound and amputated sides, often resulting in debilitating back pain. Powered knee-ankle prostheses can produce enough torque to assist meaningfully during sit-stand transitions and can meet design criteria such as producing smooth motion on the amputated side that matches the sound side. Controllers for these prostheses can be designed to allow user-driven control of the leg. However, the production of high torques not directly commanded by the user comes with increased risks. This is of particular concern because these legs must be adopted outside of controlled lab environments. Thus, any powered prosthesis must demonstrably meet design and safety criteria. While safety-critical medical devices, such as pacemakers, are subjected to extensive testing and validation procedures, there is no agreed-upon standard in the powered prosthetics field for how to define and measure safety. Prior work on sit-stand controllers has focused only on measuring a limited number of outcomes with respect to one design criterion on a small number of subjects, providing no guarantees about safety. The set of techniques known as formal verification provides powerful tools to reason about the behavior of systems that are composed of interacting mechanical, software, and biological modules. Given a model of a system, formal verification allows us to probe the system’s behavior over an infinite range of possibilities that cannot be replicated in the lab during a typical testing session. These methods can then guide real-world testing, and alert system designers to problematic regions of execution. In this project, I propose to apply formal verification techniques to design a volitional controller for sit-stand transitions with provable safety guarantees, using physics-based models and novel mathematical formulations of safety. The University of Michigan Robotics Institute is one of the top institutes of its kind in the US and provides an ideal environment and infrastructure for the successful completion of this research. The Robotics Institute gait lab has all of the necessary equipment needed for powered prosthesis research, including two state-of-the-art prosthetic legs, and access to advanced computational resources such as the Great Lakes high performance computing cluster. Drs. Gregg and Ozay have proven expertise relevant to the aims of this project, and will provide mentorship that will guide my research, my training, and the attainment of my career goals.