A Formal Approach For Modelling And Analysing Surgical Procedures (Extended Version)

TL;DR

The paper addresses the lack of standardization in surgical procedures by proposing a formal modelling paradigm that treats procedures as security ceremonies, enabling explicit representation of human interactions and potential mistakes. It develops a formal framework consisting of a message algebra, role-scripts, and an execution model, and introduces mutation-based analysis to capture deliberate or inadvertent deviations. Using two stages of a laparoscopic prostatectomy, the authors show how UPPAAL can automatically detect property violations introduced by mutations, providing concrete insights into safety-critical sequences. This approach supports exploring procedure variants and guiding safer, patient-specific planning, with future work aimed at holistic procedure modelling, inclusion of robotic and telesurgical scenarios, and broader mutation types.

Abstract

Surgical procedures are often not "standardised" (i.e., defined in a unique and unambiguous way), but rather exist as implicit knowledge in the minds of the surgeon and the surgical team. This reliance extends to pre-surgery planning and effective communication during the procedure. We introduce a novel approach for the formal and automated analysis of surgical procedures, which we model as security ceremonies, leveraging well-established techniques developed for the analysis of such ceremonies. Mutations of a procedure are used to model variants and mistakes that members of the surgical team might make. Our approach allows us to automatically identify violations of the intended properties of a surgical procedure.

Figures (2)

• Figure 1: MSC of the Cutting Stage
• Figure 2: MSC of the Lateral Dissection Stage