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