Ce travail propose une méthode pour l'analyse de systèmes temps-reél. <br />Cette méthode est basée sur la compilation des spécifications<br />vers des graphes temporisés, à partir desquels il est possible<br />de vérifier des propriétés et de générer du code exécutable.<br /><br />Les graphes temporisés sont des automates étendus avec des<br />variables, appelées horloges, qui permettent de décrire les<br />contraintes temporelles. <br /><br />Un algorithme de compilation est développé pour l'algèbre<br />de processus temporisés ATP, qui est une extension des <br />algèbres de processus avec des opérateurs temporels comme <br />le ``timeout'' et le ``watchdog''. L'intérêt de l'algorithme est <br />que la taille du graphe obtenu est indépendante des valeurs <br />des paramètres des opérateurs temporels.<br /><br />Les propriétés temps-reél sur les graphes temporisés sont <br />décrites par des formules de la logique TCTL. <br />Il est montré que les opérateurs temporels<br />de TCTL s'expriment en termes de points fixes à l'aide d'un <br />opérateur ``d'état suivant'' défini de façon appropriée.<br />De plus, ce travail propose un algorithme de vérification qui<br />consiste à évaluer symboliquement l'ensemble caractéristique<br />d'une formule comme une disjonction de contraintes linéaires<br />sur les horloges.<br /><br />Les algorithmes de compilation et de vérification développés <br />ont été implémentés dans l'outil KRONOS, <br />utilisé pour analyser des applications temps-reél <br />significatives. Les résultats obtenus confirment l'intérêt<br />pratique de l'approche proposée.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00127808 |
| Date | 19 May 1993 |
| Creators | Yovine, Sergio |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds