Home | english  | Impressum | KIT
Photo von Heinz Wörn

Prof. Dr.-Ing. Dr. h.c. Heinz Wörn

Professor im Ruhestand
Tel.: +49 721 608-44006
Fax: +49 721 608-47141
woernWby0∂kit edu


Zur Person

Professor Wörn studierte Elektrotechnik an der Universität Stuttgart und promovierte dort am Institut für Werkzeugmaschinen mit seiner Arbeit zu dem Thema "Mehrprozessorsteuerungssystem für Werkzeugmaschinen mit standartisierten Schnittstellen". Im Anschluss arbeitete er bei KUKA Schweißanlagen und Roboter GmbH, wo er eine leitende Stellung in Forschung und Entwicklung inne hatte. Professor Wörn ist ein international anerkannter Experte für Roboter und Automation. Seine Erfahrung umfasst Roboteranwendungen, Robotersteuerungen und Sensoren für Roboter, sowie deren Programmmierung und Simulation. Seit 1997 leitet er das Institut für Prozessrechentechnik, Automation und Robotik der Universität Karlsruhe als Professor für "Komplexe Systeme in Automation und Robotik".

Forschungsgebiete

  • Planung, Programmierung, Steuerung, Diagnose und Sensorsysteme für Industrieroboter
  • Autonome, mobile Roboter, Mikroroboter, Serviceroboter, Teleroboter, Autonome Fahrzeuge
  • Planung und Simulation von Anlagen und Fabriken
  • Roboter- und sensorgestützte Chirurgie
  • Mikromontage
  • Modellierung komplexer Systeme in Produktion und Medizin

Model Checking for Robotic Guided Surgery

AutorHolger Mönnich, Jörg Raczkowsky, Heinz Wörn
Jahr2010
Veröffentlicht inElectronic Healthcare
KurzfassungThis 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.
Bibtex@inproceedings{ ipr_1170857347, author = "{Holger M{{\"o}}nnich and J{{\"o}}rg Raczkowsky and Heinz W{{\"o}}rn}", title = "{Model Checking for Robotic Guided Surgery}", year = "2010", booktitle = "{Electronic Healthcare}", }
zurück zur Publikationsübersicht