Méthodes et outils pour la vérification symbolique de systèmes temporisés

This work proposes a method for the analysis of real-time systems. The method is based on the compilation of specifications into timed graphs, from which it is possible to verify real-timeproperties and to generate executable code.Timed graphs are automata extended with a set of variables,called clocks, which are used to express timing constraints. An algorithm for constructing a finite timed graph froman ATP program is developed. ATP is an algebra of timedprocesses with built-in timed operators such as timeoutsand watchdogs. The main interest of the algorithm is thatthe size of the graph is independent of the values oftime parameters. Real-time properties are specified as formulas of thelogic TCTL. It is shown that temporal constructs can beexpressed as fixed points in terms of an appropriatenext-state operator. Furthermore, this work proposesa symbolic model-checking algorithm for TCTL. Thecharacteristic set of a formula is computed as adisjunction of linear constraints over the set of clocks.Both algorithms have been implemented within the KRONOS tool, which has been used to verify several non-trivial real-time applications. The results obtained show the practical interest of this approach.Ce travail propose une méthode pour l'analyse de systèmes temps-reél. Cette méthode est basée sur la compilation des spécificationsvers des graphes temporisés, à partir desquels il est possiblede vérifier des propriétés et de générer du code exécutable.Les graphes temporisés sont des automates étendus avec desvariables, appelées horloges, qui permettent de décrire lescontraintes temporelles. Un algorithme de compilation est développé pour l'algèbrede processus temporisés ATP, qui est une extension des algèbres de processus avec des opérateurs temporels comme le ``timeout'' et le ``watchdog''. L'intérêt de l'algorithme est que la taille du graphe obtenu est indépendante des valeurs des paramètres des opérateurs temporels.Les propriétés temps-reél sur les graphes temporisés sont décrites par des formules de la logique TCTL. Il est montré que les opérateurs temporelsde TCTL s'expriment en termes de points fixes à l'aide d'un opérateur ``d'état suivant'' défini de façon appropriée.De plus, ce travail propose un algorithme de vérification quiconsiste à évaluer symboliquement l'ensemble caractéristiqued'une formule comme une disjonction de contraintes linéairessur les horloges.Les algorithmes de compilation et de vérification développés ont été implémentés dans l'outil KRONOS, utilisé pour analyser des applications temps-reél significatives. Les résultats obtenus confirment l'intérêtpratique de l'approche proposée