I'm currently working to formalize the surgical process of removing a tumor from the pituitary gland. The final goal is to have a formalization of the procedure from which a verifiably correct computer simulation can be built and used to train young surgeons or provide an objective assessment of their skill. My goal is also, through this work, to produce a framework/process in/by which any generic surgical procedure can be formalized.

The current working version of the formalized pituitary process is a step machine based on the activation of various signals. Each step of the procedure has:

• A set of precondition signals that must be active before the step can be entered
• A set of triggerd signals that, if certain circumstances hold true, will be activated or deactivated while the procedure is in this step
• A set of exit paths, each of which is composed of:
  • A list of exit conditions, in the form of signals that must be active
  • A step to move into (exiting the current one) if all exit conditions are true
  In steps with more than one exit path, the paths are prioritized in the order in which they are listed.
• A set of haptic constraints that are active in the simulation for the duration of the current step