| | | Module TH : Systèmes temporisés et hybrides |
Aujourd'hui, le logiciel joue un rôle préponderant dans des domaines tels que le contrôle du traffic aérien et terrestre, le multimédia et les télécommunications. Il s'agit notamment de logiciels embarqués qui intéragissent avec un environnement (souvent un phénomène physique) dans le but de contrôler son comportement. Le caractère "critique" de ces applications, dont la sûreté est le facteur le plus important à considérer, motive le besoin de développer des méthodes formelles de conception et de vérification dont le but est d'assurer le fonctionnement correct de ces systèmes avant leur implantation.
Nous abordons en premier lieu le problème de la spécification et l'analyse des propriétés temporelles quantitatives (dites aussi de "temps-réel") des applications, telles que, par exemple, les temps de réponse et les délais d'exécution et de communication. Ces propriétés sont modélisées par des automates équipés avec des horloges qui servent à mesurer et contrôler le temps écoulé entre les actions. Nous présentons le modèle et differentes méthodes d'analyse implantées dans l'outil KRONOS. Nous nous intéressons par la suite à une étude plus fine des intéractions entre le contrôleur et son environnement physique. Celui-ci étant de nature essentiellement continue, une telle étude nécessite un modèle "hybride" qui intègre les actions discrètes du contrôleur et l'évolution en temps continu de l'environnement. Ces systèmes sont modélisés par des automates étendus avec des variables continues dont l'évolution dans le temps est décrite par des inclusions différentielles. Nous présentons differentes approches d'analyse de systèmes hybrides et leur applications à des études de cas.
| | | Module TH : Systèmes temporisés et hybrides |