October 12, 2020
Adrien Le Coënt (LACL)Les systèmes cyber-physiques, faisant interagir des éléments informatiques et des éléments physiques, sont un des modèles majeurs de ces dernières années, pour lesquels la modélisation et la vérification formelle sont encore des challenges actuels.
Les difficultés majeures rencontrées actuellement dans l’étude formelle de ces systèmes sont: 1. La complexité des algorithmes de synthèse, limitant fortement la dimension des systèmes que l’on peut concevoir 2. La difficulté du calcul de l’ensemble atteignable, limitant le type de dynamique continue que l’on peut considérer dans ces modèles.
Nous présenterons des études de cas qui illustrent ces difficultés, et proposerons des méthodes qui tentent de répondre à ces difficultés. Plus précisément, nous proposons une méthode de synthèse compositionnelle qui permet de casser la complexité algorithmique de la recherche de contrôleur. Nous présenterons également comment utiliser une méthode de simulation garantie dans un outil de synthèse de contrôleur.