Le formalisme AltaRica, développé au LaBRI conjointement avec des industriels, permet d'analyser un même système grâce à plusieurs méthodes différentes (arbres de défaillances, réseaux de Petri, chaînes de Markov) afin d'effectuer des études de sûreté de fonctionnement. Ces méthodes sont outillées par des outils industriels. Cette thèse a eu pour but de développer un outil de vérification formelle basé sur une structure de données symbolique, les diagrammes de décision binaires, qui permet de représenter de manière compacte les systèmes de transitions. Cet outil a été doté d'un langage de spécification très expressif, le mu-calcul de Park, qui est la logique du premier ordre étendue par des points fixes sur les relations. Ce mémoire décrit la logique de spécification employée dans le vérificateur de modèles (Mec 5) que nous avons développé, le formalisme AltaRica et les extensions apportées au langage AltaRica durant cette thèse. Ensuite certains aspects de l'implémentation de Mec 5 sont décrits, comme l'architecture du logiciel et certains composants essentiels dont le module de gestion des diagrammes de décision binaires. Puis, une solution élégante et très générique du problème de la synthèse de contrôleurs est décrite, qui permet de spécifier des objectifs de contrôle arborescents et constitue donc une extension naturelle du cadre proposé par Ramadge et Wonham. Cette méthode ramène le problème de la synthèse de contrôleurs à un problème de calcul de stratégies gagnantes. Enfin, une méthode de calcul des stratégies gagnantes dans un jeu de parité est proposée et il est montré que Mec 5 peut calculer de telles stratégies.

Cette thèse propose un cadre afin de modéliser, vérifier et générer des allocations de fonctions d'un système embarqué sur des ressources avioniques. Ce cadre est fondé sur l'utilisation du langage Altarica pour décrire formellement la propagation des défaillances au sein d'un système embarqué, sur l'utilisation de techniques de vérification tel que le "model-checking" et la génération d'arbre de défaillances et sur les techniques de résolution de contraintes. Les travaux sont illustrés par deux études de cas: l'allocation de ressources de calcul et de communication à une fonction de "suivi de terrain" d'un avion de chasse, le placement des équipements d'un système hydraulique au sein d'un avion en tenant compte de risques tels que l'éclatement d'un pneu ou d'un réacteur.

Les logiciels sont désormais un des composants essentiels des équipements modernes. Ils sont responsables de leur sûreté et fiabilité. Par sûreté, nous entendons que le système garantit que ''rien de dangereux n'arrive jamais''. Ce type de propriété peut se réduire à un problème d'accessibilité: pour démontrer la propriété il suffit de démontrer qu'un ensemble d'états ''dangereux'' ne sont pas atteignables. Ceci est particulièrement important pour les systèmes critiques: les systèmes dont une défaillance peut mettre en jeu des vies humaines ou l'économie d'une entreprise. Afin de garantir un niveau de confiance suffisant dans nos équipements modernes, un grand nombre de méthodes de vérification ont étaient proposées. Ici nous nous intéressons au model checking: une méthode formelle de vérification de système. L'utilisation de méthodes de model checking et de model checker permet d'améliorer les analyses de sécurité des systèmes critiques, car elles permettent de garantir l'absence de bug vis-à-vis des propriétés spécifiées. De plus, le model checking est une méthode automatique, ceci permet à des utilisateurs non-spécialistes d'utiliser ces outils. Ceci permet l'utilisation de cette méthode à une grande communauté d'utilisateur dans différents contextes industriels. Mais le problème de l'explosion combinatoire de l'espace des états reste une difficulté qui limite l'utilisation de cette méthode dans un contexte industriel. Nous présentons deux méthodes de vérification de modèle AltaRica. La première méthode présente un algorithme CEGAR qui élague des états de l'abstraction, ce qui permet d'utiliser une sous-approximation de l'espace des états d'un système. Grâce à l'utilisation de cette sous-approximation, nous pouvons détecter des contre-exemples simples, utiliser des méthodes de réduction pour éliminer des états abstraits, ce qui nous permet de minimiser le coût de l'analyse des contre-exemples, et guider l'exploration de l'abstraction vers des contre-exemples qui sont plus pertinents. Nous avons développé cet algorithme dans le model checker Mec 5, et les expérimentations réalisées ont confirmé les améliorations attendues.

Les travaux effectués durant cette thèse portent sur la spécification, l'analyse et l'application de systèmes a événements discrets pour la modélisation de processus biologiques stochastiques en biologie des systèmes. Le point de départ de cette thèse est le langage de modélisation AltaRica, que nous étendons afin de permettre de décrire des événements temporisés selon des distributions de probabilités quelconques (dégénérées, discrètes et continues). Nous définissons ensuite la sémantique de ce langage en terme d'automates de mode stochastiques et présentons trois opérations de compositions permettant de modéliser des systèmes hiérarchiques avec événements synchronisés et partage de valeurs via un mécanisme de connexion. Nous donnons ensuite au automates de mode stochastiques une sémantique en termes de systèmes de transitions dont les transitions sont étiquetées par des distributions de probabilités et des probabilités de transitions instantanées. Nous caractérisons ensuite 6 sous classes de ces systèmes de transitions et donnons pour chacune de ces classes un algorithme de simulation ainsi qu'une mesure de probabilité sur les chemins finis. Nous montrons que pour certaines de ces classes, notre sémantique est conforme avec les mesures de probabilité de chemin usuellement associées aux chaînes de Markov a temps discret, a temps continu et aux processus semi-Markoviens généralisés. Nous abordons ensuite le problème de la réutilisation de modèles continus existant dans un système discret. Nous donnons une méthode d'abstraction permettant de représenter un ensemble de trajectoires bornées ou non d'un modèle continu sous forme d'un système de transition stochastique fini. A travers des exemples tirés de la littérature, nous montrons que notre abstraction préserve les propriétés "qualitatives" (par exemple oscillations, hystérie) des modèles continus et qu'une comparaison entre trajectoires basée sur leurs représentations en termes de systèmes de transitions permet de regrouper les trajectoires en fonction de comportements qualitatifs plus fins que ceux permis par la théorie des bifurcations. Finalement, nous étudions a l'aide de ces modèles des processus liés a la division cellulaire chez les levures. En particulier, nous définissons un modèle pour le vieillissement cellulaire dans une population de levure où le comportement individuel d'une cellule est régi par une équation différentielle ordinaire et où le processus de division est régi par un système de transition. Nous montrons a l'aide de ce modèle que la survie d'une population de levure de type Schizosaccharomyces Pombe, qui se divisent par une fission médiane, n'est possible que grâce a un mécanisme de distribution non symétrique des dégâts oxydatifs entre la progéniture et la cellule souche. Cette hypothèse fut validée expérimentalement lors d'une collaboration avec le laboratoire de micro-biologie de Göteborg. / A general goal of systems biology is to acquire a detailed understanding of the dynamics of living systems by relating functional properties of whole systems with the interactions of their constituents. Often this goal is tackled through computer simulation. A number of different formalisms are currently used to construct numerical representations of biological systems, and a certain wealth of models is proposed using ad hoc methods. There arises an interesting question of to what extent these models can be reused and composed, together or in a larger framework. In this thesis, we propose BioRica as a means to circumvent the difficulty of incorporating disparate approaches in the same modeling study. BioRica is an extension of the AltaRica specification language to describe hierarchical non-deterministic General Semi-Markov processes. We first extend the syntax and automata semantics of AltaRica in order to account for stochastic labeling. We then provide a semantics to BioRica programs in terms of stochastic transition systems, that are transition systems with stochastic labeling. We then develop numerical methods to symbolically compute the probability of a given finite path in a stochastic transition systems. We then define algorithms and rules to compile a BioRica system into a stand alone C++ simulator that simulates the underlying stochastic process. We also present language extensions that enables the modeler to include into a BioRica hierarchical systems nodes that use numerical libraries (e.g. Mathematica, Matlab, GSL). Such nodes can be used to perform numerical integration or flux balance analysis during discrete event simulation. We then consider the problem of using models with uncertain parameter values. Quantitative models in Systems Biology depend on a large number of free parameters, whose values completely determine behavior of models. Some range of parameter values produce similar system dynamics, making it possible to define general trends for trajectories of the system (e.g. oscillating behavior) for some parameter values. In this work, we defined an automata-based formalism to describe the qualitative behavior of systems’ dynamics. Qualitative behaviors are represented by finite transition systems whose states contain predicate valuation and whose transitions are labeled by probabilistic delays. We provide algorithms to automatically build such automata representation by using random sampling over the parameter space and algorithms to compare and cluster the resulting qualitative transition system. Finally, we validate our approach by studying a rejuvenation effect in yeasts cells population by using a hierarchical population model defined in BioRica. Models of ageing for yeast cells aim to provide insight into the general biological processes of ageing. For this study, we used the BioRica framework to generate a hierarchical simulation tool that allows dynamic creation of entities during simulation. The predictions of our hierarchical mathematical model has been validated experimentally by the micro-biology laboratory of Gothenburg