Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité modifiée est introduite et étudiée. Un codage imprédicatif d'une large classe de définitions inductives est proposé.

La fiabilité des logiciels est un facteur critique de notre société~: toute panne, tout bogue, tout dysfonctionnement, perturbe la bonne marche de nos activités avec parfois des conséquences humaines, financières ou morales importantes. Contrairement à d'autres domaines industriels plus anciens, la démarche qualité en informatique n'en est encore qu'à ses débuts. Il est couramment convenu comme normal qu'un ordinateur perde un fichier ou que l'installation d'un nouveau logiciel en rende un autre inutilisable. Cependant, dans des domaines précis (banque, systèmes embarqués, médecine, etc.), dits critiques, on ne peut se permettre d'avoir un système défaillant~: une phase importante du développement logiciel est celle de la validation durant laquelle le système est analysé afin de garantir qu'il respecte certaines exigences de fiabilité. Cette phase de validation fait appel à deux approches complémentaires, le test et la vérification. Les travaux présentés dans cette habilitation concernent majoritairement la verification par la technique dite de "model-checking". Une première partie montre des techniques originales pour la vérification de protocoles de sécurité. D'autres travaux, plus théoriques, portent sur l'accélération de relations de semi-commutation ainsi que sur la vérification de propriétés non fonctionnelles. Enfin, des résultats sur la génération aléatoire de structures complexes sont développés dans le contexte du test à partir de modèles et du test de performances.

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

Ce travail présente une modélisation originale de la notion de test de programmes, à partir de la logique égalitaire du premier ordre. Plusieurs applications concernant notamment les types abstraits algébriques et la validation automatique de spécifications sont proposées.<br /><br />À partir d'une étude intuitive de la notion de test, nous dégageons la notion de processus de test, fondée sur le principe du couplage.<br /><br />Nous définissions la notion de jeu de tests sur un contexte de test. Ses propriétés mathématiques sont étudiées: fiabilité, validité, absence de biais, acceptabilité. Plusieurs ordres partiels sont définis: finesses absolue et asymptotique. Les équivalences déduites donnent lieu à des théorèmes importants.<br /><br />Une méthode de pratique de test est construite à partir de cette théorie et appliquée à un programme de tri. Cette méthode est particulièrement adaptée à la validation d'un axiome d'un type abstrait algébrique sur une algèbre. Un exemple est présenté, et l'implantation d'un outil expérimental utilisant cette méthode, réalisé à titre expérimental, est décrite.<br /><br />De nombreuses annexes sont jointes: un résumé des travaux antérieurs sur le problème, une bibliographie sur la validation des programmes par test, une introduction à la logique du premier ordre et un listage partiel de l'implantation réalisée.

Ce travail porte sur le test fonctionnel, basé sur les spécifications et complètement automatisé des logiciels synchrones. Nous proposons une extension des techniques de test proposées par l'outil Lutess afin de prendre en compte des logiciels qui comportent des entrées/sorties numériques. La génération de données de test est abordée en s'appuyant sur les techniques de programmation par contraintes.<br /><br />Nous avons redéfini les méthodes de guidage de la génération afin de les adapter à ce nouveau contexte numérique. Ainsi, nous proposons, en plus de la génération aléatoire respectant les propriétés invariantes de l'environnement, le guidage du test basé sur des probabilités conditionnelles ou sur des propriétés de sûreté. Des connaissances partielles sur le logiciel, que nous appelons hypothèses de test, peuvent être intégrées dans le processus de génération et contribuer à l'amélioration du pouvoir de détection de fautes du guidage par propriétés de sûreté. Enfin, nous permettons l'utilisation conjointe de plusieurs techniques de guidage dans une même spécification.<br /><br />Une implémentation de ces méthodes de test a été réalisée dans une nouvelle version de l'outil, que nous appelons Lutess V2. L'applicabilité de ces méthodes dans un contexte plus réaliste a été évaluée sur une étude de cas significative d'un contrôleur de niveau d'eau dans une chaudière.

Ces travaux s'intéressent aux projets de développement visant l'informatisation des situations de travail complexes où les facteurs humains et organisationnels ont un rôle important et où les enjeux de sécurité sont considérables. De tels projets impliquent la participation d'intervenants provenant de domaines différents tels que les utilisateurs, les représentants utilisateur, les responsables des systèmes d'information, les ergonomes, les concepteurs. Dans ce contexte, la prise en compte des facteurs humains et organisationnels reste encore insuffisante pour la conception des systèmes informatiques, du fait, d'une part des limites des méthodes et modèles proposés par le Génie Logiciel et l'Interaction Homme-Machine pour l'analyse des situations de travail complexes, et d'autre part des collaborations également insuffisantes entre les intervenants au cœur de la conception (ex : ergonomes et concepteurs).<br />Une approche basée sur l'exploitation des techniques de modélisation du GL et de l'IHM comme solutions de modélisation communes pour la création de supports de travail entre intervenants de projet, a été proposée. <br />Une solution de modélisation pour la représentation des problèmes ergonomiques complexes et des recommandations issus des inspections ergonomiques a également été proposée dans le cadre de la thèse. Il s'agit de la méthode ErgoPNets qui combine les réseaux de Petri et l'utilisation de critères ergonomiques.

Nous proposons dans cette thèse une démarche permettant de décrire un DSML (Domain Specific Modeling Language) et les outils nécessaires à l'exécution, la vérification et la validation des modèles. La démarche que nous proposons offre une architecture générique de la syntaxe abstraite du DSML pour capturer les informations nécessaires à l'exécution d'un modèle et définir les propriétés temporelles qui doivent être vérifiées. Nous nous appuyons sur cette architecture pour expliciter la sémantique de référence et l'implanter. Plus particulièrement, nous étudions les moyens :<br />- d'exprimer et de valider la définition d'une traduction vers un domaine formel dans le but de réutiliser des outils de model-checking.<br />- de compléter la syntaxe abstraite par le comportement; et profiter d'outils génériques pour pouvoir simuler les modèles construits.<br />Enfin, de manière à valider les différentes sémantiques implantées vis-à-vis de la sémantique de référence, nous proposons un cadre formel de métamodélisation.

Dans le cadre de cette thèse, nous nous proposons d'étudier le développement et la validation de systèmes dans un contexte temps réel asynchrone. On a choisi d'utiliser le langage AADL pour ses spécificités issues de l'avionique, domaine proche du spatial, et pour la précision de la description de son modèle d'exécution. Le travail de cette thèse se divise en deux axes principaux : d'une part, on étudie l'utilisation du langage AADL dans le cadre du développement d'un logiciel de vol ; et d'autre part, on présente une version réduite du langage AADL, et la définition formelle de son modèle d'exécution à l'aide du langage TLA+. L'objectif de la première partie est d'envisager l'utilisation d'AADL dans le cadre d'un processus de développement existant dans le domaine du spatial. Dans cette partie, on a cherché à identifier des motifs de conceptions récurrents dans les logiciels de vol. Enfin, on étudie l'expression en AADL des différents éléments de ce processus de développement. La seconde partie comporte la définition d'un mini AADL suffisant pour exprimer la plupart des concepts de parallélisme, de communication et de synchronisation qui caractérisent AADL. La partie formalisation est nécessaire afin de pouvoir vérifier des propriétés dynamiques. En effet, la définition formelle du modèle d'exécution permet de décrire le comportement attendu des modèles AADL. Une fois ce modèle défini, on peut à l'aide d'un vérificateur de modèles (model-checker) animer une modélisation AADL ou aborder la vérification de propriétés dynamiques. Cette étude a par ailleurs été menée dans le cadre de la standardisation du langage AADL.

La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Les deux principaux outils industriels dans ce domaine sont Simulink et Lustre/Scade. Ces deux outils possèdent de nombreuses fonctionnalités comme un moteur de simulations, des générateurs de tests ou de code. Cependant, Simulink est, dans la majorité des cas, utilisé pour la conception de systèmes embarqués et ceci parce qu'il a une expressivité plus importante. Il est capable de modéliser et de simuler des systèmes à temps continu, à temps discret et un mélange des deux, c'est-à-dire des systèmes hybrides. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications est un défi industriel et scientifique important pour la validation des logiciels embarqués. De plus, l'utilisation de méthodes formelles, au plus tôt dans le cycle de développement, est un challenge essentiel dans l'industrie afin de réduire les coûts liés à la correction de bogues.<br /><br />Dans cette thèse, nous définissons une analyse statique par interprétation abstraite de modèles Simulink. Nous appelons cette analyse Simulation Abstraite. L'objectif de la Simulation Abstraite est de fournir un critère de correction des comportements numériques des exécutions des modèles Simulink. Ces simulations sont souvent utilisées pour valider les systèmes modélisés, mais elles sont plus proches de l'activité de tests que celle de la preuve. En conséquence, elles ne permettent pas de valider vis-à-vis des spécifications un système modélisé avec Simulink. La Simulation Abstraite fournit un critère de correction dans le sens que les comportements des modèles Simulink représentent au mieux les comportements du monde réel.<br /><br />Nous supposons que le modèle mathématique, représenté par un modèle Simulink, est correcte vis-à-vis du monde réel. Notre objectif est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs. Le critère de correction des modèles à temps continu est obtenu en évaluant la distance séparant les résultats des méthodes d'intégration numérique, utilisées par le moteur de simulations, des résultats obtenus par une méthode d'intégration numérique garantie. Le critère de correction des modèles à temps discret est donné par l'utilisation du domaine numérique abstrait des nombres flottants avec erreurs différentiées. Ce nouveau domaine numérique est issu de la combinaison du domaine des flottants avec erreurs et la méthode de différentiation automatique permettant d'avoir une meilleure abstraction des erreurs. Nous définissons également une abstraction d'un domaine des séquences utilisant les partitions d'un ensemble. Nous sommes ainsi en mesure de représenter des simulations infinies d'une manière finie. L'ensemble de ces domaines permet alors d'estimer les erreurs introduites par les traitements numériques présents lors des simulations. Nous obtenons alors une méthode de validation des comportements numériques des systèmes embarqués modélisés en Simulink.

Cette thèse propose une Démarche de Vérification Formelle d'Architectures Logicielles : DVFAL. La démarche DVFAL supporte divers formalismes de description d'architectures logicielles tels que : les ADL (langages de description d'architectures), UML2.0, Symphony et des profils UML2.0 dédiés au domaine des architectures logicielles. La démarche DVFAL préconise l'ADL Wright en tant que langage formel pivot permettant de représenter des architectures logicielles décrites dans les divers formalismes. En outre, elle propose des transformations de modèles sous forme des traducteurs (Wright vers CSP de Hoare et Wright vers Ada) pour bénéficier des outils de vérification des propriétés supportant CSP et Ada tels que FDR et FLAVERS. Enfin, la démarche DVFAL propose un profil UML2.0-Wright jouant le rôle d'un langage intermédiaire entre les formalismes à base d'UML et Wright.