Le pré-dimensionnement se situe en amont du processus de conception d'un système : à partir d'un ensemble d'exigences, il consiste à déterminer un ensemble de solutions techniques possibles dans un espace de recherche souvent très grand et structuré par une connaissance partielle et incertaine du futur système et de son environnement. Bien avant de penser au choix définitif des composants et au dimensionnement précis du système complet, les concepteurs doivent s'appuyer sur un premier cahier des charges, des modélisations des principaux phénomènes et divers retours d'expériences pour formaliser des contraintes, faire des hypothèses simplificatrices, envisager diverses architectures et faire des choix sur des données imprécises (i.e. caractérisées sous la forme d'intervalles, de listes de valeurs possibles, etc…). Les choix effectués lors du pré-dimensionnement pouvant être très lourds de conséquences sur la suite du développement, il est primordial de détecter au plus tôt d'éventuelles incohérences et de pouvoir vérifier la satisfaction des exigences dans un contexte incertain. Dans ce travail, une méthodologie de vérification des exigences basée sur l'échange de modèles ensemblistes entre donneurs d'ordre et fournisseurs est proposée. Elle s'inscrit dans le cadre d'un paradigme de conception basé sur la réduction d'incertitudes. Après un travail portant sur la modélisation des systèmes mécatroniques, une attention particulière est portée à la prise en compte d'incertitudes déterministes sur des grandeurs continues : des techniques basées sur l'analyse par intervalles telles que la satisfaction de contraintes (CSP), des calculs d'atteignabilité pour des modèles dynamiques de connaissances ou encore l'identification de modèles de comportements ensemblistes sont ainsi mis en œuvre et développés afin d'outiller la méthodologie proposée et contribuer à répondre à l'objectif d'une vérification à couverture garantie. / The pre-sizing takes place upstream to the process of designing a system: from a set of requirements, it consists in determining a set of possible technical solutions in an often very large search space which is structured by the uncertain and partial knowledge available about the future system and its environment. Long before making the final choice and the final sizing of the system components, the designers have to use specifications, models of the main phenomena, and experience feedbacks to formalize some constraints, make simplifying assumptions, consider various architectures and make choices based on imprecise data (i.e. intervals, finite sets of possible values, etc…). The choices made during the pre-sizing process often involving strong commitments for the further developments, it is very important to early detect potential inconsistencies and to verify the satisfaction of the requirements in an uncertain context. In this work, a methodology based on the exchange of set-membership models between principals and suppliers is proposed for the verification of requirements. This methodology is fully consistent with a design paradigm based on the reduction of uncertainties. After a work dedicated to the modeling of mechatronic systems, a special attention is paid to dealing with deterministic uncertainties affecting continuous values: some techniques based on interval analysis such as constraint satisfaction (interval CSP), reachability computations for knowledge dynamic models or identification of set-membership behavioral models are used and developed, so providing a set of tools to implement the proposed methodology and contribute to reach the goal of a verification with a full and guaranteed coverage.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal.

Nous proposons dans cette thèse plusieurs contributions relatives à la vérification quantitative des systèmes. Cette discipline vise à évaluer les propriétés fonctionnelles et les performances d'un système. Une telle vérification requiert deux ingrédients : un modèle formel de représentation d'un système et une logique temporelle pour exprimer la propriété considérée. L'évaluation est alors faite par une méthode statistique ou numérique. La complexité spatiale des méthodes numériques, proportionnelle à la taille de l'espace d'états, les rend impraticables si les systèmes présentent une combinatoire importante. La méthode de comparaison stochastique basée sur les chaînes de Markov censurées réduit la mémoire occupée en restreignant l'analyse à un sous-ensemble des états de la chaîne originale. Dans cette thèse nous fournissons de nouvelles bornes dépendant de l'information disponible relative à la chaîne. Nous introduisons une nouvelle logique temporelle quantitative appelée Hybrid Automata Stochastic Logic (HASL), pour la vérification des processus stochastiques à événements discrets (DESP).HASL emploie les automates linéaires hybrides (LHA) pour sélectionner des préfixes de chemins d'exécution d'un DESP. LHA permet de collecter des informations élaborées durant la génération des chemins, fournissant ainsi à l'utilisateur un moyen d'exprimer des mesures sophistiquées. HASL supporte donc des raisonnements temporels mixés avec une analyse à base de récompenses. Nous avons aussi développé COSMOS, un outil qui implémente la vérification statistique de formules HASL pour des réseaux de Petri stochastiques. Les ateliers flexibles (FMS) ont souvent été modélisés par des réseaux de Petri. Cependant le modélisateur doit avoir une bonne connaissance de ce formalisme. Afin de faciliter cette modélisation nous proposons une méthodologie de modélisation compositionnelle orientée vers les applications qui ne requiert aucune connaissance des réseaux de Petri. / We propose in this thesis several contributions related to the quantitative verification of systems. This discipline aims to evaluate functional and performance properties of a system. Such a verification requires two ingredients: a formal model to represent the system and a temporal logic to express the desired property. Then the evaluation is done with a statistical or numerical method. The spatial complexity of numerical methods which is proportional to the size of the state space of the model makes them impractical when the state space is very large. The method of stochastic comparison with censored Markov chains is one of the methods that reduces memory requirements by restricting the analysis to a subset of the states of the original Markov chain. In this thesis we provide new bounds that depend on the available information about the chain. We introduce a new quantitative temporal logic named Hybrid Automata Stochastic Logic (HASL), for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) to select prefixes of relevant execution paths of a DESP. LHA allows rather elaborate information to be collected on-the-fly during path selection, providing the user with a powerful mean to express sophisticated measures. In essence HASL provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. We have also developed COSMOS, a tool that implements statistical verification of HASL formulas over stochastic Petri nets. Flexible manufacturing systems (FMS) have often been modelized by Petri nets. However the modeler should have a good knowledge of this formalism. In order to facilitate such a modeling we propose a methodology of compositional modeling that is application oriented and does not require any knowledge of Petri nets by the modeler.

Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d’Isabelle/HOL nous avons fourni une intégration vérifiée d’UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d’Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d’Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié. / The work presented in this thesis is a contribution to formal specification and verification methods. Formal specifications are used to describe a software, or more generally a system, in a mathematical unambiguous way. Formal verification techniques are defined on the basis of these specifications to ensure the correctness of the resulting system. However, formal methods are often not convenient and easy to use in real system developments. One of the reasons is that many specification formalisms are not rich enough to cover both data-oriented and behavioral requirements. Some specification languages were proposed to cover this kind of requirements. The Circus language distinguishes itself among these languages by a rich syntax and a fully integrated semantics.The aim of this thesis is to provide a formal environment for specifying and verifying complex systems. Specifications are written in Circus and verification is performed either by testing or by theorem proving. Similar specifications and verification environment have already been proposed. A specificity of our approach is to combine supports for proofs and test generation. Moreover, most test generation methods are based on a syntactic characterization of the studied languages. Our proposed environment is different since it is based on the denotational and operational semantics of Circus. The Isabelle/HOL theorem prover is the formal platform on top of which we built our specification and verification environment.The first main contribution of our work is the Isabelle/Circus specification and proof environment based on the denotational semantics of Circus. On top of Isabelle/HOL we provide a machine-checked shallow embedding of UTP, the semantics basis of Circus. This embedding is used to formalize the denotational semantics of the Circus language. The Isabelle/Circus environment associates to this semantics some parsing facilities that help writing Circus specifications. The proof support of Isabelle/HOL can be used directly to reason on these specifications thanks to the shallow embedding of the semantics. We present an application of the environment to refinement proofs on Circus processes (involving both data and behavioral aspects). The second main contribution is the CirTA testing framework build on top of Isabelle/Circus. The framework provides two symbolic test generation tactics that allow checking two notions of refinement: traces inclusion and deadlocks reduction. The framework is based on a shallow symbolic formalization of the operational semantics of Circus using Isabelle/Circus. Several symbolic definition and test generation tactics are defined in the CirTA framework. The formal infrastructure allows us to represent explicitly test theories as well as test selection hypothesis. Proof techniques and symbolic computations are the basis of test generation tactics. The test generation environment was used for a case study to test an existing message monitoring system. A specification of the system is written in Circus, and used to generate tests following the defined conformance relations. The tests are then compiled in forms of JUnit test methods and executed against a Java implementation of the monitoring system.This thesis is a step towards, on one hand, the development of sophisticated testing tools making use of proof techniques and, on the other hand, the integration of testing and proving within formally verified software developments.

Dans le domaine de l’aéronautique, les systèmes embarqués ont fait leur apparition durant les années 60, lorsque les équipements analogiques ont commencé à être remplacés par leurs équivalents numériques. Dès lors, l’engouement suscité par les progrès de l’informatique fut tel que de plus en plus de fonctionnalités ont été numérisées. L’accroissement permanent de la complexité des systèmes a conduit à la définition d’une architecture appelée Avionique Modulaire Intégrée (IMA pour Integrated Modular Avionics). Cette architecture se distingue des architectures antérieures, car elle est fondée sur des standards (ARINC 653 et ARINC 664 partie 7) permettant le partage des ressources de calcul et de communication entre les différentes fonctions avioniques. Ce type d’architecture est appliqué aussi bien dans le domaine civil avec le Boeing B777 et l’Airbus A380, que dans le domaine militaire avec le Rafale ou encore l’A400M. Pour des raisons de sûreté, le comportement temporel d’un système s’appuyant sur une architecture IMA doit être prévisible. Ce besoin se traduit par un ensemble d’exigences temps réel que doit satisfaire le système. Le problème exploré dans cette thèse concerne la vérification d’exigences temps réel dans les systèmes IMA. Ces exigences s’articulent autour de chaînes fonctionnelles, qui sont des séquences de fonctions. Une exigence spécifie alors une borne acceptable (minimale ou maximale) pour une propriété temporelle d’une ou plusieurs chaînes fonctionnelles. Nous avons identifié trois catégories d’exigences temps réel, que nous considérons pertinentes vis-à-vis des systèmes étudiés. Il s’agit des exigences de latence, de fraîcheur et de cohérence. Nous proposons une modélisation des systèmes IMA, et des exigences qu’ils doivent satisfaire, dans le formalisme du tagged signal model. Nous montrons alors comment, à partir de ce modèle, nous pouvons générer pour chaque exigence un programme linéaire mixte, c’est-à-dire contenant à la fois des variables entières et réelles, dont la solution optimale permet de vérifier la satisfaction de l’exigence / Embedded systems appeared in aeronautics during the 60’s, when the process of replacing analog devices by their digital counterpart started. From that time, the broad thrust of computer science advances make it possible to digitize more and more avionics functionalities. The continual increase of the complexity of these systems led to the definition of a new architecture called Integrated Modular Avionics (IMA). This architecture stands apart from previous architecture because it is based on standards (ARINC 653 and ARINC 664 part 7) which allow the sharing of computation and communication resources among avionics functions. This architecture is implemented in civil aircrafts, with Boeing B777 and Airbus A380, and in military aircrafts, with Rafale or A400M. For safety reason, the temporal behaviour of such a system must be predictable, which is expressed with a set real-time requirements. A real-time requirement specifies an upper or lower bound of a temporal property of one or several functional chains. A functional chain is a sequence of functions. In this thesis, we explore the verification of real-time requirements in IMA systems. We have identified three real-time requirements relevant to our problem : latency, freshness and consistency. We propose a model of IMA systems, and the requirements they must meet, based on the tagged signal model. Then we derive from this model, for each requirement, a mixed integer linear program whose optimal solution allows us to verify the requirement

Plusieurs outils ont été développé pour vérifier automatiquement les propriétés de sécurité sur des protocoles cryptographiques. Jusqu'à maintenant, la plupart de ces outils permettent de vérifier des propriétés de trace (ou propriétés d'accessibilité) tel que le secret simple ou l'authentification. Néanmoins, plusieurs propriétés de sécurité ne peuvent pas être exprimés en tant que propriété de trace, mais peuvent l'être en tant que propriété d'équivalence. L'anonymat, la non-tracabilité ou le secret fort sont des exemples classique de propriété d'équivalence. Typiquement, deux protocoles P et Q sont équivalent si les actions d'un adversaire (intrus) ne lui permettent pas de distinguer P de Q. Dans la littérature, plusieurs notions d'équivalence ont été étudiés, par exemple l'équivalence de trace ou l'équivalence observationnelle. Néanmoins, ces équivalences se relèvent être très difficiles à démontrer , d'où l'importance de développer des outils de vérification automatique efficaces de ces équivalences. Au sein de cette thèse, nous avons dans un premier temps travaillé sur une approche reposant sur des techniques de résolution de contraintes et nous avons créé un nouvel algorithme pour décider l'équivalence de trace entre deux protocoles pouvant contenir des conditionnelles avec branches "else", et pouvant également être non-déterministe. Cet algorithme a été appliqué sur des exemples concrets comme le "Private authentification protocol" ainsi que le "E-passport protocol". Cette thèse propose également des résultats de composition pour l'équivalence de trace. En particulier, nous nous sommes intéressé à la composition parallèle de protocoles partageant certains secrets. Ainsi dans cette thèse, nous avons démontré que, sous certaines conditions, la composition parallèle de protocoles préserve les propriétés d'équivalence. Ce résultat fut appliqué au "E-passport protocol". Enfin, cette thèse présente une extension à l'outil de vérification automatique ProVerif afin de démontrer automatiquement plus de propriétés d'équivalence. Cette extension a été implémenté au sein de ProVerif ce qui a permis de démontrer la propriété d'anonymat pour le "Private authentification protocol" . / Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools. We first worked on an approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol. We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties are preserved under parallel composition and under shared secrets. We applied our result on the e-passport protocol. At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allows us to automatically prove anonymity in the private authentication protocol.

On présente une Logique Probabiliste avec des opérateurs Conditionnels - LPCP, sa syntaxe, sémantique, axiomatisation correcte et fortement complète, comprenant une règle de déduction infinitaire. On prouve que LPCP est décidable, et on l'étend pour qu’il puisse représenter l'évidence, en créant ainsi la première axiomatisation propositionnelle du raisonnement basé sur l'évidence. On codifie les Logiques Probabilistes LPP1Q et LPPQ2 dans l'Assistant de Preuve Coq, et on vérifie formellement leurs propriétés principales: correction, complétude fort et non-compacité. Les deux logiques étendent la Logique Classique avec des opérateurs de probabilité, et présentent une règle de déduction infinitaire. LPPQ1 permet des itérations des opérateurs de probabilité, lorsque LPPQ2 ne le permet pas. On a formellement justifié l'utilisation des solveurs SAT probabilistes pour vérifier les questions liées à la cohérence. On présente LFP, un Cadre Logique avec Prédicats Externes, en introduisant un mécanisme pour bloquer et débloquer types et termes dans LF, en permettant l'utilisation d’oracles externes. On démontre que LFP satisfait tous les principales propriétés et on développe un cadre canonique correspondant, qui permet de prouver l’adéquation. On fournit diverses encodages - le λ-calcul non-typé avec la stratégie de réduction CBV, Programmation-par-Contrats, un langage impératif avec la Logique de Hoare, des Logiques Modales et la Logique Linéaire Non-Commutative, en montrant que en LFP on peut codifier aisément des side-conditions dans l'application des règles de typage et atteindre une séparation entre vérification et computation, en obtenant des preuves plus claires et lisibles. / We introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary inference rule. We prove the obtained formalism decidable, and extend it so as to represent evidence, making it the first propositional axiomatisation of reasoning about evidence. We encode Probability Logics LPP1Q and LPP2Q in the Proof Assistant Coq and formally verify their key properties - soundness, strong completeness, and non-compactness. Both logics extend Classical Logic with modal-like probability operators, and both feature an infinitary inference rule. LPP1Q allows iterations of probability operators, while LPP2Q does not. In this way, we have formally justified the use of Probabilistic SAT-solvers for the checking of consistency-related questions. We present LFP - a Logical Framework with External Predicates, by introducing a mechanism for locking and unlocking types and terms into LF, allowing the use of external oracles. We prove that LFP satisfies all the main meta-theoretic properties and develop a corresponding canonical framework, allowing for easy proofs of adequacy. We provide a number of encodings - the simple untyped λ-calculus with a Call-by-Value reduction strategy, the Design-by-Contract paradigm, a small imperative language with Hoare Logic, Modal Logics in Hilbert and Natural Deduction style, and Non-Commutative Linear Logic (encoded for the first time in an LF-like framework), illustrating that in LFP we can encode side-conditions on the application of rules elegantly, and achieve a separation between verification and computation, resulting in cleaner and more readable proofs.

La vérification de programmes avec des calculs sur les nombres à virgule flottante est une étape très importante dans le développement de logiciels critiques. Les calculs sur les nombres flottants sont généralement imprécis, et peuvent dans certains cas diverger par rapport au résultat attendu sur les nombres réels. L’objectif de cette thèse est de concevoir un solveur de contraintes sur les nombres à virgule flottante dédié à la vérification de programmes. Nous présentons dans ce manuscrit une nouvelle méthode de résolution de contraintes sur les flottants. Cette méthode se base principalement sur la sur-approximation des contraintes sur les flottants par des contraintes sur les réels. Cette sur-approximation doit être conservative des solutions sur les flottants. Les contraintes obtenues sont ensuite résolues par un solveur de contraintes sur les réels. Nous avons proposé un algorithme de filtrage des domaines sur les flottants basé sur le concept de la sur-approximation qui utilise des techniques de programmation linéaire. Nous avons aussi proposé une méthode de recherche de solutions basée sur des heuristiques. Cette méthode offre aussi la possibilité de comparer le comportement des programmes par rapport à une spécification sur les réels. Ces méthodes ont été implémentées et expérimentées sur un ensemble de programmes avec du calcul sur les nombres flottants. / The verification of programs with floating-point numbers computation is an important issue in the development of critical software systems. Computations over floating-point numbers are not accurate, and the results may be very different from the expected results over real numbers. The aim of this thesis is to design a constraint solver over floating-point numbers for program verification purposes. We introduce a new method for solving constraints over floating-point numbers. This method is based on an over-approximation of floating-point constraints using constraints over real numbers. This overapproximation is safe, that’s to say it doesn’t loose any solution over the floats. The generated constraints are then solved with a constraint solver over real numbers. We propose a new filtering algorithm using linear programming techniques, which takes advantage of these over-approximations of floating-point constraints. We introduce also new search methods and heuristics to find floating-point solutions of these constraints. Using our implementation, we show on a set of counter-examples the difference of the execution of programs over the floats with the specification over real numbers.

Les centrales solaires thermiques de grande dimension basse et moyenne température (80-120°C) peuvent fournir une chaleur renouvelable et compétitive aux réseaux de chaleurs et aux industries. Ces installations, intensives en capital et avec des faibles coûts de fonctionnement, ont un retour sur investissement sur le long terme. Le suivi de performance et la détection et le diagnostic de défauts automatisés sont donc des axes essentiels permettant de garantir des performances optimales sur toute la durée de vie de l’installation.Cette thèse a pour but l’analyse des défauts les plus importants, dans un but de détection et de diagnostic. Dans un premier temps, une étude exhaustive des défauts pouvant affecter les installations solaires thermiques a été réalisée. Cette étude a permis d’identifier les défauts les plus fréquents et les plus graves, autrement appelés défauts critiques. Parmi ces défauts, six ont été sélectionnés pour être étudiés plus en détails.Afin d’analyser le comportement du système lorsqu’il est soumis aux différents défauts étudiés, un modèle numérique a été mis en place. En particulier, un nouveau modèle de capteur solaire thermique plan a été développé, les modèles existants ne détaillant pas suffisamment certaines caractéristiques physiques nécessaires à la reproduction des défauts. Une validation expérimentale de ce modèle en fonctionnement normal et défaillant a montré qu’il permet une modélisation simple des défauts et que son comportement est réaliste.Une méthodologie pour analyser de façon numérique l’impact des défauts sur le comportement du système est ensuite proposée. Un ensemble de grandeurs permettant de caractériser ce comportement sont notamment définies. Cette méthodologie est ensuite appliquée, d’abord à l’échelle du composant directement impacté par le défaut, puis à l’échelle du système complet. Les résultats permettent d’identifier les défauts détectables ainsi que ceux qui sont identifiables et de proposer un ensemble réduit de grandeurs suffisant pour les détecter et les identifier.Ces travaux offrent une base méthodologique et des premiers résultats qui pourront permettre de développer un algorithme automatisé pour détecter et diagnostiquer les défauts critiques d’une installation solaire thermique de grande dimension. / Large scale solar systems at low and medium temperature (80-120 °C) can provide renewable and competititve energy to district heating and industrial processes. These systems, which are capital-intensive and have low operating costs, present a long-term return on investment. Automated monitoring and fault detection and diagnosis are key elements to guarantee optimal performances during all the lifespan of the plant.This dissertation aims to analyze of the main faults, in a detection and diagnosis purpose. First, an exhaustive study of the dysfunctions that can affect the large scale solar systems enabled to identify the more frequent and serious faults, also called critical faults. Among these critical faults, six were selected for a more detailed study.To analyze the behavior of the system subjected to the studied faults, a numerical model was implemented. A new flat plate thermal solar collector model was particularly developed as existing ones do not detail enough several physical characteristics required for the reproduction of faults. An experimental validation of this model in normal and faulty operation showed that it enables a simple fault modelling and presents a realistic behavior.A methodology to numerically analyze the impact of the faults on the system behavior is then proposed. A set of features enabling the characterizing of this behavior are particularly defined. This approach is applied first at the scale of directly affected component then at system scale. The results enable to identify detectable and isolable faults, but also to propose a reduced set of features sufficient to properly detect and diagnose them.This work presents a methodologic base and first results to develop an automated algorithm for detection and diagnosis of critical faults of a large scale thermal solar system.

En analyse de risques, les arbres d’attaque sont utilisés pour évaluer les menaces sur un système. Les méthodes formelles permettent leur analyse quantitative et leur synthèse, mais les propriétés exprimant la qualité des arbres d’attaque par rapport au système n’ont pas été formalisées. Dans ce document, nous définissons un nouveau cadre formel pour les arbres d’attaque prenant en compte un modèle opérationnel du système, et dotant les arbres d’une sémantique de chemins. Nous définissons les propriétés de correction des raffinements, et étudions leurs complexités. A partir d’une attaque optimale dans un modèle de système quantitatif, nous guidons la conception d’un arbre d’attaque, en indiquant ses feuilles qui contribuent à l’attaque optimale considérée. / In risk analysis, attack trees are used to assess threats to a system. Formal methods allow for their quantitative analysis and synthesis, but the properties expressing the quality of the attack trees with respect to the system have not been formalized. In this document, we define a new formal framework for attack trees that takes an operational model of the system into account, and provides the trees with a path semantics. We define the correctness properties of refinements, and study their computational complexity. Given an optimal attack in a quantitative system model, we guide the design of a attack tree, indicating its leaves that contribute to considered the optimal attack.