Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal. / Ce mémoire présente un outil et une méthodologie permettant le développement rapide de modèles structurés dans le but de vérifier la fonctionnalité de systèmes numériques VLSI. Le modèle d'un système numérique s'élabore en décrivant le comportement du système tel qu'observé à son interface avec le monde extérieur. Les chronogrammes représentent les opérations de base de l'interface du système, sur lesquelles sont mises en évidence les relations temporelles entre les événements composant l'opération. Ceci permet de décrire précisément l'aspect temporel (timing) de l'opération. Son aspect fonctionnel est capturé en annotant de procédures et de fonctions, les événements d'un chronogramme. La composition à l aide d'opérateurs hiérarchiques des diagrammes chronologiques de base complète la description du comportement du système tel qu'observable à son interface. Idéalement, les diagrammes chronologiques hiérarchiques annotés sont capturés graphiquement. Un langage de description de ces diagrammes est proposé afin de servir de forme intermédiaire entre les outils de capture et des applications qui utilisent les diagrammes. Une de ces applications est traitée: soit la génération de modèles exécutables de système en langage de description de matériel, à partir de leur description sous forme de chronogrammes hiérarchiques annotés. L aspect algorithmique de cette simulation est abordé et un exemple précisant les concepts de modélisation est développé. La modélisation, en composant hiérarchiquement les opérations de base d'un système sur lesquelles l'aspect temporel et fonctionnel est capturé, permet le développement rapide et précis de modèles. La possibilité d'exécuter ces modèles permet de vérifier le comportement d'un système avant même de commencer le développement de sa réalisation matérielle. Les problèmes potentiels du système sont ainsi identifiés à un stade où il est moins coûteux d'y remédier.

L'utilisation des réseaux de capteurs sans fil (RCSF) croît dans plusieurs domaines, dont celui des espaces intelligents. Dans un espace intelligent, les RCSF sont utilisés puisque les noeuds qui les composent se dissimulent dans l'environnement et consomment très peu d'énergie. Pour l'installation, la maintenance et la gestion des contextes, il est nécessaire de pouvoir reprogrammer un, noeud sans avoir à le redémarrer. Ce projet de recherche vise l'amélioration de la reprogrammation des RCSF en utilisant l'ingénierie logicielle basée sur les composants (ILBC). En utilisant un cadriciel hybride de composants et un format exécutable allégé, les composants dynamiques deviennent utilisables à moindres coûts. Les résultats obtenus lors de ces travaux ont été publiés dans un article de journal. Les travaux de ce projet se divisent en deux volets. Le premier volet est l'optimisation des cadriciels dynamiques de composants. Le problème est que ces derniers demandent trop de ressources et ne sont pas envisageables pour les RCSF. Afin de diminuer la surcharge en taille de l'utilisation de composants dynamiques, un concept de cadriciel hybride de composants' est proposé. Pour valider ce concept, le cadriciel NodeCom est créé et requiert aussi peu de mémoire que Contiki. NodeCom possède un noyau minimal qui est statique alors que les autres composants peuvent être statiques ou dynamiques. Le deuxième volet est l'optimisation de la reprogrammation adaptée aux RCSF avec l'ILBC. C'est en compressant. le format de fichiers exécutable qui contint les composants que la reprogrammation est optimisée. Le chargement dynamique utilisé est accéléré et la consommation énergétique du transfert de composants est diminuée. C'est le format ELF qui est modifié pour partager les composants dynamiques. Pour réduire sa taille, plusieurs sections et symboles peuvent être supprimés en raison des contraintes imposées par l'utilisation de l'ILBC. Puisque les RCSF utilisent majoritairement des microcontrôleurs 8 bits ou 16 bits, les métadonnées 32 bits du format ELF sont converties. La résultante de ces modifications est le format de composants ComELF qui permet d'obtenir des compressions de près de 50 %. À ce format, une description des composants est finalement ajoutée pour permettre une gestion automatique du chargement dynamique.

La programmation orientée langage (Language-Oriented Programming – LOP) préconise l’utilisation de langages de modélisation dédiés exécutables (eXecutable Domain-Specific Modeling Languages – xDSMLs) pour la conception, le développement, la vérification et la validation de systèmes hautement concurrents. De tels systèmes placent l’expression de la concurrence dans les langages informatiques au coeur du processus d’ingénierie logicielle, par exemple à l’aide de formalismes dédiés appelés modèles de concurrence (Models of Concurrency – MoCs). Ceux-ci permettent une analyse poussée du comportement des systèmes durant les phases de vérification et de validation, mais demeurent complexes à comprendre, utiliser, et maîtriser. Dans cette thèse, nous développons et étendons une approche qui vise à faire collaborer l’approche LOP et les MoCs à travers le développement de xDSMLs dans lesquels la concurrence est spécifiée de façon explicite (Concurrency-aware xDSMLs). Dans de tels langages, on spécifie l’utilisation systématique d’un MoC au niveau de la sémantique d’exécution du langage, facilitant l’expérience pour l’utilisateur final qui n’a alors pas besoin d’appréhender et de maîtriser l’utilisation du MoC choisi.Un tel langage peut être raffiné lors de la phase de déploiement, pour s’adapter à la plateforme utilisée, et les systèmes décrits peuvent être analysés sur la base du MoC utilisé. / Language-Oriented Programming (LOP) advocates designing eXecutable Domain-Specific Modeling Languages (xDSMLs) to facilitate the design, development, verification and validation of modern softwareintensive and highly-concurrent systems. These systems place their needs of rich concurrency constructs at the heart of modern software engineering processes. To ease theirdevelopment, theoretical computer science has studied the use of dedicated paradigms for the specification of concurrent systems, called Models of Concurrency (MoCs). They enable the use of concurrencyaware analyses such as detecting deadlocks or starvation situations, but are complex to understand and master. In this thesis, we develop and extend an approach that aims at reconciling LOP and MoCs by designing so-called Concurrencyaware xDSMLs. In these languages, the systematic use of a MoC is specified at the language level, removing from the end-user the burden of understanding or using MoCs. It also allows the refinement of the language for specific execution platforms, and enables the use of concurrency-aware analyses on the systems.

Les méthodes de vérification automatique des logiciels connaissent un succès croissant depuis le début des années 2000, suite à plusieurs succès industriels (Microsoft, Airbus, etc.). L'analyse statique vise, à partir d'une description du programme, à inférer automatiquement des propriétés vérifiées par celui-ci. Les techniques standards d'analyse statique travaillent sur le code source du logiciel, écrit par exemple en C ou Java. Cependant, avoir accès au code source n'est pas envisageable pour de nombreuses applications relatives à la sécurité, soit que le code source n'est pas disponible (code mobile, virus informatiques), soit que le développeur ne veut pas le divulguer (composants sur étagère, certification par un tiers).Nous nous intéressons dans cette thèse à la conception et au développement d'une plate-forme d'analyse statique de code binaire à des fins d'analyse de sécurité. Nos principales contributions se font à trois niveaux: sémantique, implémentation et analyse statique.Tout d'abord, la sémantique des programmes binaires analysés est basée sur un formalisme générique appelé DBA qui a été enrichi avec des mécanismes de spécification et d'abstraction. La définition de la sémantique des programmes binaires requiert aussi un modèle mémoire adéquat.Nous proposons un modèle mémoire adapté au binaire, inspiré des travaux récents sur le code C bas-niveau. Ce nouveau modèle permet de profiter de l'abstraction du modèle à régions tout en gardant l'expressivité du modèle plat.Ensuite, notre plate-forme d'analyse de code binaire nommée BinSec offre trois services de base: désassemblage, simulation et analyse statique.Chaque instruction machine est traduite vers un bloc d'instructions DBA avec une sémantique équivalente. Une large partie des instructions x86 est gérée par la plateforme. Une passe de simplification permet d'éliminer les calculs intermédiaires inutiles afin d'optimiser le fonctionnement des analyses ultérieures. Nos simplifications permettent notamment d'éliminer jusqu'à75% des mises à jours de flags.Enfin, nous avons développé un moteur d'analyse statique de programmes binaires basé sur l'interprétation abstraite. Outre des domaines adaptés aux spécificités du code binaire, nous nous sommes concentrés sur le contrôle par l'utilisateur du compromis entre précision/correction et efficacité. De plus, nous proposons une approche originale de reconstruction de conditions dehaut-niveau à partir des conditions bas-niveau afin de gagner plus de précision d'analyse. L'approche est sûre, efficace, indépendante de la plateforme cibleet peut atteindre des taux de reconstruction très élevés. / Automatic software verification methods have seen increasing success since the early 2000s, thanks to several industrial successes (Microsoft, Airbus, etc.).Static program analysis aims to automatically infer verified properties of programs, based on their descriptions. The standard static analysis techniques apply on the software source code, written for instance in C or Java. However, access to source code is not possible for many safety-related applications, whether the source code is not available (mobile code, computer virus), or the developer does not disclose it (shelf components, third party certification).We are interested in this dissertation in design and development of a static binary analysis platform for safety analysis. Our contributions are made at three levels: semantics, implementation and static analysis.First, the semantics of analyzed binary programs is based on a generic, simple and concise formalism called DBA. It is extended with some specification and abstraction mechanisms in this dissertation. A well defined semantics of binary programs requires also an adequate memory model. We propose a new memory model adapted to binary level requirements and inspired from recent work on low-level C. This new model allows to enjoy the abstraction of the region-based memory model while keeping the expressiveness of the flat model.Second, our binary code analysis platform BinSec offers three basic services:disassembly, simulation and static analysis. Each machine instruction is translated into a block of semantically equivalent DBA instructions. The platform handles a large part of x86 instructions. A simplification step eliminates useless intermediate calculations in order to ease further analyses. Our simplifications especially allow to eliminate up to 75% of flag updates.Finally, we developed a static analysis engine for binary programs based on abstract interpretation. Besides abstract domains specifically adapted to binary analysis, we focused on the user control of trade offs between accuracy/correctness and efficiency. In addition, we offer an original approach for high-level conditions recovery from low-level conditions in order to enhance analysis precision. The approach is sound, efficient, platform-independent and it achieves very high ratio of recovery.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique

Les techniques formelles de la famille « vérification de modèles » (« model checking ») se heurtent au problème de l’explosion combinatoire. Ceci limite les perspectives d’exploitation dans des projets industriels. Ce problème est provoqué par la combinatoire dans la construction de l’espace des états possibles durant l’exécution des systèmes modélisés. Le nombre d’états pour des modèles de systèmes industriels réalistes dépasse régulièrement les capacités des ressources disponibles en calcul et stockage. Cette thèse défend l’idée qu’il est possible de réduire cette combinatoire en spécialisant les outils pour des familles de propriétés. Elle propose puis valide expérimentalement un ensemble de méthodes pour le développement de ce type d’outils en suivant une approche guidée par les propriétés appliquée au contexte temps réel. Il s’agit donc de construire des outils d’analyse performants pour des propriétés temps réel qui soient exploitables pour des modèles industriels de taille réaliste. Les langages considérés sont, d’une part UML étendu par le profil MARTE pour la modélisation par les utilisateurs, et d’autre part les réseaux de Petri temporisés comme support pour la vérification. Les propositions sont validées sur un cas d’étude industriel réaliste issu du monde avionique : l’étude de la latence et la fraicheur des données dans un système de gestion des alarmes exploitant les technologies d’Avionique Modulaire Intégrée. Ces propositions ont été mise en oeuvre comme une boite à outils qui intègre les cinq contributions suivantes: la définition de la sémantique d’exécution spécifiques aux propriétés temps réel pour les modèles d’architecture et de comportement spécifiés en UML/MARTE; la spécification des exigences temps réel en s’appuyant sur un ensemble de patrons de vérification atomiques dédiés aux propriété temps réel; une méthode itérative d’analyse à base d’observateurs pour des réseaux de Petri temporisés; des techniques de réduction de l’espace d’états spécifiques aux propriétés temps réel pour des Réseaux de Petri temporisés; une approche pour l’analyse des erreurs détectées par « vérification des modèles » en s’appuyant sur des idées inspirées de la « fouille de données » (« data mining »). / Automatic formal verification such as model checking faces the combinatorial explosion issue. This limits its application in indus- trial projects. This issue is caused by the explosion of the number of states during system’s execution , as it may easily exceed the amount of available computing or storage resources. This thesis designs and experiments a set of methods for the development of scalable verification based on the property-driven approach. We propose efficient approaches based on model checking to verify real-time requirements expressed in large scale UML-MARTE real-time system designs. We rely on the UML and its profile MARTE as the end-user modeling language, and on the Time Petri Net (TPN) as the verification language. The main contribution of this thesis is the design and implementation of a property-driven verification prototype toolset dedicated to real-time properties verification for UML-MARTE real-time software designs. We validate this toolset using an avionic use case and its user requirements. The whole prototype toolset includes five contributions: definition of real-time property specific execution semantics for UML-MARTE architecture and behavior models; specification of real- time requirements relying on a set of verification dedicated atomic real- time property patterns; real-time property specific observer-based model checking approach in TPN; real-time property specific state space reduction approach for TPN; and fault localization approach in model checking.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique / In this thesis a temporal model for abstract state machines (ASM) method is pro- posed. An extension of ASM specification language on the base of the proposed temporal model with continuous time is developed. The language extension helps to reduce the size of the specification hence to diminish the probability of an error. The semantics of the extended ASM language is developed which takes into account the definitions of external functions, the values of time delays and the method of non-determinism resolving. A subsystem for verification of user properties in the FOTL language is developed. A simulator prototype for ASMs with time is developed and implemented. It includes the parser of the timed ASM language, the interpreter, the verification subsystem and the graphical user interface