Les travaux de cette thèse contribuent au développement de méthodes automatiques de vérification et de valida-tion de systèmes informatiques, à partir de modèles. Ils sont divisés en deux parties : vérification et générationde tests.Dans la partie vérification, pour le problème du model-checking régulier indécidable en général, deux nouvellestechniques d’approximation sont définies, dans le but de fournir des (semi-)algorithmes efficaces. Des sur-approximations de l’ensemble des états accessibles sont calculées, avec l’objectif d’assurer la terminaison del’exploration de l’espace d’états. Les états accessibles (ou des sur-approximations de cet ensemble d’états)sont représentés par des langages réguliers, ou automates d’états finis. La première technique consiste à sur-approximer l’ensemble des états atteignables en fusionnant des états des automates, en fonction de critèressyntaxiques simples, ou d’une combinaison de ces critères. La seconde technique d’approximation consisteaussi à fusionner des états des automates, mais à l’aide de transducteurs. De plus, pour cette seconde technique,nous développons une nouvelle approche pour raffiner les approximations, qui s’inspire du paradigme CEGAR(CounterExample-Guided Abstraction Refinement). Ces propositions ont été expérimentées sur des exemplesde protocoles d’exclusion mutuelle.Dans la partie génération de tests, une technique qui permet de combiner la génération aléatoire avec un critèrede couverture, à partir de modèles algébriques (des grammaires algébriques, des automates à pile) est définie.Générer les tests à partir de ces modèles algébriques (au lieu de le faire à partir de graphes) permet de réduirele degré d’abstraction du modèle et donc de générer moins de tests qui ne sont pas exécutables dans le systèmeréel. Ces propositions ont été expérimentées sur la grammaire de JSON (JAvaScript Object Notation), ainsi quesur des automates à pile correspondant à des appels de fonctions mutuellement récursives, à une requête XPath,et à l’algorithme Shunting-Yard. / The thesis contributes to development of automatic methods for model-based verification and validation ofcomputer systems. It is divided into two parts: verification and test generation.In the verification part, for the problem of regular model checking undecidable in general, two new approxi-mation techniques are defined in order to provide efficient (semi-)algorithms. Over-approximations of the setof reachable states are computed, with the objective of ensuring the termination of the exploration of the statespace. Reachable states (or over-approximations of this set of states) are represented by regular languages or,equivalently, by finite-state automata. The first technique consists in over-approximating the set of reachablestates by merging states of automata, based on simple syntactic criteria, or on a combination of these criteria.The second approximation technique also merges automata states, by using transducers. For the second tech-nique, we develop a new approach to refine approximations, inspired by the CEGAR paradigm (for Counter-Example-Guided Abstraction Refinement). These proposals have been tested on examples of mutual exclusionprotocols.In the test generation part, a technique that combines the random generation with coverage criteria, fromcontext-free models (context-free grammars, pushdown automata) is defined. Generate tests from these mo-dels (instead of doing from graphs) reduces the model abstraction level, and therefore allows having moretests executable in the real system. These proposals have been tested on the JSON grammar (JavaScript ObjectNotation), as well as on pushdown automata of mutually recursive functions, of an XPath query, and of theShunting-Yard algorithm.

Un nouveau modèle de turbulence adapté aux écoulements turbulents soumis à laflottabilité a été développé en utilisant la configuration du canal plan vertical différentiellementchauffé comme référence. L’étude des DNS disponibles pour chacun des régimes de convection amontré les défauts des relations constitutives classiques conduisant à la mauvaise représentationdes écoulements de convection naturelle. Ces modèles ne prennent en compte ni le couplage deschamps thermique et dynamique ni l’anisotropie de l’écoulement, tout deux induits par la flottabilité.Une approche algébrique a donc été utilisées. L’hypothèse d’équilibre local a été validéedans une large partie du canal sauf dans la région de paroi et au voisinage d’un gradient devitesse nul, quel que soit le régime de convection. Les modèles homogènes et pariétaux pour lescorrélations de pression ont été étudiés et sélectionnés. Deux modèles EARSM et EAHFMprenant en compte les termes de flottabilité ont été développés. Ces modèles intègrent aussi destraitements spécifiques à la paroi reposant sur la pondération elliptique. Ils sont couplés à unmodèle corrigé pour mieux représenter le pic d’énergie cinétique turbulente prèsde la paroi. Le modèle complet a été confronté aux DNS sur la configuration du canal pourchacun des régimes de convection à travers des tests a priori et des calculs complets montrantdes résultats très encourageants et de meilleures prévisions que les modèles classiques. / A new turbulence model dedicated to buoyant flows is developped using the differentiallyheated vertical plane channel flow configuration as test case. For each convection regime,the examination of available DNS databases pointed out the failure of classical modeling topredict buoyant flows. Neither the coupling between thermics and dynamics nor the anisotropy,both due to the buoyancy, are considered by these models. So, algebraic models are used. Theweak equilibrium assumption is validated in a large part of the channel except in the wall regionand close to zero velocity gradient whatever the convection regime. The wall and homogeneousmodels for the pressure terms are investigated and selected. Then, an EARSM and an EAHFMare developped to include the buoyant terms. These models both include wall treatments. Theyare coupled with a model modified to improve the representation of the turbulentkinetic energy maximum close to the wall. The complete model is finally compared to theDNS on the channel flow configuration for all convection regime thanks to a priori tests andcomplete computations, showing encouraging results and better predictions than classical models