Difference between revisions of "Specifications, constraints and Proofs"

Revision as of 12:33, 4 April 2011

Presentation

Context and goals

Permanents staff

2 professors : Jean-François Dufourd and Pascal Schreck
4 assistant professors : Caroline Essert, Nicolas Magaud, Pascal Mathis, Julien Narboux

Other participants

Associate researcher : Gabriel Braun (MC) associate since 2009

Post-doctoral : Christophe Brun (ATER), Simon E.B. Thierry (ATER)

PhD students : Rémi Imbach

Former PhD students : Claire Baegert, Christophe Brun, Simon E. B. Thierry.

Outcome

Theorem proving

Specification, proofs of algorithms and implementation

Specification and constraint solving

Formalisation and planning of surgical interventions

In these works, we propose an original approach to assist automatically the planning of a position of a surgical tool. Our method allows for elaborating an optimal strategy of intervention, specific to the patient and to the type of intervention, thanks to an automatic computation which is based on the expertise of the field and the preoperative data.

To this end, we put into play some approaches coming from declarative modeling and geometric constraint solving, to compute automatically optimal trajectories for rigid and straight surgical tools. The comutation of the trajectory is performed in several steps. First, the expertise of the surgeon on a given type of intervention is transcribed

Dans cet objectif, nous avons mis en œuvre des approches issues de la modélisation déclarative et de la résolution de contraintes géométriques pour calculer automatiquement des trajectoires optimales d'outils chirurgicaux rectilignes rigides. Le calcul de trajectoire se fait en plusieurs étapes. Tout d'abord, l'expertise du praticien sur un type d'intervention donné est retranscrit sous forme d'équations mathématiques (égalités, fonctions de coût). Puis ces équations sont formalisées en contraintes géométriques, écrites sous la forme de termes combinant opérateurs géométriques et arithmétiques, et données issues des images médicales (IRM, CT). Un premier calcul permet de résoudre les contraintes géométriques dites "strictes" (booléennes) pour donner l'espace des solutions. Enfin, un deuxième calcul permet de résoudre les contraintes géométriques dites "souples" (numériques), grâce à une optimisation numérique, pour donner la solution optimale.

Nous avons testé nos approches sur 2 types d'interventions : l'ablation de tumeurs hépatiques par radiofréquence (hyperthermie) en collaboration avec le Pr. Gangi du service de radiologie interventionnelle de l'Hôpital Civil de Strasbourg, et l'implantation d'électrodes de stimulation cérébrale profonde en collaboration avec le Dr. Haegelen du service de neurochirurgie du CHU de Rennes Pontchaillou.

Le travail de thèse de Claire Baegert a porté sur ces travaux [1]. De nombreuses publications ont porté sur ces thèmes, concernant la radiofréquence [2][3][4][5][6] et la stimulation cérébrale profonde [7]. Ces travaux ont également donné lieu à une collaboration avec le DKFZ de Heidelberg sur l'accélération des calculs d'obstacles aux trajectoires par GPU [8][9].

Ces travaux ont donné lieu au projet ANR blanc ACouStiC, qui a démarré en janvier 2011 pour une durée de 4 ans, et dont IGG est partenaire. Ce thème de recherche s'insère également dans le cadre de l'IHU de Strasbourg "Institut de Chirugie Mini Invasive Guidée par l'Image" ou Mix-Surg.

Perspectives

Concernant la planification d'opérations chirurgicales, dans le cadre entre autres du projet ANR blanc ACouStiC, nous allons entamer une extension du domaine des solutions possibles, en étudiant les trajectoires courbes et/ou multiples, ainsi que les trajectoires volumiques. Cela nous permettra d'étendre le champ des applications à des outils chirurgicaux déformables, insérés dans des tissus également déformables, ou encore à des outils multiples (par exemple la cryoablation de tumeurs du foie), ou enfin à des volumes d'accès par exemple pour la craniotomie dans le cadre d'exérèse de lésions cérébrales. Nous allons également travailler à la navigation contrainte dans l'espace des solutions, afin de restreindre la modification de la trajectoire proposée à un espace des solutions possibles et/ou raisonnables. Pour cela, le lien sera fait avec l'axe "Visualisation et interactions" et notamment le thème de recherche sur les interfaces à retour d'effort.

@@ Line 31: / Line 31: @@
-===Spécification et résolution de contraintes===
+===Specification and constraint solving===
-===Formalisation et planification d'opérations percutanées===
+===Formalisation and planning of surgical interventions===
 [[Image:HD_snap_final_11104.jpg|left|thumb|200px]]
-Dans ce travail nous proposons une approche originale pour l'assistance à la planification avec automatisation du positionnement d'un outil chirurgical. Notre méthode permet d'élaborer une stratégie optimale d'intervention, spécifique au patient et au type d'opération concerné, grâce à un calcul automatique qui se base à la fois sur l'expertise du domaine et sur des données préopératoires.
+In these works, we propose an original approach to assist automatically the planning of a position of a surgical tool. Our method allows for elaborating an optimal strategy of intervention, specific to the patient and to the type of intervention, thanks to an automatic computation which is based on the expertise of the field and the preoperative data.
+To this end, we put into play some approaches coming from declarative modeling and geometric constraint solving,  to compute automatically optimal trajectories for rigid and straight surgical tools. The comutation of the trajectory is performed in several steps. First, the expertise of the surgeon on a given type of intervention is transcribed
 Dans cet objectif, nous avons mis en œuvre des approches issues de la modélisation déclarative et de la résolution de contraintes géométriques pour calculer automatiquement des trajectoires optimales d'outils chirurgicaux rectilignes rigides. Le calcul de trajectoire se fait en plusieurs étapes. Tout d'abord, l'expertise du praticien sur un type d'intervention donné est retranscrit sous forme d'équations mathématiques (égalités, fonctions de coût). Puis ces équations sont formalisées en contraintes géométriques, écrites sous la forme de termes combinant opérateurs géométriques et arithmétiques, et données issues des images médicales (IRM, CT). Un premier calcul permet de résoudre les contraintes géométriques dites "strictes" (booléennes) pour donner l'espace des solutions. Enfin, un deuxième calcul permet de résoudre les contraintes géométriques dites "souples" (numériques), grâce à une optimisation numérique, pour donner la solution optimale. [[Image:Caro zonesoptimisationdec2006 detoure.jpg|right|thumb|150px]]