7-10 juin 2022 Vannes (France)
Illustration de spécifications temporisées paramétrées sur des signaux continus
Etienne André  1  
1 : Laboratoire Lorrain de Recherche en Informatique et ses Applications
Institut National de Recherche en Informatique et en Automatique, Université de Lorraine, Centre National de la Recherche Scientifique : UMR7503

La spécification de propriétés peut s'avérer délicate. Nous proposons ici une approche automatisée pour l'illustration de propriétés données sous forme d'automates étendus avec des contraintes temporelles et des paramètres temporels, et qui peuvent également spécifier des contraintes sur des signaux à valeurs continues. En d'autres termes, étant donné une telle spécification et un automate bornant le comportement admissible de chacun des signaux, notre approche construit des exécutions continues fournissant ainsi des exemples d'exécutions réelles ou impossibles pour la spécification de départ. Dans notre approche, tant la spécification que les automates bornant les comportements admissibles sont donnés sous forme d'une sous-classe des automates hybrides linéaires, plus précisément des automates temporisés étendus par des vitesses d'horloges arbitraires, des contraintes sur les signaux, et des paramètres temporels ; notre méthode génère alors des exécutions concrètes permettant d'illustrer la spécification.



  • Poster
Personnes connectées : 1 Vie privée
Chargement...