Abstract FR:

Depuis peu les robots font leur apparition dans les salles d'operation, et tendent a s'introduire parmi les humains pour les assister dans la vie quotidienne. Cet elargissement du champ operatoire des robots necessite une robustesse accrue et une programmation plus sophistiquee. Le langage maestro propose dans cette these, ainsi que son environnement de verification formelle contribue a faire face a ces besoins. Il s'inscrit dans une approche tres structuree de la programmation robotique : l'approche controle commande. Celle-ci dissocie les aspects continus de la commande des robots et le controle discret dont la logique decide des changements de mode de commande. Nous avons concu maestro comme un langage de programmation dedie au controle robotique. Sa principale originalite est l'introduction de methodes formelles dans le domaine de la robotique pour d'analyse des programmes, promouvant ainsi une surete de programmation accrue. Pour ce faire, nous utilisons tout d'abord des techniques d'analyse statique. Elles sont basees sur un ensemble de regles logiques decrivant le comportement de chacun des operateurs du langage et permettant la verification de certaines proprietes generiques, independantes de l'application. De plus, nous avons defini une traduction des programmes maestro dans le langage synchrone esterel, donnant acces a des outils de verification comportementale. Celles-ci aident a prouver que les reactions du programme sont systematiquement correctes, quelque soit le deroulement de l'execution. En plus d'une syntaxe simple et dediee a la robotique, nous avons defini pour maestro une semantique et une interface claire avec les actions elementaire de commande, a la base de la traduction en esterel. L'utilisation de maestro a ete validee grace a une implantation dans l'environnement centaur et des experimentations conjointes avec l'environnement orccad sur plusieurs plates-formes robotiques.