Les spécifications formelles et la modélisation par objets sont considérés comme deux champs ayant un fort potentiel d'influence sur l'avenir du génie logiciel. Dans un premier temps, nous étudions cette affirmation en dégageant les caractéristiques essentielles du développement du logiciel. L'intersection des deux champs est un domaine nouveau et prometteur. Nous en étudions les différents variantes et nous synthétisons les choix faits dans les méthodes formelles à objets actuelles. Dans ce contexte, cette thèse propose une méthode de spécification et de conception de composants logiciels destinée à faciliter la formalisation, automatiser partiellement le processus de conception, permettre le contrôle et la réutilisation des classes avant implantation. L'accent est mis sur la séparation entre les niveaux de description pour clarifier le processus de conception et sur l'uniformisation à l'intérieur des niveaux de description pour assurer la cohérence. Deux modèles sont décrits. Le premier modèle, dit des types abstraits graphiques, définit les composants suivant un axe dynamique et suivant un axe fonctionnel. La modélisation dynamique, naturelle pour des objets est donnée en termes d'automates d'états finis gardés. Outre sa lisibilité, le modèle dynamique a pour intérêt majeur la construction guidée de spécifications algébriques, support de l'axe fonctionnel. Le second modèle, dit des classes formelles, est un modèle général, formel et abstrait pour la conception à objets. Basé sur les types abstraits algébriques, il permet le raisonnement abstrait et ma mise en oeuvre dans différents langages de programmation à objets. Les modèles présentés sont indépendants et sont adaptables dans d'autres méthodes de développement. Nous proposons une méthode de transition entre ces deux modèles, qui favorise le contrôle et la réutilisation des spécifications. Plusieurs outils d'écriture et de preuve sont communs aux deux modèles et nous insistons sur l'ouverture vers d'autres environnements de spécification.

Cette thèse traite de la vérification formelle de systèmes critiques où la correction du système dépend du respect des contraintes temporelles. La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réel dans le contexte de l’industrie aéronautique et spatiale. La deuxième partie décrit notre méthode d’exploitation des symétries pour les réseaux de Petri temporels. Nous définissons un opérateur de composition symétrique pour la construction de réseaux. Puis nous proposons des solutions pour la construction d’espaces d’états quotients par la relation d’équivalence induite par les symétries. Notre méthode s’applique aux réseaux de Petri, temporels ou non. A notre connaissance il s’agit de la première méthode applicable aux réseaux de Petri temporels. Des résultats expérimentaux encourageants sont présentés. / This thesis deals with formal verification of critical systems where the system’s correction depends on compliance with time constraints. The first part studies the formal modeling and verification by model-checking of realtime systems in the context of the aerospace industry. The second part describes our method for symmetry reduction of Time Petri Net. We define a symmetric composition operator for building Net. Then we present our solution for construction of quotients of the state spaces by the equivalence relation induced by symmetries. Our method applies to Petri nets, temporal or not, but to our knowledge this is the first methodology for Time Petri Nets. Encouraging experimental results are presented.

Partie de faits empiriques observés au Burkina Faso, cette thèse aborde la question des déterminants de la qualité de l’éducation. Bien que la Loi d’orientation de l’éducation ait définie une vision holistique, le système éducatif de ce pays est cloisonné en formel, non formel et informel. Le système formel est dominant mais peu performant. Le système non formel est marginalisé mais est porteur de qualité. Qu’est-ce qui explique cette qualité du non formel malgré sa marginalisation ? Comme réponse provisoire, l’auteur fait appel à l’ingénierie de formation, procède par une triangulation de théories interactionnistes pour cerner les cinq formules éducatives constituant l’objet d’observation central de la thèse. La recherche révèle deux phases dans le développement des formules éducatives: une phase d’investigation où les acteurs vivent des moments d’idéation, d’analyse puis de conception portant sur les solutions à trouver aux problèmes éducatifs; Une phase de mise en œuvre où ils réalisent le projet éducatif validé, suivent et évaluent activités, résultats et procèdent à leur diffusion. Positionnée dans l’éducation non formelle, l’ingénierie de formation s’enrichit de deux nouvelles étapes: l’idéation ou l’émergence de la commande sociale en éducation, et la diffusion, moyen de réingénierie des formules éducatives. En somme, la recherche aboutit au fait que le développement des alternatives éducatives mobilise une ingénierie de formation, source de leur qualité. Cette qualité influence le système formel. Ainsi, les systèmes formel et non formel échangent des approches et pratiques inscrivant le champ éducatif dans une logique de transaction sociale et de métissage. / Part of empirical facts observed in Burkina Faso, this thesis addresses the question of the determinants of the quality of education. Although the Education Orientation Law has defined a holistic vision, the education system in Burkina Faso is partitioned into formal, non-formal and informal. The formal system is dominant but inefficient. The non-formal system is marginalized but carries quality. What explains this quality of non-formal despite its marginalization? As an interim response, the author uses training engineering, proceeds by a triangulation of interactionist theories to identify the five educational formulas constituting the central observation object of the thesis.The research reveals two phases in the development of educational formulas: an investigation phase where the actors live moments of ideation, analysis and conception concerning the solutions to be found to the educational problems; An implementation phase where they carry out the validated educational project, monitor and evaluate activities, results and disseminate them. Positioned in non-formal education, training engineering is enriched by two new stages: ideation or the emergence of social demand in education, and dissemination, a means of re-engineering educational formulas.In sum, the research leads to the fact that the development of educational alternatives mobilizes a training engineering that ensures them a quality education. This quality influences the formal education system. Thus, the formal and non-formal systems exchange approaches and practices that place the educational field in a logic of social transaction and miscegenation.

Un logiciel pour les solutions formelles d'équations différentielles linéaires d'ordre 2 au voisinage de points singuliers est présenté. Pour les équations d'ordre quelconque on donne une version modifiée de l'algorithme de newton. Un algorithme permettant d'obtenir une base de solutions asymptotiques d'une équation récurrente linéaire à coefficients polynomiaux est ensuite présenté. Ceci mène à l'étude des systèmes linéaires aux différences à coefficients séries de factorielles

L'objet de cette thèse est d'étudier les capacités du système Coq à mélanger démonstrations et programmes en pratique en essayant d'y implémenter une part du programme Kenzo, un outil de calcul formel en algèbre homologique. À cet effet, nous travaillons sous trois contrainte: nous voulons essayer de lire le programme comme une démonstration avec un contenu calculatoire, ces démonstrations doivent calculer efficacement et nous cherchons à éviter de dupliquer des morceaux de démonstration. Nous montrons dans un premier temps comment le soucis d'efficacité conduit à reconsidérer certains aspects des mathématiques traditionnelle. Nous proposons une abstraction catégorielle adaptée, qui répond à la fois à un soucis de clareté et au besoin de partager les démonstration quand c'est possible. Cette abstraction, bien que différente des propositions traditionnelles, permet de formuler les notions d'algèbre homologique dans un style proche de celui de Kenzo. Nous proposons par ailleurs des modifications au programme de Coq pour rendre les démonstrations plus confortables, et pour permettre d'écrire des programmes plus efficaces. La première modification permet d'utiliser des tactiques plus fines, souvent nécessaire quand l'utilisation des types dépendents se fait commune. La seconde permet d'utiliser les capacité du processeur pour faire des calculs plus efficaces sur des entiers. Pour finir nous proposons quelques pistes pour améliorer le partage et la clareté du code. Malheureusement, nous nous heurtons aux limites du système. Nous montrons ainsi que Coq ne tiens pas forcément ses promesses et qu'il y aura besoin de travaux théoriques pour comprendre comment lever ces limites.

Les technologies actuelles permettent l'intégration sur une même puce de systèmes complexes (SoCs) qui sont composés de blocs préconçus (IPs) pouvant être interconnectés grâce à un réseau sur la puce (NoCs). De manière générale, les IPs sont validés par diverses techniques (simulation, test, vérification formelle) et le problème majeur reste la validation des infrastructures des communications. Cette thèse se concentre sur la vérification formelle des réseaux sur puce à l'aide d'un outil de preuve automatique, le démonstrateur de théorèmes ACL2. Un méta-modèle pour les réseaux sur puce a été développé et implémenté dans ACL2. Il satisfait des propriétés de correction générique, conséquences logiques d'un ensemble d'obligations de preuve sur les constituants principaux du réseau (topologie, routage, technique de commutation,...). La preuve de correction pour une instance spécifique de réseau sur puce est alors réduite à la vérification de ces obligations de preuve. Cette thèse poursuit les travaux entrepris dans ce domaine en étendant ce méta-modèle dans plusieurs directions : prise en compte plus fine de la modélisation temporelle, du contrôle de flux, des mécanismes de priorités,... Les résultats sont démontrés sur plusieurs réseaux actuels : Hermes (Université fédérale du Rio Grande do Sul, Brésil et LIRMM) et Nostrum (Royal Institute Of Technology, Suéde).

Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérifi cation formelle de systèmes réactifs nis sur architectures parallèles. Ces travaux se basent sur les techniques de véri cation par model checking. Notre approche cible des architectures multi-processeurs et multi-coeurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement. Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois effi caces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d'espaces d'états en parallèle ; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs. Parallèlement à la défi nition de nouveaux algorithmes de model checking pour machines multi-coeurs, nous nous intéressons également aux algorithmes de vérifi cation probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérifi cation d'un système. La véri fication probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d'une faible probabilité de ne pas être exhaustif ; il s'agit donc d'une stratégie permettant de répondre au problème de l'explosion combinatoire.

Les architectures des systèmes sur puce (System-on-Chip, SoC) actuelles intègrent de nombreux composants différents tels que les processeurs, les accélérateurs, les mémoires et les blocs d'entrée/sortie, certains pouvant contenir des caches. Vu que l'effort de validation basée sur la simulation, actuellement utilisée dans l'industrie, croît de façon exponentielle avec la complexité des SoCs, nous nous intéressons à des techniques de vérification formelle. Nous utilisons la boîte à outils CADP pour développer et valider un modèle formel d'un SoC générique conforme à la spécification AMBA 4 ACE récemment proposée par ARM dans le but de mettre en œuvre la cohérence de cache au niveau système. Nous utilisons une spécification orientée contraintes pour modéliser les exigences générales de cette spécification. Les propriétés du système sont vérifié à la fois sur le modèle avec contraintes et le modèle sans contraintes pour détecter les cas intéressants pour la cohérence de cache. La paramétrisation du modèle proposé a permis de produire l'ensemble complet des contre-exemples qui ne satisfont pas une certaine propriété dans le modèle non contraint. Notre approche améliore les techniques industrielles de vérification basées sur la simulation en deux aspects. D'une part, nous suggérons l'utilisation du modèle formel pour évaluer la bonne construction d'une unité de vérification d'interface. D'autre part, dans l'objectif de générer des cas de test semi-dirigés intelligents à partir des propriétés de logique temporelle, nous proposons une approche en deux étapes. La première étape consiste à générer des cas de tests abstraits au niveau système en utilisant des outils de test basé sur modèle de la boîte à outils CADP. La seconde étape consiste à affiner ces tests en cas de tests concrets au niveau de l'interface qui peuvent être exécutés en RTL grâce aux services d'un outil commercial de génération de tests dirigés par les mesures de couverture. Nous avons constaté que notre approche participe dans la transition entre la vérification du niveau interface, classiquement pratiquée dans l'industrie du matériel, et la vérification au niveau système. Notre approche facilite aussi la validation des propriétés globales du système, et permet une détection précoce des bugs, tant dans le SoC que dans les bancs de test commerciales. / State-of-the-art System-on-Chip (SoC) architectures integrate many different components, such as processors, accelerators, memories, and I/O blocks. Some of those components, but not all, may have caches. Because the effort of validation with simulation-based techniques, currently used in industry, grows exponentially with the complexity of the SoC, this thesis investigates the use of formal verification techniques in this context. More precisely, we use the CADP toolbox to develop and validate a generic formal model of a heterogeneous cache-coherent SoC compliant with the recent AMBA 4 ACE specification proposed by ARM. We use a constraint-oriented specification style to model the general requirements of the specification. We verify system properties on both the constrained and unconstrained model to detect the cache coherency corner cases. We take advantage of the parametrization of the proposed model to produce a comprehensive set of counterexamples of non-satisfied properties in the unconstrained model. The results of formal verification are then used to improve the industrial simulation-based verification techniques in two aspects. On the one hand, we suggest using the formal model to assess the sanity of an interface verification unit. On the other hand, in order to generate clever semi-directed test cases from temporal logic properties, we propose a two-step approach. One step consists in generating system-level abstract test cases using model-based testing tools of the CADP toolbox. The other step consists in refining those tests into interface-level concrete test cases that can be executed at RTL level with a commercial Coverage-Directed Test Generation tool. We found that our approach helps in the transition between interface-level and system-level verification, facilitates the validation of system-level properties, and enables early detection of bugs in both the SoC and the commercial test-bench.

Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérification formelle de systèmes réactifs finis sur architectures parallèles. Ces travaux se basent sur les techniques de vérification model checking. Notre approche cible des architectures multi-processeurs et multi-cœurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement.Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois efficaces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d’espaces d'états en parallèle; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs.Parallèlement à la définition de nouveaux algorithmes de model checking pour machines multi-cœurs, nous nous intéressons également aux algorithmes de vérification probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérification d’un système. La vérification probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d’une faible probabilité de ne pas être exhaustif; il s’agit donc d’une stratégie permettant de répondre au problème de l’explosion combinatoire / In this thesis, we propose and study new algorithms and data structures for model checking finite-state, concurrent systems. We focus on techniques that target shared memory, multi-cores architectures, that are a current trend in computer architectures.In this context, we present new algorithms and data structures for exhaustive parallel model checking that are as efficient as possible, but also ``friendly'' with respect to the work-sharing policies that are used for the state space generation (e.g. a work-stealing strategy): at no point do we impose a restriction on the way work is shared among the processors. This includes both the construction of the state space as the detection of cycles in parallel, which is is one of the key points of performance for the evaluation of more complex formulas.Alongside the definition of enumerative, model checking algorithms for many-cores architectures, we also study probabilistic verification algorithms. By the term probabilistic, we mean that, during the exploration of a system, any given reachable state has a high probability of being checked by the algorithm. Probabilistic verification trades savings at the level of memory usage for the probability of missing some states. Consequently, it becomes possible to analyze part of the state space of a system when there is not enough memory available to represent the entire state space in an exact manner

Dans un contexte où l'insertion socioprofessionnelle et culturelle des jeunes représente un enjeu majeur, il est opportun de considérer des interventions visant à aider des jeunes adultes qui vivent en situation de précarité. De fait, cette recherche vise à mieux comprendre comment l'apprentissage expérientiel réalisé dans un projet d'éducation non formelle, centré sur les arts et s'adressant à des jeunes en situation de précarité, peut contribuer au développement des participants. L'apport particulier de notre enquête se situe dans l'intérêt porté aux liens entre l'expérience vécue, les apprentissages et le développement des participants. Au plan méthodologique, quelques années après la fin du projet, nous avons rencontré des anciens participants du projet Artéflux dans le cadre d'entretiens semi-directifs. Leur témoignage constitue la pierre angulaire des résultats de recherche que nous avons étudiés en effectuant une analyse thématique. Les résultats nous indiquent que plusieurs apprentissages signifiants ont été amorcés durant le projet Artéflux.