Cette thèse propose une nouvelle approche pour la synthèse de valeurs temporelles dans les systèmes temporisés. Notre approche est basée sur la méthode inverse suivante : à partir d’une instance de référence des paramètres, nous synthétisons une contrainte sur les paramètres, garantissant le même comportement que pour l’instance de référence, abstraction faite du temps. Il en résulte un critère de robustesse pour le système. En itérant cette méthode sur des points dans un domaine paramétrique borné, nous sommes alors à même de partitionner l’espace des paramètres en bonnes et mauvaises zones par rapport à une propriété à vérifier. Ceci nous donne une cartographie comportementale du système. Cette méthode s’étend aisément aux systèmes probabilistes. Nous présentons également des variantes de la méthode inverse pour les graphes orientés valués et les processus de décision markoviens. Parmi les prototypes implémentés, IMITATOR II implémente la méthode inverse et la cartographie pour les automates temporisés. Ce prototype nous a permis de synthétiser de bonnes valeurs pour les paramètres temporels de plusieurs études de cas, dont un modèle abstrait d’une mémoire commercialisée par le fabricant de puces STMicroelectronics, ainsi que plusieurs protocoles de communication. / This thesis proposes a novel approach for the synthesis of delays for timed systems, in particular in the framework oftimed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same timeabstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points of a bounded parameter domain, we are then able to partition the parametric space into good and bad zones, with respect to a given property one wants to verify. This gives a behavioral cartography of the system. This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols.

Les probabilités sont de plus en plus utilisées dans la conception et l'analyse des systèmes logiciels et matériels informatiques. L'introduction des tirages aléatoires dans les algorithmes concurrents et distribués permet de résoudre certains problèmes insolubles dans le cadre déterministe et de réduire la complexité de nombreux autres. Nous avons été amenés à étudier deux types de propriétés probabilistes. La convergence : cette propriété assure que, quel que soit l'état de départ et quel que soit l'enchainement des actions, le système atteindra toujours (avec probabilité 1) un ensemble donné d'états d'arrivée en un nombre fini d'actions (auto-stabilisation).L'accessibilité : ce type de propriété répond à des questions telles que "quelle est la probabilité p qu'une exécution partant d'un état initial donné atteigne un état final donné ? Quelles sont les bornes maximales et minimales de p ?" En ce qui concerne le premier point, nous avons développé de nouveaux critères permettant d'assurer la convergence et d'en calculer la vitesse (mixing time). Ces crotères utilisent l'analogie avec des modèles de physiquestatistique (champs de Markov) et exploitent des outils d'analyse probabiliste classiques (coupling, chaînes de Markov, processus de décision markoviens). Pour le second point, nous avons obtenu des résultats pratiques sur la vérification de protocoles de communication, comme le protocole Ethernet, en les modélisant à l'aide d'automates temporisés probabilistes et utilisant des outils de model-checking temporisés (HyTech) et probabiliste (PRISM, APMC).

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles.

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles. / We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a high-level formalism derived from the π-calculus, for considering stochastic, timed, deterministic or indeterministic behaviors. However, in the π-calculus, the basic communication primitive of systems is the synchronous point-to-point communication. However, mobile systems that use wireless networks, mostly communicate by local broadcast. Therefore, we first define the broadcast communication into the π-calculus, to better model the systems we study. We propose to use probabilistic and stochastic versions of the algebra we have defined to allow performance studies. We define a temporal version to consider time in the models. But the lack of tools for analyzing properties of models specified with π-calculus is a major obstacle to our work and its objectives. The definition of translation rules into the PRISM language allows us to translate our models in low-level models which can support model checking, namely discrete time, or continuous time Markov chains, timed automata, or probabilistic timed automata. We chose the PRISM model checker because, in our best knowledge, in its latest version, it is the only tool that supports the low-level formalisms that we have previously cited, and thus, makes it possible to realize complete performability studies. This approach allows us to overcome the lack of model checkers for our models. Subsequently, we apply these theoretical concepts to analyse performability of mobile wireless sensor networks.