Modélisation et synthèse de contrôleurs des systèmes hybrides linéaires

Abstract

Ce mémoire présente, d'abord, une méthode de modélisation des systèmes hybrides linéaires. Le modèle adopté pour la modélisation d'un procédé physique ayant une composante continue et une composante discrète est un automate hybride linéaire qui définit une sous-classe des automates hybrides. Ce travail se situe dans le cadre des travaux de Thomas Henzinger. Ensuite, une procédure de synthèse de contrôleurs des systèmes hybrides linéaires a été développée. Cette procédure consiste à transformer une procédure de vérification en une procédure de synthèse. D'où, la présentation d'un outil de vérification nommé HYTECH ainsi que son adaptation en un outil de synthèse. Dans ce mémoire, nous considérons un système de positionnement d'antennes comme exemple d'application.