Nous nous intéressons dans ce document à la génération automatique de tests de conformité pour des implémentations réactives. Nous nous attachons dans un premier temps à étendre la méthode de génération de tests, basée sur la théorie du test de conformité à la ioco, en reliant trois niveaux de description (propriétés, spécification et implémentation). Nous combinons pour cela vérification formelle et test de conformité. Nous obtenons ainsi, lors de l'exécution du cas de test sur l'implémentation, des verdicts pouvant indiquer la non-conformité de l'implémentation, mais également la satisfaction/violation de la propriété par l'implémentation et/ou la spécification. Nous étendons dans un deuxième temps la génération de tests par l'expressivité du modèle de spécification en nous intéressant aux spécifications interprocédurales récursives. Notre méthode est basée sur une analyse exacte de co-accessibilité permettant de décider si et comment un objectif de test pourra être atteint. Cependant, l'incapacité des cas de test récursifs à connaître leur propre pile d'exécution ne permet pas d'utiliser la totalité des résultats de l'analyse. Nous discutons de ce problème d'observation partielle et de ses conséquences puis nous proposons un moyen de minimiser son impact. Enfin, nous expérimentons ces méthodes de génération de tests sur quelques exemples et une étude de cas

En cette ère numérique, l’utilisation des documents papier s’avère peu pratique et inefficace, ce qui motive les sociétés à évoluer vers l’utilisation des documents électroniques (ou e-docs). Ce désir d’innover vers une opération sans papier peut améliorer l’efficacité et la qualité des services d’administrations publiques ou privées de manière à accélérer leurs activités et en même temps mieux satisfaire les besoins des clients. Cependant, cette pratique a créé des nouveaux besoins, tels que la signature numérique réelle de documents. Dans ce mémoire, nous avons proposé un nouveau schéma de signature numérique utilisant FIDO2, qui se trouve être une nouvelle norme d’authentification sécurisée en ligne basée sur la signature numérique. Le fait que FIDO2 soit un standard libre permet aux développeurs de logiciel et de matériel d’implémenter plus facilement leurs propres produits. Cela nous a inspiré à l’utiliser pour une fin de signature numérique, l’idée étant de remplacer le défi envoyé par le serveur avec le hash de e-docs et de l’envoyer à l’appareil du signataire afin que ce dernier signe avec sa clé privée. Comme dans le cas de l’infrastructure à clé publique, chaque utilisateur possédait une paire de clés, c’est-à-dire une clé privée et une clé publique. Un signataire doit confirmer son identification biométrique (empreinte digitale, reconnaissance faciale, voix, etc.) ou son code PIN pour accéder à la clé privée stockée localement sur son appareil et signer un document. Au cours de notre recherche, nous avons effectué plusieurs tests avec différents équipements (PC, USB FIDO, Smartphone) ainsi que différentes OS (Android, iOS, Windows). Les résultats de nos tests nous montrent que nous pouvons utiliser FIDO2 pour signer un document électronique. Cette nouvelle approche proposée peut être utilisée pour une signature face à face (en locale) ou à distance (en ligne). Le prototype développé pour la mise en œuvre de notre approche a été validé auprès d’usagers types (membres clients et conseillers) dans une entreprise. / In this digital era, the use of paper documents is impractical and inefficient, which motivates companies to move towards the use of electronic documents (or e-docs). This desire to innovate towards a paperless operation can improve the efficiency and quality of public or private administration services so as to speed up their activities and at the same time better meet customer needs. However, this practice has created new needs, such as the actual digital signature of documents. In this thesis, we have proposed a new digital signature scheme using FIDO2, which happens to be a new standard for secure online authentication based on digital signatures. The fact that FIDO2 is a free standard makes it easier for software and hardware developers to implement their own products. This inspired us to use it a digital signature purpose, the idea being, to replace the challenge sent by the server with the hash of e-docs and send it to the signer’s device so that the latter signs with his private key. As with public key infrastructure, each user had a key pair, that is, a private key and a public key. A signatory must confirm their biometric identification (fingerprint, facial recognition, voice, etc.) or PIN code to access the private key stored locally on their device and sign a document. During our research, we carried out several tests with different equipment (PC, USB FIDO, Smartphone) as well as different OS (Android, iOS, Windows). The results of our tests show us that we can use FIDO2 to sign an electronic document. This proposed new approach can be used for a face-to-face (local) or remote (online) signature. The prototype developed for the implementation of our approach has been validated with typical users (member-clients and advisers) in a company.

Nous étudions la modélisation et la validation hors-ligne des applications temps-réel en environnement monoprocesseur, qui prend explicitement en compte l'échange des messages, le partage des ressources et les instructions conditionnelles entre les tâches. Notre objectif est de mettre en évidence l'impact de ces paramètres sur l'analyse des applications. Classiquement, ces applications sont modélisées de façon linéaire, en encapsulant les blocs conditionnels, et les séquences sont utilisées pour leur validation. Nous proposons une approche de modélisation et de validation arborescente, qui permet de considérer de façon explicite les blocs conditionnels, et qui utilise les arbres d'ordonnancement pour la validation. Nous comparons ensuite ces deux approches, et prouvons que les premières sont parfois trop pessimistes, c'est à dire qu'elles peuvent conduire à déclarer certaines applications comme non ordonnançables, alors qu'en réalité elles le sont. Nous commençons par construire un générateur d'arbres d'ordonnancement valides. La complexité du générateur étant exponentielle en fonction du nombre de tâches, cette approche est di cile à mettre en ÷uvre dans la pratique. Nous proposons donc une approche de modélisation bas ée sur les réseaux de Petri. Ce réseau sera utilisé pour générer les arbres valides, par construction du graphe de marquages, et la complexité pourra être réduite grâce à des heuristiques.