Research Article
Model Checking for Robotic Guided Surgery
@INPROCEEDINGS{10.1007/978-3-642-11745-9_1, author={H. M\o{}nnich and J. Raczkowsky and H. W\o{}rn}, title={Model Checking for Robotic Guided Surgery}, proceedings={Electronic Healthcare. Second International ICST Conference, eHealth 2009, Istanbul, Turkey, September 23-15, 2009, Revised Selected Papers}, proceedings_a={E-HEALTH}, year={2012}, month={5}, keywords={Workflow Systems service oriented architecture CORBA knowledge management temporal logic}, doi={10.1007/978-3-642-11745-9_1} }- H. Mönnich
J. Raczkowsky
H. Wörn
Year: 2012
Model Checking for Robotic Guided Surgery
E-HEALTH
Springer
DOI: 10.1007/978-3-642-11745-9_1
Abstract
This paper describes a model checking approach for robotic guided surgical interventions. The execution plan is modeled with a workflow editor as a petri net. The net is then analyzed for correct structure and syntax with XMLSchema. Petri nets allow checking for specific constraints, like soundness. Still the possibility to prove the net with runtime variables is missing. For this reason model checking is introduced to the architecture. The Petri-Net is transformed to the Model Checking language of NuSMV2, an open source model checking tool. Conditions are modeled with temporal logic and these specifications are proved with the model checker. This results in the possibility to prove the correct initialization of hardware devices and to find possible runtime errors. The workflow editor and model checking capabilities are developed for a demonstrator consisting of a KUKA lightweight robot, a laser distance sensor and ART tracking for CO2 laser ablation on bone.
