La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple Uppaal) et les réseaux de Petri temporisés (par exemple Tina). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non-temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec Uppaal) et vers des réseaux de Petri temporisés (pour la vérification avec Tina). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple.

Le calcul de la réponse macroscopique des agrégats polycristallins à partir des propriétés de leurs constituants est un problème important en mécanique des matériaux. Lors de la déformation plastique, les grains du matériau sont réorientés. Une texture cristallographique, responsable de l'anisotropie, peut alors se développer. Donc, la modélisation de l'évolution de la texture est importante afin de prévoir les effets d'anisotropie lors des procédés industriels.La formulation de la plasticité des polycristaux métalliques a fait l'objet de nombreuses études et différentes approches d’homogénéisation ont été proposées. En 2008, Ahzi et M'Guil ont développé un modèle viscoplastique, baptisé le modèle-phi. Ce modèle prend en compte les effets d'interaction entre les grains sans passer par la théorie de l'inclusion d’Eshelby. Dans ce travail, le modèle-phi a été appliqué à différentes structures cristallographiques et sous différentes conditions de chargement. Le mécanisme de maclage a été pris en compte. Pour le laminage des métaux CFC, la transition de texture du type cuivre au type laiton a été étudiée. L’essai de cisaillement des métaux CFC a été également étudié. Nous montrons que le modèle est capable de prédire une transition de texture de cisaillement caractérisant une gamme de métaux CFC ayant une EDE élevée/moyenne à une EDE faible. Dans une étude dédiée aux métaux CC, nous avons comparé nos résultats à ceux prédits par un modèle auto-cohérent. Nous présentons également une comparaison avec des textures expérimentales de laminage à froid issues de la littérature. Le modèle a également été étendu aux métaux HC. Nous avons simulé le comportement de déformation d’un alliage de magnésium pour différentes niveaux d'interaction inter-granulaire. Nous montrons que le modèle prédit des résultats en bon accord avec les résultats expérimentaux. / The computation of the macroscopic response of polycrystalline aggregates from the properties of their single-crystal is a main problem in materials mechanics. During the mechanical deformation processing, all the grains in the polycrystalline material sample are reoriented. A crystallographic texture may thus be developed which is responsible for the material anisotropy. Therefore, the modeling of the texture evolution is important to predict the anisotropy effects present in industrial processes. The formulation of polycrystals plasticity has been the subject of many studies and different approaches have been proposed. Ahzi and M’Guil developed a viscoplastic phi-model. This model takes into account the grains interaction effects without involving the Eshelby inclusion problems.In this thesis, the phi-model was applied to different crystallographic structures and under different loading conditions. The mechanical twinning has been taken into account in the model. The FCC rolling texture transition from copper-type to brass-type texture is studied. The shear tests in FCC metals are also studied. The predicted results are compared with experimental shear textures for a range of metals having a high SFE to low SFE. For BCC metal, we compare our predicted results with those predicted by the VPSC model. We study the slip activities, texture evolutions and the evolution of yield loci. We also present a comparison with experimental textures from literatures for several BCC metals under cold rolling tests. The model has also been extended to HCP metals. We predict the deformation behavior of the magnesium alloy for different interaction strengths. We also compare our predicted results with experimental data from literatures. We show that the results predicted by the phi-model are in good agreement with the experimental ones.