Laboratoire d’Analyse et d’Architecture des Systèmes
A.MEKKI-MOKHTAR
TSF
Doctorat : Univ. de Toulouse 3-UPS, 12 Décembre 2012, 128p., Président: G.JUANOLE, Rapporteurs: F.SIMONOT-LION, J.M.THIRIET, Examinateurs: D.ANDREU, Directeurs de thèse: D.POWELL, J.GUIOCHET, Membre invité: J.P.BLANQUART , N° 12674
Lien : http://tel.archives-ouvertes.fr/tel-00766636
Diffusable
Plus d'informations
Les progrès récents dans la définition de mécanismes décisionnels ont permis de déléguer de plus en plus de responsabilités aux systèmes informatiques. Par exemple, des robots de service travaillent aujourd'hui en interaction avec l'humain et réalisent des tâches de plus en plus complexes. Ce transfert de responsabilité pose alors de manière critique le problème de la sécurité pour l'homme, l'environnement du système, ou le système lui-même. La surveillance en ligne par un moniteur de sécurité indépendant vise à assurer un comportement sûr malgré la présence de fautes et d'incertitudes. Un tel moniteur doit détecter des situations potentiellement dangereuses afin d'enclencher des actions de mise en état sûr et d'éviter les défaillances catastrophiques. Cette thèse traite de l'identification de conditions de déclenchement de sécurité permettant de lancer des actions de mise en état sûr. Un processus systématique permettant d'identifier de telles conditions est défini, en partant d'une analyse de risque HazOp/UML du système fonctionnel. Par ailleurs, une méthode est proposée pour identifier les états du système où des actions de sécurité peuvent être enclenchées simultanément, afin d'être revues et corrigées, en cas de besoin, par un expert du système. L'approche proposée est appliquée à un robot déambulateur.
Recent progress in the definition of decisional mechanisms has allowed computer-based systems to become more and more autonomous. For example, service robots can nowadays work in direct interaction with humans and carry out increasingly complex tasks. This transfer of responsibility poignantly raises the issue of system safety towards humans, the environment and the system itself. System surveillance by an independent safety monitor aims to enforce safe behaviour despite faults and uncertainties. Such a monitor must detect potentially dangerous situations in order to trigger safety actions aiming to bring the system towards a safe state. This thesis addresses the problem of identifying safety trigger conditions. A systematic process is proposed for the identification, starting from a HazOp/UML risk analysis. The proposed methodology also allows the identification of system states in which multiple safety actions might be executed concurrently, in order to be checked and, if necessary, corrected by a system expert. The methodology is applied to a robotic rollator.
R.AKROUT
TSF
Doctorat : INSA Toulouse, 18 Octobre 2012, 142p., Président: A.BENZEKRI, Rapporteurs: C.AGUILAR MELCHOR, C.BIDAN, Examinateurs: A.RIBAULT, Directeurs de thèse: M.KAANICHE, V.NICOMETTE , N° 12747
Lien : http://tel.archives-ouvertes.fr/tel-00782565
Diffusable
Plus d'informations
Avec le développement croissant d'Internet, les applications Web sont devenues de plus en plus vulnérables et exposées à des attaques malveillantes pouvant porter atteinte à des propriétés essentielles telles que la confidentialité, l'intégrité ou la disponibilité des systèmes d'information. Pour faire face à ces malveillances, il est nécessaire de développer des mécanismes de protection et de test (pare feu, système de détection d'intrusion, scanner Web, etc.) qui soient efficaces. La question qui se pose est comment évaluer l'efficacité de tels mécanismes et quels moyens peut-on mettre en oeuvre pour analyser leur capacité à détecter correctement des attaques contre les applications web. Dans cette thèse nous proposons une nouvelle méthode, basée sur des techniques de clustering de pages Web, qui permet d'identifier les vulnérabilités à partir de l'analyse selon une approche boîte noire de l'application cible. Chaque vulnérabilité identifiée est réellement exploitée ce qui permet de s'assurer que la vulnérabilité identifiée ne correspond pas à un faux positif. L'approche proposée permet également de mettre en évidence différents scénarios d'attaque potentiels incluant l'exploitation de plusieurs vulnérabilités successives en tenant compte explicitement des dépendances entre les vulnérabilités. Nous nous sommes intéressés plus particulièrement aux vulnérabilités de type injection de code, par exemple les injections SQL. Cette méthode s'est concrétisée par la mise en oeuvre d'un nouveau scanner de vulnérabilités et a été validée expérimentalement sur plusieurs exemples d'applications vulnérables. Nous avons aussi développé une plateforme expérimentale intégrant le nouveau scanner de vulnérabilités, qui est destinée à évaluer l'efficacité de systèmes de détection d'intrusions pour des applicationsWeb dans un contexte qui soit représentatif des menaces auxquelles ces applications seront confrontées en opération. Cette plateforme intègre plusieurs outils qui ont été conçus pour automatiser le plus possible les campagnes d'évaluation. Cette plateforme a été utilisée en particulier pour évaluer deux techniques de détection d'intrusions développées par nos partenaires dans le cadre d'un projet de coopération financé par l'ANR, le projet DALI.
Web applications vulnerability analysis and intrusion detection systems assessment With the increasing development of Internet, Web applications have become increasingly vulnerable and exposed to malicious attacks that could affect essential properties such as confidentiality, integrity or availability of information systems. To cope with these threats, it is necessary to develop efficient security protection mechanisms and testing techniques (firewall, intrusion detection system, Web scanner, etc..). The question that arises is how to evaluate the effectiveness of such mechanisms and what means can be implemented to analyze their ability to correctly detect attacks against Web applications. This thesis presents a new methodology, based on web pages clustering, that is aimed at identifying the vulnerabilities of a Web application following a black box analysis of the target application. Each identified vulnerability is actually exploited to ensure that the identified vulnerability does not correspond to a false positive. The proposed approach can also highlight different potential attack scenarios including the exploitation of several successive vulnerabilities, taking into account explicitly the dependencies between these vulnerabilities. We have focused in particular on code injection vulnerabilities, such as SQL injections. The proposed method led to the development of a new Web vulnerability scanner and has been validated experimentally based on various vulnerable applications. We have also developed an experimental platform integrating the new web vulnerability scanner, that is aimed at assessing the effectiveness ofWeb applications intrusion detection systems, in a context that is representative of the threats that such applications face in operation. This platform integrates several tools that are designed to automate as much as possible the evaluation campaigns. It has been used in particular to evaluate the effectiveness of two intrusion detection techniques that have been developed by our partners of the collaborative project DALI, funded by the ANR, the French National Research Agency.
H.CHU
TSF
Doctorat : Institut National Polytechnique, Toulouse, 1 Septembre 2011, 105p., Président: J.ARLAT, Rapporteurs: B.ESPIAU, P.J.GIL VIVENTE, Examinateurs: J.P.BLANQUART, F.INGRAND, D.SEGUELA, Directeurs de thèse: D.POWELL, M.O.KILLIJIAN , N° 11495
Lien : http://tel.archives-ouvertes.fr/tel-00627225/fr/
Diffusable
Plus d'informations
The implementation of autonomous systems requires the development and the using of multi-layer software architecture. Typically, a functional layer contains several modules that control the material of the system and provide elementary services. To be robust, the functional layer must be implemented with protection mechanisms with respect to erroneous or inopportune requests sent from the superior layer. We present a methodology for robustness testing these mechanisms. We define a general framework to evaluate the robustness of a functional layer by characterizing its behavior with respect to inappropriate requests. We also propose an validation environment based on fault injection in the control software of a simulated robot. A great number of test cases is generated automatically by the mutation of a sequence of valid requests. The descriptive statistics of the behaviors in the presence of inappropriate requests are analyzed in order to evaluate the robustness of the system under test.
La mise en oeuvre de systèmes autonomes nécessite le développement et l'utilisation d'architectures logicielles multi-couches qui soient adaptées. Typiquement, une couche fonctionnelle renferme des modules en charge de commander les éléments matériels du système et de fournir des services élémentaires. Pour être robuste, la couche fonctionnelle doit être dotée de mécanismes de protection vis-à-vis de requêtes erronées ou inopportunes issues de la couche supérieure. Nous présentons une méthodologie pour tester la robustesse de ces mécanismes. Nous définissons un cadre général pour évaluer la robustesse d'une couche fonctionnelle par la caractérisation de son comportement vis-à-vis de requêtes inopportunes. Nous proposons également un environnement de validation basé sur l'injection de fautes dans le logiciel de commande d'un robot simulé. Un grand nombre de cas de tests est généré automatiquement par la mutation d'une séquence de requêtes valides. Les statistiques descriptives des comportements en présence de requêtes inopportunes sont analysées afin d'évaluer la robustesse du système sous test.
O.HAMOUDA
TSF
Doctorat : Université Paul Sabatier, Toulouse, 19 Juillet 2010, 166p., Président:G.JUANOLE, Rapporteurs: B.CICIANI, R.MARIE, Examinateurs: H-P.SCHWEFEL, Directeurs de thèse: M.KAANICHE, K.KANOUN , N° 10721
Lien : http://tel.archives-ouvertes.fr/tel-00546260/fr/
Diffusable
Plus d'informations
Cette thèse porte sur le développement de méthodes et de modèles permettant de quantifier la sûreté de fonctionnement d'applications embarquées sur des systèmes mobiles. L'objectif est de fournir des indicateurs pour l'analyse et la sélection des architectures les plus adaptées pour satisfaire les exigences de sûreté de fonctionnement. Nous considérons le cas des applications véhiculaires utilisant des communications inter-véhicules basées sur des réseaux ad-hoc et pouvant avoir accès à des services situés sur des infrastructures fixes. Nous proposons une approche combinant: 1) des modèles de sûreté de fonctionnement utilisant des réseaux d'activités stochastiques permettant de décrire les modes défaillances et de restauration des systèmes considérés et 2) des simulations et des modèles analytiques de scénarios de mobilité permettant d'estimer des caractéristiques de connectivité de ces systèmes. Cette approche est illustrée sur trois cas d'études dont un système d'autoroute automatisée, et une boîte noire virtuelle basée sur la réplication et la sauvegarde coopérative des données.
This thesis focuses on developing methods and models making it possible to evaluate quantitative measures characterizing the dependability of mobile services as perceived by the users. These models and measures are aimed at providing support to the designers during the selection and analysis of candidate architectures that are well suited to fulfill the dependability requirements. We consider the case of vehicular applications using inter-vehicle communications based on ad-hoc networks and may have access to services located on fixed infrastructure. We propose an approach combining: 1) dependability models based on stochastic activity networks, in order to describe the system failure modes and associated recovery mechanisms, and 2) simulation and analytical models allowing the estimation of connectivity characteristics, taking into account different mobility scenarios and environment. This approach is illustrated on three case studies including a virtual black box based on cooperative data replication and backup, and an automated highway system (Platooning application).
M.SGHAIRI
TSF
Doctorat : Institut National Polytechnique, Toulouse, 27 Mai 2010, 146p., Président:F.SIMONOT-LION, Rapporteurs: M.BAYART, L.PAUTET, Examinateurs: Y.TRINQUET, J.J.AUBERT, P.BROT, Directeurs de thèse: A.DE BONNEVAL, Y.CROUZET , N° 10414
Lien : http://tel.archives-ouvertes.fr/tel-00509156/fr/
Diffusable
Plus d'informations
The current civil aircraft's electrical flight control has been changed to take benefit of technical improvements. New technologies, when mature, can be incorporated in aircrafts. Evolutions are considered towards a digital communication and intelligent actuators. This thesis is aiming at proposing alternative architectures with distribution of system functionality between flight control computers and actuators with less hardware and software resources. New architectures must meet the same safety and availability requirements with additional operational reliability (required by airlines). Dependability and robustness of new architectures have been validated trough respectively OCAS / AltaRica and Matlab / Simulink.
L'aboutissement aux Commandes de Vol Électriques (CDVE) des avions civils actuels s'est fait par étapes, après une longue maturation des différentes technologies mises en place. La prochaine étape est l'utilisation de communications intégralement numériques et d'actionneurs intelligents. Cette thèse propose de nouvelles architectures, en rupture avec l'état de l'art, avec de nouvelles répartitions des fonctions intelligentes entre l'avionique centrale (calculateurs de commandes de vols) et l'avionique déportée (électroniques locales des actionneurs) dont l'avantage est d'exiger moins de ressources par rapport aux architectures conventionnelles tout en satisfaisant les mêmes exigences de sécurité et de disponibilité ainsi que les exigences croissantes en fiabilité opérationnelle de la part des compagnies aériennes. La sûreté de fonctionnement et la robustesse des nouvelles architectures proposées ont été validées respectivement sous OCAS/Altarica et Matlab/Simulink.
E.LACOMBE
TSF
Doctorat : Institut National des Sciences Appliquées, Toulouse, 15 Décembre 2009, 164p., Président : D. HAGIMONT, Rapporteurs : J-L. LANET, J-J. QUISQUATER, F. RAYNAL, Examinateurs : C. BLANCHER, L. DUFLOT, Directeurs de thèse : Y. DESWARTE, V. NICOMETTE , N° 09853
Lien : http://tel.archives-ouvertes.fr/tel-00462534/fr/
Diffusable
Plus d'informations
Cette thèse traite de la préservation de l'intégrité des systèmes d'exploitation courants. L'objectif est de répondre aux menaces actuelles et futures que représentent les logiciels malveillants qui s'implantent dans le noyau de ces systèmes (comme les rootkits "noyau") ou du moins en altèrent l'intégrité (comme les rootkits "hyperviseur"). La première partie de ce document se focalise sur ces logiciels malveillants. Tout d'abord, les attaques logiques sur les systèmes informatiques sont présentées dans leur globalité. Ensuite est proposée une classification des actions malveillantes qui provoquent la perte de l'intégrité d'un noyau. Enfin, les résultats d'une étude sur les rootkits "noyau" sont donnés et la création d'un rootkit original est expliquée. La seconde partie s'intéresse à la protection des noyaux. Après une description de l'état de l'art, une approche originale est proposée, fondée sur le concept de préservation de contraintes. En premier lieu, les éléments essentiels sur lesquels reposent un noyau sont identifiés et les contraintes sur ces éléments, nécessaires à un fonctionnement correct du noyau, sont exposées. Un hyperviseur léger (Hytux) a été conçu pour empêcher la violation de ces contraintes en interceptant certaines des actions du noyau. Sa mise en oeuvre est décrite pour un noyau Linux 64 bits sur architecture x86 qui dispose des technologies Intel VT-x et VT-d.
This Ph.D thesis addresses the integrity preservation of current operating systems. The main goal is to counter current and future threats coming from malware that infects the kernel of these systems (as kernel rootkits) or at least that provoke a loss of their integrity (as hypervisor rootkits). The first part of this document focuses on such malware. First, logical attacks are presented globally. Then, a classification of malicious actions that lead to the loss of kernel integrity is proposed. Finally, the outcomes of a study on kernel rootkits are given and the creation of an original rootkit is explained. The second part deals with kernel protection. After describing the state of the art, an original approach is proposed, based on the concept of constraint preservation. First, the essential elements which a kernel rests on are identified and the required constraints on these elements for correct kernel operation are exhibited. A lightweight hypervisor (Hytux) has been elaborated to prevent any violation of these constraints by intercepting some actions of the kernel. Its implementation is described for a 64-bit Linux kernel on an x86 architecture that supports the Intel VT-x and VT-d technologies.
C.LU
TSF
Doctorat : Institut National Polytechnique, Toulouse, 14 Décembre 2009, 142p., Président: C.CONSEL, Rapporteurs: F.SIMONOT-LION, Y.TRINQUET, Examinateurs: A.ALBINET, F.OUGIER, Directeurs de thèse: J.C.FABRE, M.O.KILLIJIAN , N° 09899
Lien : http://tel.archives-ouvertes.fr/tel-00468924/fr/
Diffusable
Plus d'informations
Les mécanismes de détection et de recouvrement d'erreur doivent être soigneusement sélectionnés pour les applications embarquées automobiles, principalement à cause de ressources limitées et de contraintes économiques. Cependant, des exigences de sûreté importantes, aggravées par la complexité croissante du logiciel, motive l'industrie automobile à chercher des solutions techniques pour améliorer la robustesse à l'exécution. Le défi est de concevoir une solution de tolérance aux fautes portable, flexible, à forte contraintes économique, en examinant différemment les techniques classiques de redondance et de diversification. Le principe directeur est de contrôler rigoureusement quelle information et quand elle est essentielle à récupérer; quelle instrumentation est nécessaire pour réaliser de la tolérance aux fautes et où il faut la placer dans le programme. La thèse propose une approche pour développer un logiciel de défense, tel un composant externe configurable, reposant sur l'observabilité et la contrôlabilité de mécanismes fournis par un standard d'architecture logicielle automobile émergent AUTOSAR.
Due to limited resources and stringent economical constraints in the automotive industry, error detection and recovery mechanisms of embedded systems are carefully selected. However, critical safety requirements and increasing software complexity motivate car makers to look for technical solutions to improve online software robustness. The challenge is to design a portable, customizable, and lowcost solution for fault tolerance by using differently classical techniques, such as redundancy and diversification. The main principle is to control rigorously which information and when it is necessary to get it; which instrumentation is necessary to perform fault tolerance and where to add this instrumentation in the source code. An approach to develop a defense software is proposed. The defense software is designed as an external customizable component, relying on control and observability mechanisms provided by an emergent standard for automotive software architecture AUTOSAR.
G.VACHE
TSF
Doctorat : Institut National des Sciences Appliquées, Toulouse, 8 Décembre 2009, Président : M. Cukier, Rapporteurs : M. Dacier, B. Randell, Examinateurs : V. Nicomette, Directeur de thèse : J-C. Laprie , N° 09889
Lien : http://tel.archives-ouvertes.fr/tel-00462530/fr/
Diffusable
Plus d'informations
Cette thèse présente une nouvelle approche pour l'évaluation quantitative de la sécurité des systèmes informatiques. L'objectif de ces travaux est de définir et d'évaluer plusieurs mesures quantitatives. Ces mesures sont des mesures probabilistes visant à quantifier les influences de l'environnement sur un système informatique en présence de vulnérabilités. Dans un premier temps, nous avons identifié les trois facteurs ayant une influence importante sur l'état du système : 1) le cycle de vie de la vulnérabilité, 2) le comportement de la population des attaquants et 3) le comportement de l'administrateur du système. Nous avons étudié ces trois facteurs et leurs interdépendances et distingué ainsi deux scénarios principaux, basés sur la nature de la découverte de la vulnérabilité, malveillante ou non. Cette étape nous a permis d'identifier les états possibles du système en considérant le processus d'exploitation de la vulnérabilité et de définir quatre mesures relatives à l'état du système qui peut être vulnérable, exposé, compromis, corrigé ou sûr. Afin d'évaluer ces mesures, nous avons modélisé ce processus de compromission. Par la suite, nous avons caractérisé de manière quantitative les événements du cycle de vie de la vulnérabilité à partir de données réelles issues d'une base de données de vulnérabilités pour paramétrer nos modèles de manière réaliste. La simulation de ces modèles a permis d'obtenir les valeurs des mesures définies. Enfin, nous avons étudié la manière d'étendre le modèle à plusieurs vulnérabilités. Ainsi, cette approche a permis l'évaluation de mesures quantifiant les influences de différents facteurs sur la sécurité du système.
This thesis presents a new approach for quantitative security evaluation for computer systems. The main objective of this work is to define and evaluate several quantitative measures. These measures are probabilistic and aim at quantifying the environment influence on the computer system security considering vulnerabilities. Initially, we identified the three factors that have a high influence on system state: 1) the vulnerability life cycle, 2) the attacker behaviour and 3) the administrator behaviour. We studied these three factors and their interdependencies and distinguished two main scenarios based on nature of vulnerability discovery, i.e. malicious or non malicious. This step allowed us to identify the different states of the system considering the vulnerability exploitation process and to define four measures relating to the states of the system: vulnerable, exposed, compromised, patched and secure. To evaluate these measures, we modelled the process of system compromising by vulnerability exploitation. Afterwards, we characterized the vulnerability life cycle events quantitatively, using real data from a vulnerability database, in order to assign realistic values to the parameters of the models. The simulation of these models enabled to obtain the values of the four measures we had defined. Finally, we studied how to extend the modelling to consider several vulnerabilities. So, this approach allows the evaluation of measures quantifying the influences of several factors on the system security.
Y.LAAROUCHI
TSF
Doctorat : Université Paul Sabatier, Toulouse, 30 Novembre 2009, 175p., Président: D.POWELL, Rapporteurs: G.MULLER, F.SIMONOT-LION, Examinateurs: F.ARMAND, E.TOTEL, E.DE NADAI, Directeurs de thèse: Y.DESWARTE, J.ARLAT , N° 09898
Lien : http://tel.archives-ouvertes.fr/tel-00468923/fr/
Diffusable
Plus d'informations
La conception et le développement des applications critiques en avionique sont soumis à des contraintes strictes visant à assurer un niveau de confiance compatible avec les exigences de sécurité-innocuité (au sens safety) des tâches mises en Suvre. Ces contraintes induisent un accroissement considérable des coûts de production et de maintenance, ce qui rend le prix de revient de tels systèmes prohibitif. D'un autre côté, les composants sur étagère (Commercial Off-The-Shelf, COTS), matériels et logiciels, sont maintenant d'usage courant et offrent des services étendus pour un coût faible. Cependant, les COTS ne répondent pas aux contraintes d'innocuité exigées pour les tâches critiques ; de plus, ils présentent des vulnérabilités facilement exploitables par des attaques, les rendant incompatibles avec des exigences élevées de sécurité-immunité (au sens security). Il serait toutefois intéressant de profiter de tels composants dans un contexte avionique, mais en faisant en sorte qu'ils ne puissent affecter de façon préjudiciable les tâches critiques. Intégrer de tels composants dans les systèmes avioniques conduit donc à prendre en considération l'hétérogénéité des niveaux de confiance entre d'une part les applications critiques classiques, et d'autre part de nouvelles applications utilisant des composants sur étagère. Dans le cadre de cette thèse, nous proposons une architecture autorisant de telles interactions tout en préservant les propriétés de safety et security. La définition de cette architecture s'appuie sur le modèle Totel, et elle utilise la virtualisation afin de faciliter la mise en Suvre des mécanismes de tolérance aux fautes destinés à augmenter la crédibilité d'une application exécutée de façon répliquée sur des plateformes d'exécution COTS de niveau de confiance faible. Afin de valider notre approche, nous avons réalisé un prototype en nous appuyant sur deux cas d'étude identifiés avec Airbus et concernant tous deux des ordinateurs portables : un dédié à la maintenance et un au calcul du profil de décollage d'un avion.
In avionics, the design and development of critical software applications are strictly constrained in order to ensure a confidence level commensurate with the safety requirements of the implemented tasks. These constraints considerably increase the development and maintenance costs, making such critical systems very expensive. On the other hand, Commercial Off-The-Shelf (COTS) components (hardware and software) are widespread and offer extensive functionalities for a reasonable cost. However, such components are unreliable and vulnerable to malicious attacks. Nevertheless, it would be interesting to take advantage of such (hardware and software) COTS components for non-critical tasks in avionics while preventing them from detrimentally affecting critical tasks. To do so, we need to consider interactions between components with heterogeneous criticality levels. In this thesis, we propose an architecture allowing such interactions in a safe and secure manner, i.e., such that correct operation of the critical components is not affected. This architecture is based on Totel's model and uses virtualization to support the implementation of fault tolerance techniques to increase the confidence level of an application executed redundantly on untrusted COTS platforms. To demonstrate our approach, we have implemented a prototype based on two case studies identified with Airbus: a maintenance laptop and a take-off profile computation laptop.
M.D.NGUYEN
TSF
Doctorat : Ecole Doctorale Systèmes, 19 Novembre 2009, 124p., Président : T. GAYRAUD, Rapporteurs : A. R. CAVALLI, F. SIMONOT-LION, Examinateurs : K. GUENNOUN, N. RIVIERE, H-P. SCHWEFEL, Directeur de thèse : D. POWELL, Co-directeur de thèse : H WAESELYNCK , N° 09856
Lien : http://tel.archives-ouvertes.fr/tel-00459848/fr/
Diffusable
Plus d'informations
Les avancées technologiques du monde du « sans fil » ont conduit au développement dapplications dédiées à linformatique mobile. Leurs caractéristiques propres posent de nouveaux défis pour leur vérification. Ce mémoire traite de la technologie de test pour les systèmes mobiles. Nous avons débuté notre travail par un état de lart sur le test des applications mobiles conjointement avec une analyse dune étude de cas, un protocole d'appartenance de groupe (GMP) dans le domaine des réseaux ad hoc, pour nous permettre de mieux comprendre les problèmes liés au test de ces applications. En conséquence, nous avons décidé davoir une approche de test qui se base sur les descriptions de scénarios. Nous avons constaté que les scénarios dinteractions doivent tenir compte des configurations spatiales des nSuds comme un concept majeur. Afin de couvrir les nouvelles spécificités des systèmes mobiles dans les langages de descriptions, nous avons introduit des extensions qui portent essentiellement sur les relations spatio-temporelles entre nSuds et sur la communication par diffusion. Le traitement de laspect spatial a conduit au développement de loutil GraphSeq. GraphSeq a pour but danalyser des traces de test afin dy identifier des occurrences de configurations spatiales successives décrites à partir dun scénario abstrait. Lapplication de GraphSeq (support à limplémentation des cas de test, vérification de la couverture des traces) est présentée avec les analyses des sorties dun simulateur de mobilité et des traces dexécution de létude de cas GMP.
Advances in wireless networking have yielded the development of mobile computing applications. Their unique characteristics provide new challenges for verification. This dissertation elaborates on the testing technology for mobile systems. As a first step, a review of the state-of-the-art is performed together with a case study - a group membership protocol (GMP) in mobile ad hoc settings - that allowed us to gain insights into testing problems. We present, then, a testing approach which bases on the descriptions of scenarios. We note that the scenario interactions must take into account the spatial configurations of nodes as first class concepts. To cover new specificities of mobile systems in description languages, we introduce some extensions that focus on spatio-temporal relations between nodes and on broadcast communication. The processing of spatial aspect leads to the development of the tool GraphSeq. GraphSeq aims to analyze test traces in order to identify occurrences of successive spatial patterns described in an abstract scenario. The application of GraphSeq (support to implementation of test cases, verification of trace coverage) is shown with the analysis of outputs of a simulator and execution traces of the case study GMP.