Abstract:

Lors de la conception d'un système temps réel, avoir la connaissance complète du système est difficile voire impossible et augmente la complexité de la conception, de la vérification et de la recherche de contrôleur pour ces systèmes. L'utilisation d'un modèle temporel paramétré est alors intéressante et permet d'abstraire la représentation du système. Cependant, pour des modèles paramétrés généraux des SED tels que les Parametric Timed Automata ou les Parametric Time Petri Nets, le problème de l'existence de valeurs des paramètres telles qu'un état soit accessible est indécidable. Il n'existe actuellement pas d'algorithme de synthèse de valeurs de paramètres excepté pour des sous classes très restrictives de ces modèles. Nous proposons donc de considérer des sous classes sémantiques des SED à paramètres temporels pour lesquelles les paramètres sont pris dans l'ensemble des entiers. Ces sous classes sont en pratique peu restrictives mais d'un point de vue théorique conduisent à la décidabilité de nombreux problèmes de model-checking, de synthèse de paramètres et de contrôle.