ScreamaeraX: Modeling Laryngeal Surgical Robots Using Differential Dynamic Logic

McClain, Natalie

Student Work

ScreamaeraX: Modeling Laryngeal Surgical Robots Using Differential Dynamic Logic

Public

Surgical robots are a benefit to both doctors and patients, but carry risks in their usage. Modeling them as cyber-physical systems allows us to formally prove that they will not violate safety conditions. The Super-elastic Continuum Robot for Endoscopic Articulation and Manipulation (SCREAM) is a laryngeal endoscopic robot designed for better reachability within the larynx. We created mathematical models with differential equations of a SCREAM’s motion in progressively more complex ways. We used Differential Dynamic Logic (dL) to prove the safety of these models with a proof assistant. In this, the safety condition was not stabbing the larynx of a patient. We created four models, one in two dimensions and three in three dimensions, each one with a closer to accurate model of motion than the previous.

This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.

Creator