Search

Unmanned Aerial Vehicles (UAV) are now widespread in our society and are often used in a context where they can put people at risk. Studying their reliability, in particular in the context of flight above a crowd, thus becomes a necessity. In this thesis, we study the modeling and analysis of UAV in the context of their flight plan. To this purpose, we build several parametrics probabilistic models of the UAV and use them, as well as a given flight plan, in order to model its trajectory. Our most advanced model takes into account the precision of position estimation by embeddedsensors, as well as wind force and direction.The model is analyzed in order to measure the probability that the drone enters an unsafe zone. Because of the nature and complexity of the obtained models, their exact verification using classical tools such as PRISM or PARAM is impossible. We therefore develop a new approximation method, called Parametric Statistical Model Checking. This method has been implemented in a prototype tool, which we tested on this complex case study. Finally, we use the result to propose some ways to improve the safety of the public in our context.; Les drones sont maintenant très répandus dans la société et sont souvent utilisés dans des situations dangereuses pour le public environnant. Il est alors nécessaire d’étudier leur fiabilité, en particulier dans le contexte de vols au-dessus d’un public. Dans cette thèse, nous étudions la modélisation et l’analyse de drones dans le contexte de leur plan de vol. Pour cela, nous construisons plusieurs modèles probabilistes du drone et les utilisons ainsi que le plan de vol pour modéliser la trajectoire du drone. Le modèle le plus détaillé obtenu prend en compte des paramètres comme la précision de l’estimation de la position par les différents capteurs, ainsi que la force et la direction du vent. Le modèle est analysé afin de mesurer la probabilité que le drone entre dans une zone dangereuse. Du fait de la nature et de la complexité des modèles successifs obtenus, leur vérification avec les outils classiques, tels que PRISM ou PARAM, est impossible. Nous utilisons donc une nouvelle méthode d’approximation, appelée Model Checking Statistique Paramétrique. Cette méthode a été implémentée dans un prototype, que nous avons mis à l’épreuve sur ce cas d’étude complexe. Nous avons pour finir utilisé les résultats fournis par ce prototype afin de proposer des pistes permettant d’améliorer la sécurité du public dans le contexte considéré.

This thesis aims to propose an architecture that addresses the design, supervision, management and adaptation of an interactive experience. We therefore propose a complete framework to facilitate the modeling phase of an interactive system and guarantee sufficient flexibility to achieve the objectives of complexity, scalability, adaptability and improvement through automatic learning. For this purpose, the formal model, CIT, based on two layers of description was introduced. The dynamic supervision process consists in controlling the interactive experience with regard to the formal model, based on networks of timed input/output automata. Two softwares, CELTIC (Common Editor for Location Time Interaction and Content) and EDAIN (Execution Driver based on Artificial INtelligence), implementing the CIT model and the activity supervision engine respectively, were developed during this thesis., Cette thèse a pour objectif de proposer une architecture répondant aux problématiques de conception, de supervision, de pilotage et d'adaptation d'une expérience interactive. Nous proposons donc un framework complet destiné à faciliter la phase de modélisation d’un système interactif et garantissant une souplesse suffisante pour atteindre les objectifs de complexité, d’extensibilité, d’adaptabilité et d’amélioration par apprentissage automatique. Pour cela, le modèle formel, CIT, basé sur deux couches de description a été introduit. Le processus de supervision dynamique consiste à contrôler l’expérience interactive au regard du modèle formel, basé sur des réseaux d’automates temporisés à entrées/sorties. Deux plateformes logicielles, CELTIC (Common Editor for Location Time Interaction and Content) et EDAIN (Execution Driver based on Artificial INtelligence), implémentant respectivement le modèle CIT et le moteur de supervision de l’activité ont été développés au cours de cette thèse.

This piece of work is situated in the context of research on notation systems enabled to transcribe symbolically the concrete and sensorial aspect, and not only the abstract and structural aspect, of computer music artefacts. In this perspective, we first expose a complete and minimal formal model for digital audio objects and structures, relatively to the criteria of perception ; this model is implemented as a Turing-potent functional language, that draws the correspondance between the mathematical expression of a signal and its computational realisation. Then, we apply this formal construction to the expression of a number of schemes for sound synthesis, producing a software synthetiser whose expressivity is consequent. These tools are organised following the lines of Schaefferian theories, through a decomposition into categories whose parameters correspond with morphological notions. Finally, we draw the conclusions of a series of experiments aiming to evaluate the relevance of those schemes in human hearing, with the assistance of a musicologist, then with a number of subjects, and eventually by associating a public that is as wide as possible. This leads us to question the methodology most appropriate to tackle this kind of problem, which brings us closer to social science, and suggests a participative science approach.; Ce travail se situe dans le cadre de la recherche de systèmes de notation permettant de transcrire de façon symbolique l’aspect concret et sensoriel, et non seulement abstrait et structurel, des artefacts de la musique par ordinateur. Dans ce but, nous exposons tout d’abord un modèle formel complet et minimal des objets et structures audionumériques, en référence aux critères de la perception ; ce modèle est implémenté sous la forme d’un langage fonctionnel Turing-potent qui permet d’effectuer l’équivalence entre l’expression mathématique d’un signal et sa réalisation informatique. Puis, nous employons ce formalisme afin d’exprimer un ensemble de critères de synthèse sonore, ce qui donne lieu à un logiciel de synthèse dont l’expressivité est considérable. Ces outils sont organisés suivant le schéma des théories Schaefferiennes, par une décomposition catégorielle dans laquelle les paramètres correspondent à des notions morphologiques. Finalement, nous rendons compte d’une série d’expériences visant à évaluer la pertinence de ces critères dans l’audition humaine, avec le concours d’un musicologue, puis sur un ensemble de sujets, et enfin vis-à-vis d’un public aussi large que possible. Ceci nous conduit à remettre en question la méthodologie la plus adéquate pour traiter ce type de problème, qui nous rapproche des sciences humaines et sociales, et suggère une démarche de science participative.

Caches’ systems are ubiquitous in modern computer systems, eitherembedded in hardware (processors, disks controlers, . . . ) or in software(file systems, databases, web servers, . . . ). A large amount ofwork has been dedicated to design, implement and optimise thosesystems. However there exists to the best of our knowledge no universalconception of what is and what achieves a cache, and thereforeno tool allowing the conception and the simulation of systemsdefined this way. In this thesis we propose such a generic and universalpoint of view on caches and we develop a new cache modeltoward this direction. A simulator implementing this model is realisedand examples are developed in order to illustrate the usageof the model and validate its relevance., Les systèmes de cache sont omniprésents dans les systèmes informatiquesmodernes, qu’ils soient embarqués dans le matériel (processeurs,contrôleurs de disques, . . .) ou le logiciel (systèmes de fichiers,bases de données, serveurs web, . . .). Une grande quantité de travauxont été réalisés pour concevoir, implémenter et optimiser cessystèmes. Cependant il n’existe pas à notre connaissance de conceptionuniverselle de ce qu’est et réalise un cache, ni donc d’outil permettantla conception et la simulation de système définis ainsi. Danscette thèse nous proposons un tel point de vue générique et universelsur les caches et nous développons un nouveau modèle de cacheallant dans cette direction. Un simulateur implémentant ce modèleest réalisé et des exemples sont développés afin d’illustrer l’usage dumodèle et d’en valider la pertinence.

Both design and development of Real-Time Embedded Systems (RTES) are very complex because of the wide range of execution platforms. These systems must also meet non-functional requirements such as time constraints. Model Driven Engineering (MDE) is particularly suitable for handling the diversity of implementation targets. Therefore, several RTES development suites leverage MDE by automatically generating platform-specificcode from high-level design models. Such tools may also take non-functional requirements into account by integrating verification activities. These activities typically rely on the generation of formal models from the same high-level design descriptions used for code generation. However, the consideration of the behavior of software execution platforms stays a major problem. On the one hand, code generators often reveal a lack of consideration genericity, on the other hand, the generation of formal models partly overlooks mecanisms of these platforms. How can the behavior both generically and formally be considered ? The presented work is part of a tool suite during a multiplatform deployment phase. The adopted strategy relies on the composition of a deployed application model with a model of the behavior of the targeted platform, within a MDE. Behavior is formally translated with classical Time Petri Nets (TPNs). A formalization is then proposed to compose a global TPN regardless of the considered platform. As an illustration, we finally give a generation example of TPNs describing an application deployed on two different platforms (OSEK/VDX and VxWORKS ).; La conception et le développement des systèmes temps réels embarqués (SETRs) sont très complexes du fait d’un grand nombre de plates-formes d’exécution. Ces systèmes doivent aussi répondre à des exigences non-fonctionnelles telles que les contraintes temporelles. L’Ingénierie Dirigée par les Modèles (IDM) répond à la diversité de mise en oeuvre de tels systèmes. Plusieurs suites de développement tirent ainsi profit de l’IDM pour générer automatiquement du code spécifique à une plate-forme à partir de descriptions de conception haut niveau des SETRs. De tels outils considèrent alors des exigences non-fonctionnelles en générant des modèles formels pour intégrer des activités de vérification. Cependant, la considération du comportement des plates-formes d’exécution logicielles demeure un problème majeur. D’un côté, les générateurs de code manquent bien souvent de généricité de considération, de l’autre, la génération de modèles formels s’abstrait en partie des mécanismes de ces plates-formes. Est-il alors possible de considérer à la fois génériquement et formellement ce comportement ? Ce travail s’intègre dans une suite d’outils durant une phase de déploiement multiplates-formes. La stratégie adoptée repose sur la composition d’un modèle d’application déployée avec celui du comportement de la plate-forme visée, dans une IDM. Le comportement est traduit formellement avec les classiques réseaux de Petri temporels (ou Time Petri Net (TPNs)). Une formalisation est alors proposée pour composer un TPN global indépendamment de la plate-forme considérée. À titre d’exemple, la génération de TPNs d’une application exécutée sur deux plates-formes différentes (OSEK/VDX et VxWORKS ) est enfin donnée.

Both design and development of Real-Time Embedded Systems (RTES) are very complex because of the wide range of execution platforms. These systems must also meet non-functional requirements such as time constraints. Model Driven Engineering (MDE) is particularly suitable for handling the diversity of implementation targets. Therefore, several RTES development suites leverage MDE by automatically generating platform-specificcode from high-level design models. Such tools may also take non-functional requirements into account by integrating verification activities. These activities typically rely on the generation of formal models from the same high-level design descriptions used for code generation. However, the consideration of the behavior of software execution platforms stays a major problem. On the one hand, code generators often reveal a lack of consideration genericity, on the other hand, the generation of formal models partly overlooks mecanisms of these platforms. How can the behavior both generically and formally be considered ? The presented work is part of a tool suite during a multiplatform deployment phase. The adopted strategy relies on the composition of a deployed application model with a model of the behavior of the targeted platform, within a MDE. Behavior is formally translated with classical Time Petri Nets (TPNs). A formalization is then proposed to compose a global TPN regardless of the considered platform. As an illustration, we finally give a generation example of TPNs describing an application deployed on two different platforms (OSEK/VDX and VxWORKS ).; La conception et le développement des systèmes temps réels embarqués (SETRs) sont très complexes du fait d’un grand nombre de plates-formes d’exécution. Ces systèmes doivent aussi répondre à des exigences non-fonctionnelles telles que les contraintes temporelles. L’Ingénierie Dirigée par les Modèles (IDM) répond à la diversité de mise en oeuvre de tels systèmes. Plusieurs suites de développement tirent ainsi profit de l’IDM pour générer automatiquement du code spécifique à une plate-forme à partir de descriptions de conception haut niveau des SETRs. De tels outils considèrent alors des exigences non-fonctionnelles en générant des modèles formels pour intégrer des activités de vérification. Cependant, la considération du comportement des plates-formes d’exécution logicielles demeure un problème majeur. D’un côté, les générateurs de code manquent bien souvent de généricité de considération, de l’autre, la génération de modèles formels s’abstrait en partie des mécanismes de ces plates-formes. Est-il alors possible de considérer à la fois génériquement et formellement ce comportement ? Ce travail s’intègre dans une suite d’outils durant une phase de déploiement multiplates-formes. La stratégie adoptée repose sur la composition d’un modèle d’application déployée avec celui du comportement de la plate-forme visée, dans une IDM. Le comportement est traduit formellement avec les classiques réseaux de Petri temporels (ou Time Petri Net (TPNs)). Une formalisation est alors proposée pour composer un TPN global indépendamment de la plate-forme considérée. À titre d’exemple, la génération de TPNs d’une application exécutée sur deux plates-formes différentes (OSEK/VDX et VxWORKS ) est enfin donnée.

In the last decade, the complexity of embedded systems has exploded and the usual industrial design flows do not suffice any more to propose reliable products while respecting time to market constrain. Thus, developing new design methodologies has become an imperative. The thesis aims at the improvement of the methodologies of conception of the embedded systems. It proposes a method for assisting the process of refinement along the design flow. The proposed approach splits the design flow into multiple-levels, in order to guide the designer in the design process, from the most abstract model down to a synthesizable model. Furthermore, by using formal techniques the method allows to check the preservation of functional correctness along the design flow., La dernière décennie, la complexité des technologies embarqués a explosé et les flots de conception industrielle habituels ne suffisent plus pour proposer des produits fiables en respectant les exigences du marché. Ainsi, le développement de nouvelles méthodologies de conception est devenu un besoin impératif. La thèse vise l'amélioration des méthodologies de conception des systèmes embarqués. En proposant une approche de conception par niveaux d’abstraction, la nouvelle approche permet de guider et d’assister les concepteurs dans les étapes de conception, précisément de raffiner les composants de communication. Elle offre des garanties de préservation des propriétés fonctionnelles le long du flot de conception. La méthode proposée permet de raisonner sur les différents niveaux de description d'un système en exploitant des techniques de preuve de propriétés associées aux raffinement formel.

In Arabic language, the assignation of case marks and modal marks is explained by a formal model, the theory of government: the words which exhibit these marks, the "operands", receive them by action of "operators" present in the statement. Ibn al-Anbārī's (m.1181) Inṣāf provides information on the progressive definition of principles and terminology for this model. At the same time semantic models of case marks interpreting cases in terms of meanings are developed: one compatible with the formal model of government is based on verbal syntax and particle's syntax and set by Ğurğānī (m.1078) and relayed by Zamaḫšarī (m.1144). A concurrent logical-semantic model distinguishes the case of predicative elements from the case of non-predicative elements: it has been systematized by Astarābāḏī (m.1287) and tends to make obsolete the government's principle according to which every case results of a concrete operator's action., En arabe, l'attribution des marques de cas et de modes s'inscrit dans un modèle formel, la théorie de la rection : les mots "régis" reçoivent ces marques de "régissants" présents dans l'énoncé. L'Inṣāf d'Ibn al-Anbārī (m.1181) nous renseigne sur la précision progressive des principes de ce modèle et d'un métalangage propre. Parallèlement se développent des modélisations sémantiques du marquage casuel, interprétant les cas en termes de significations : l'une, compatible avec le modèle rectionnel formel, se fonde sur la syntaxe verbale et particulaire. Elle est fixée par Ğurğānī (m.1078) et relayée par Zamaḫšarī (m.1144). Une conception concurrente, logico-sémantique, oppose le cas des termes du noyau prédicatif à ceux des éléments non prédicatifs : systématisée par Astarābāḏī (m.1287), elle tend à rendre caduc le principe rectionnel selon lequel tout cas résulte de l'action d'un régissant concret.

The objective of this PhD thesis is to provide a model, a method and a tool for producing interactive scenarios. Our solution solves the opposition between the controlle devolution of a video game and its interactivity level. In other words, our goal is to assist (authors) in producing video games whose unfolding satisfies authors’ intentions while it is simultaneously influenced by player’s choices (expressed via her/his actions).To this purpose, our proposal is to allow users to produce a good quality game scenario model, which is: (a) rich – the scenario provides enough pertinent options for player/non-player characters so that the player can determine the evolution of the game and always feels that the created discourse is interesting, (b) valid – all the possible discourses in the scenario are consistent and meet authors required effects, (c) operational – the representation of the scenario is executable. This scenario is then used as the input of an interactive storytelling control system to assist it in managing the unfolding of the game. As a consequence, the evolution of the video games, which are directed by such a control system, guarantees authors requirements, while at the same time, it depends on player’s actions. In order to execute the foregoing proposal, we base our solution on a calculable mathematical model (linear logic) which provides rigorous and automatic deduction mechanisms. We have made an overview of existing approaches concerning interactive storytelling controland scenario validation problems. This allows us to identify necessary principles for our solution, such as: architecture elements of a control system; construction, representation, implementation of narrative scenarios; important narrative properties; reference evolution of the drama parameters; discourse structuralization; scenario validation strategy; necessary statistical and qualitative information; etc. Our contributions consist (1) in the definition of a set of narrative properties specifying the quality of game scenarios; (2) in the proposal of models, algorithms and tools in order to produce scenario models respecting these properties. We validate our results by realizing two examples. The first is an extract of an education algame explaining how to apply our tools to produce a valid game scenario model, which is expressed by a linear logic sequent whose representation conforms to a metamodel of the sequent calculus. For the second example, we describe the complete production process of areal video game based on the story "Little Red Cap", implementing a prototype of control system we have proposed, which allows unfolding the game according to the produced valid scenario, so its evolution satisfies authors intentions and simultaneously depends on player's actions.; L’objectif de cette thèse est de fournir un modèle, une méthode et un outil d’aide à la réalisation de scénarios interactifs. Cette solution répond au problème de l’opposition entre la maîtrise du déroulement d’un jeu vidéo et son niveau d’interactivité. En d’autres termes, notre but est d’aider à réaliser des jeux vidéo dont l’évolution satisfait les intentions des auteurs tout en autorisant un déroulement influencé par les choix du joueur (exprimés aux travers de ses actions). Pour cela, notre proposition permet à l’utilisateur de produire un modèle de scénario de jeu de bonne qualité qui est : (a) riche – le scénario fournit suffisamment d’options pertinentes aux personnages joueur/non-joueur de sorte que le joueur puisse déterminer le déroulement du jeu et sente toujours que le discours créé est intéressant, (b) valide – tous les discours possibles dans le scénario sont cohérents et répondent aux effets désirés par les auteurs, (c) opérationnel – la représentation du scénario est exécutable. Ce scénario est ensuite employé comme l’entrée d’un système de pilotage de narration interactive assurant le contrôle de la gestion du déroulement du jeu. Par conséquent, l’évolution des jeux, qui sont dirigés par un tel système de pilotage, garantit que l’exécution du jeu respecte les souhaits des auteurs, et en même temps, autorise la liberté des actions du joueur. Pour répondre au problème exposé ci-dessus, nous appuyons notre solution sur un modèle mathématique calculable (la logique linéaire) qui offre des mécanismes de déductions rigoureux et automatiques.Nous avons fait un tour d'horizon des approches existantes concernant le pilotage de narration interactive et la validation de scénario. Ceci nous permet d'identifier les principes nécessaires à notre solution, tels que les éléments d'architecture d'un système de pilotage ; la construction,la représentation, l'exécution de scénarios narratifs ; les propriétés de narration importantes ; l'évolution de référence des paramètres dramatiques ; la structuration de discours ; la stratégie pour la validation d'un scénario ; les informations qualitatives et statistiques nécessaires… Nos contributions portent (1) sur la définition d'un ensemble de propriétés de narration spécifiant la qualité des scénarios de jeu ; (2) sur la proposition de modèles, algorithmes et outils pour écrire des modèles de scénario respectant ces propriétés. Nous validons nos résultats par la réalisation de deux exemples. Le premier est un extrait d'un jeu éducatif expliquant comment appliquer notre outil en vue de produire un modèle de scénario de jeu valide, qui est exprimé par un séquent de logique linéaire dont la représentation est conforme à un métamodèle du calcul des séquents. Pour le second exemple, nous décrivons le processus de production complet d'un jeu vidéo réel basé sur l'histoire « Le Petit Chaperon rouge », mettant en oeuvre un prototype de système de pilotage que nous avons proposé, ce qui permet de dérouler le jeu selon le scénario valide produit, donc son évolution satisfait les intentions des auteurs, et en même temps, dépend des actions du joueur.

The objective of this PhD thesis is to provide a model, a method and a tool for producing interactive scenarios. Our solution solves the opposition between the controlle devolution of a video game and its interactivity level. In other words, our goal is to assist (authors) in producing video games whose unfolding satisfies authors’ intentions while it is simultaneously influenced by player’s choices (expressed via her/his actions).To this purpose, our proposal is to allow users to produce a good quality game scenario model, which is: (a) rich – the scenario provides enough pertinent options for player/non-player characters so that the player can determine the evolution of the game and always feels that the created discourse is interesting, (b) valid – all the possible discourses in the scenario are consistent and meet authors required effects, (c) operational – the representation of the scenario is executable. This scenario is then used as the input of an interactive storytelling control system to assist it in managing the unfolding of the game. As a consequence, the evolution of the video games, which are directed by such a control system, guarantees authors requirements, while at the same time, it depends on player’s actions. In order to execute the foregoing proposal, we base our solution on a calculable mathematical model (linear logic) which provides rigorous and automatic deduction mechanisms. We have made an overview of existing approaches concerning interactive storytelling controland scenario validation problems. This allows us to identify necessary principles for our solution, such as: architecture elements of a control system; construction, representation, implementation of narrative scenarios; important narrative properties; reference evolution of the drama parameters; discourse structuralization; scenario validation strategy; necessary statistical and qualitative information; etc. Our contributions consist (1) in the definition of a set of narrative properties specifying the quality of game scenarios; (2) in the proposal of models, algorithms and tools in order to produce scenario models respecting these properties. We validate our results by realizing two examples. The first is an extract of an education algame explaining how to apply our tools to produce a valid game scenario model, which is expressed by a linear logic sequent whose representation conforms to a metamodel of the sequent calculus. For the second example, we describe the complete production process of areal video game based on the story "Little Red Cap", implementing a prototype of control system we have proposed, which allows unfolding the game according to the produced valid scenario, so its evolution satisfies authors intentions and simultaneously depends on player's actions., L’objectif de cette thèse est de fournir un modèle, une méthode et un outil d’aide à la réalisation de scénarios interactifs. Cette solution répond au problème de l’opposition entre la maîtrise du déroulement d’un jeu vidéo et son niveau d’interactivité. En d’autres termes, notre but est d’aider à réaliser des jeux vidéo dont l’évolution satisfait les intentions des auteurs tout en autorisant un déroulement influencé par les choix du joueur (exprimés aux travers de ses actions). Pour cela, notre proposition permet à l’utilisateur de produire un modèle de scénario de jeu de bonne qualité qui est : (a) riche – le scénario fournit suffisamment d’options pertinentes aux personnages joueur/non-joueur de sorte que le joueur puisse déterminer le déroulement du jeu et sente toujours que le discours créé est intéressant, (b) valide – tous les discours possibles dans le scénario sont cohérents et répondent aux effets désirés par les auteurs, (c) opérationnel – la représentation du scénario est exécutable. Ce scénario est ensuite employé comme l’entrée d’un système de pilotage de narration interactive assurant le contrôle de la gestion du déroulement du jeu. Par conséquent, l’évolution des jeux, qui sont dirigés par un tel système de pilotage, garantit que l’exécution du jeu respecte les souhaits des auteurs, et en même temps, autorise la liberté des actions du joueur. Pour répondre au problème exposé ci-dessus, nous appuyons notre solution sur un modèle mathématique calculable (la logique linéaire) qui offre des mécanismes de déductions rigoureux et automatiques.Nous avons fait un tour d'horizon des approches existantes concernant le pilotage de narration interactive et la validation de scénario. Ceci nous permet d'identifier les principes nécessaires à notre solution, tels que les éléments d'architecture d'un système de pilotage ; la construction,la représentation, l'exécution de scénarios narratifs ; les propriétés de narration importantes ; l'évolution de référence des paramètres dramatiques ; la structuration de discours ; la stratégie pour la validation d'un scénario ; les informations qualitatives et statistiques nécessaires… Nos contributions portent (1) sur la définition d'un ensemble de propriétés de narration spécifiant la qualité des scénarios de jeu ; (2) sur la proposition de modèles, algorithmes et outils pour écrire des modèles de scénario respectant ces propriétés. Nous validons nos résultats par la réalisation de deux exemples. Le premier est un extrait d'un jeu éducatif expliquant comment appliquer notre outil en vue de produire un modèle de scénario de jeu valide, qui est exprimé par un séquent de logique linéaire dont la représentation est conforme à un métamodèle du calcul des séquents. Pour le second exemple, nous décrivons le processus de production complet d'un jeu vidéo réel basé sur l'histoire « Le Petit Chaperon rouge », mettant en oeuvre un prototype de système de pilotage que nous avons proposé, ce qui permet de dérouler le jeu selon le scénario valide produit, donc son évolution satisfait les intentions des auteurs, et en même temps, dépend des actions du joueur.

Internet servers are software with specific features. Indeed, they answer request of wide and distant clients, support the customer evolution and be robust because they never stop. The concurrency models allow to interleave the statements of wide customers. No general agreement frees on a better model. To abstract himself from the concurrency model, I propose a development model of Internet servers. Model checkers allow to increase the software safety. But, it is necessary to provide a simple model of software to check it. I propose to use my development model of servers in order to genrate ther server automatically and its formal model. Finally as the request parsing depends on the concurrency model, I propose to use Tatoo, a parser generator. Tatoo abstracts himself from this dependency and automates the development of parsing; Les serveurs Internet sont des logiciels particuliers. Ils doivent répondre aux demandes d'un grand nombre de clients distants, supporter leur évolution et être robustes car ils ne s'arrêtent jamais. Les modèles de concurrence permettent d'entrelacer les traitements d'un grand nombre de clients. Aucun consensus ne se dégage sur un meilleur modèle. Pour s'abstraire du modèle de concurrence, je propose un modèle de développement de serveurs Internet. Les outils de vérification formelle permettent d'accroître la sûreté des logiciels mais il est nécessaire de leur fournir un modèle simple du logiciel. Le modèle de développement que je propose est utilisé pour générer le serveur et son modèle formel. Le décodage d'une requête cliente dépend du modèle de concurrence. Je propose d'utiliser un générateur d'analyseur syntaxique qui s'abstrait de ce problème et automatise le développement du décodage

This work deals with the automatic testing of interactive systems. The proposed approach is based on testing techniques for synchronous reactive software. The behaviour of synchronous systems, consisting of cycles starting by reading an input and ending by issuing an output, is to a certain extent similar to the one of interactive systems. In particular, we are using Lutess, a synchronous testing environment, to validate interactive systems. We show the interest of applying the testing techniques proposed by Lutess in order to generate interesting scenarios and we illustrate their use on a case study (a mobile virtual reality application). We also study the generation of test data from task trees, which can be enriched by operational profiles specification. The adaptation of synchronous testing techniques for the validation of multimodal interactive systems is also studied, taking into account multimodality-related properties.; Ce travail porte sur le test automatique de systèmes interactifs. L'approche proposée est basée sur des techniques de test de systèmes réactifs synchrones. Le comportement de systèmes synchrones, qui est constitué de cycles commençant par la lecture d'une entrée et finissant par l'émission d'une sortie, est sous certaines conditions, similaire à celui de systèmes interactifs. En particulier, nous étudions l'utilisation de Lutess, un environnement de test synchrone, pour valider les systèmes interactifs. Nous montrons l'intérêt d'utiliser les techniques de test proposées par Lutess afin de générer des scénarios intéressants et nous illustrons leur utilisation sur une étude de cas (une application de réalité virtuelle mobile). Nous avons également étudié la génération de données de test à partir d'arbres de tâches, qui peuvent être enrichis d'une spécification de profils opérationnels. L'adaptation des techniques de test synchrone à la validation d'applications interactives multimodales est également étudiée, notamment en prenant en compte certaines propriétés concernant la multimodalité.