Les RCsF sont des réseaux ad hoc, sans fil, large échelle déployés pour mesurer des paramètres de l'environnement et remonter les informations à un ou plusieurs emplacements (nommés puits). Les éléments qui composent le réseau sont de petits équipements électroniques qui ont de faibles capacités en termes de mémoire et de calcul ; et fonctionnent sur batterie. Ces caractéristiques font que les protocoles développés, dans la littérature scientifique de ces dernières années, visent principalement à auto-organiser le réseau et à réduire la consommation d'énergie. Avec l'apparition d'applications critiques pour les réseaux de capteurs sans fil, de nouveau besoins émergent, comme le respect de bornes temporelles et de fiabilité. En effet, les applications critiques sont des applications dont dépendent des vies humaines ou l'environnement, un mauvais fonctionnement peut donc avoir des conséquences catastrophiques. Nous nous intéressons spécifiquement aux applications de détection d'événements et à la remontée d'alarmes (détection de feu de forêt, d'intrusion, etc), ces applications ont des contraintes temporelles strictes. D'une part, dans la littérature, on trouve peu de protocoles qui permettent d'assurer des délais de bout en bout bornés. Parmi les propositions, on trouve des protocoles qui permettent effectivement de respecter des contraintes temporelles mais qui ne prennent pas en compte les spécificités des RCsF (énergie, large échelle, etc). D'autres propositions prennent en compte ces aspects, mais ne permettent pas de garantir des bornes temporelles. D'autre part, les applications critiques nécessitent un niveau de confiance très élevé, dans ce contexte les tests et simulations ne suffisent pas, il faut être capable de fournir des preuves formelles du respect des spécifications. A notre connaissance cet aspect est très peu étudié pour les RcsF. Nos contributions sont donc de deux types : * Nous proposons un protocole de remontée d'alarmes, en temps borné, X-layer (MAC/routage, nommé RTXP) basé sur un système de coordonnées virtuelles originales permettant de discriminer le 2-voisinage. L'exploitation de ces coordonnées permet d'introduire du déterminisme et de construire un gradient visant à contraindre le nombre maximum de sauts depuis toute source vers le puits. Nous proposons par ailleurs un mécanisme d'agrégation temps-réel des alarmes remontées pour lutter contre les tempêtes de détection qui entraînent congestion et collision, et donc limitent la fiabilité du système. * Nous proposons une méthodologie de vérification formelle basée sur les techniques de Model Checking. Cette méthodologie se déroule en trois points, qui visent à modéliser de manière efficace la nature diffusante des réseaux sans fil, vérifier les RCsF en prenant en compte la non-fiabilité du lien radio et permettre le passage à l'échelle de la vérification en mixant Network Calculus et Model Checking. Nous appliquons ensuite cette méthodologie pour vérifier RTXP.

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.

Le développement de circuits électroniques et de systèmes logiciels critiques pour le ferroviaire ou l’avionique, par exemple, demande à être systématiquement associé à un processus de vérification formelle permettant de garantir l’exhaustivité des tests. L’approche formelle la plus répandue dans l’industrie est le Model Checking. Le succès de son adoption provient de deux caractéristiques : (i) son aspect automatique, (ii) sa capacité à produire un témoin (un scénario rejouable) lorsqu’un comportement indésirable est détecté, ce qui fournit une grande aide aux concepteurs pour corriger le problème. Néanmoins, la complexité grandissante des systèmes à vérifier est un réel défi pour le passage à l’échelle des techniques existantes. Pour y remédier, différents algorithmes de model checking (e.g., parcours symbolique des états du système, interpolation), diverses méthodes complémentaires (e.g., abstraction,génération automatique d’invariants), et de multiples procédures de décision(e.g., diagramme de décision, solveur SMT) sont envisageables.Dans cette thèse, nous nous intéressons plus particulièrement à l’induction temporelle.Il s’agit d’un algorithme de model checking très utilisé dans l’industrie pour vérifier les systèmes critiques. C’est également l’algorithme principal de l’outil développé au sein de l’entreprise Safe River, entreprise dans laquelle cette thèse a été effectuée. Plus précisément, l’induction temporelle combine deux techniques :(i) BMC (Bounded Model Checking), une méthode très efficace pour la détection debugs dans un système (ii) k-induction, une méthode ajoutant un critère de terminaison à BMC lorsque le système n’admet pas de bug. Ces deux techniques génèrent des formules logiques propositionnelles pour lesquelles il faut en déterminer la satisfaisabilité.Pour se faire, nous utilisons un solveur SAT, c’est-à-dire une procédure de décision qui détermine si une telle formule admet une solution.L’originalité des travaux proposés dans cette thèse repose en grande partie sur la volonté de renforcer la collaboration entre le solveur SAT et le model checker.Nos efforts visent à accroître l’interconnexion de ces deux modules en exploitant la structure haut niveau du problème. Nous avons alors défini des méthodes profitant de la structure symétrique des formules. Cette structure apparaît lors du dépliage successif de la relation de transition, et nous permet de dupliquer les clauses ou encore de déplier les transitions dans différentes directions (i.e., avant ou arrière). Nous avons aussi pu instaurer une communication entre le solveur SAT et le model checker permettant de : (i) simplifier la représentation au niveau du model checker grâce à des informations déduites par le solveur, et (ii) aider le solveur lors de la résolution grâce aux simplifications effectuées sur la représentation haut niveau. Une autre contribution importante de cette thèse est l’expérimentation des algorithmes proposées. Cela se concrétise par l’implémentation d’un model checker prenant en entrée des modèles AIG (And-Inverter Graph) dans lequel nous avons pu évaluer l’efficacité de nos différentes méthodes. / The design of electronic circuits and safety-critical software systems in railway or avionic domains for instance, is usually associated with a formal verification process. More precisely, test methods for which it is hard to show completeness are combined with approaches that are complete by definition. Model Checking is one of those approaches and is probably the most prevalent in industry. Reasons of its success are mainly due to two characteristics, namely: (i) its fully automatic aspect, and (ii) its ability to produce a short execution trace of undesired behaviors, which is very helpful for designers to fix the issues. However, the increasing complexity of systems to be verified is a real challenge for the scalability of existing techniques. To tackle this challenge, different model checking algorithms (e.g., symbolic model checking, interpolation), various complementary methods (e.g., abstraction, automatic generation of invariants) and multiple decision procedures (e.g., decision diagram, SMT solver) can be considered. In this thesis, we particularly focus on temporal induction. It is a model checking algorithm widely used in the industry to check safety-critical systems. This is also the core algorithm of the tool developed within SafeRiver, company in which this thesis was carried out. More precisely, temporal induction consists of a combination of BMC (Bounded Model Checking) and k-induction. BMC is a very efficient bugfinding method. While k-induction adds a termination criterion to BMC when the system does not admit bugs. These two techniques generate formulas for which it is necessary to determine their satisfiability. To this end, we use a SAT solver as a decision procedure to determine whether a propositional formula has a solution. The main contribution of this thesis aims to strengthen the collaboration between the SAT solver and the model checker. The improvements proposed mainly focus on increasing the interconnections of these two modules by exploiting the high-level structure of the problem.We have therefore defined several methods taking advantage of the symmetrical structure of the formulas. This structure emerges during the successive unfolding of the transition relation, and allows us to duplicate clauses or even unroll the transitions in different directions (i.e., forward or backward). We also established a communication between the solver and the model checker, which has for purpose to: (i) simplify the model checker representation using the information inferred by the solver, and (ii) assist the solver during resolution with simplifications performed on the high-level representation. Another important contribution of this thesis is the empirical evaluation of the proposed algorithms on well-established benchmarks. This is achieved concretely via the implementation of a model checker taking AIG (And-Inverter Graph) as input, from which we were able to evaluate the effectiveness of our algorithms.

Vérifier formellement des programmes concurrents est une tâche difficile. S’il existe différentes techniques pour la réaliser, très peu sont effectivement mises en oeuvre pour des programmes écrits dans des langages de programmation réalistes. En revanche, les techniques de vérification formelles de programmes séquentiels sont utilisées avec succès depuis plusieurs années déjà, et permettent d’atteindre de hauts degrés de confiance dans nos systèmes. Cette thèse propose une alternative aux méthodes d’analyses dédiées à la vérification de programmes concurrents consistant à transformer le programme concurrent en un programme séquentiel pour le rendre analysable par des outils dédiés aux programmes séquentiels. Nous nous plaçons dans le contexte de FRAMA-C, une plate-forme d’analyse de code C spécifié avec le langage ACSL. Les différentes analyses de FRAMA-C sont des greffons à la plate-forme, ceux-ci sont à ce jour majoritairement dédiés aux programmes séquentiels. La méthode de vérification que nous proposons est appliquée manuellement à la vérification d’un code concurrent issu d’un hyperviseur. Nous automatisons la méthode à travers un nouveau greffon à FRAMA-C qui permet de produire automatiquement, depuis un programme concurrent spécifié, un programme séquentiel spécifié équivalent. Nous présentons les bases de sa formalisation, ayant pour but d’en prouver la validité. Cette validité n’est valable que pour la classe des programmes séquentiellement consistant. Nous proposons donc finalement un prototype de solveur de contraintes pour les modèles mémoire faibles, capable de déterminer si un programme appartient bien à cette classe en fonction du modèle mémoire cible. / Formal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware.

Les logiciels embarqués critiques de contrôle-commande sont soumis à des contraintes fortes englobant le déterminisme, la correction logique et la correction temporelle. Nous supposons que les spécifications sont exprimées à l'aide du langage formel de description d'architectures logicielles temps réel multipériodiques Prelude. L'objectif de cette thèse est, à partir d'un programme Prelude ou d'un ensemble de tâches temps réel dépendantes, de générer un code multithreadé exécutable sur une architecture multicœur tout en respectant la sémantique initiale. Pour cela, nous avons développé une boîte à outil, SchedMCore,permettant : - d'une part, la vérification formelle de l'ordonnançabilité. La vérification proposée est basée sur le parcours exhaustif du comportement avec pas de temps discret. Il est alors possible d'analyser des politiques en-ligne (FP, gEDF, gLLF et LLREF) mais également de calculer une affectation de priorité fixe valide et une séquence valide hors-ligne.- d'autre part, l'exécution multithreadée sur une cible multicœur. L'exécutif encode les politiques proposées étudiées dans la partie d'analyse d'ordonnançabilité, à savoir les quatre politiques en-ligne ainsi que les séquences valides générées. L'exécutif permet 3 modes d'utilisation, allant de la simulation temporelle à l'exécution temps précis des comportements des tâches. Il est compatible Posix et facilement portable sur divers OS. / A real-time control-command embedded system is subject to strong constraints such as determinism, logical and temporal correctness. We assume that the specifications are expressed using the formal software architecture description language Prelude, dedicated to real-time multiperiodic applications. The goal of this thesis is, given a Prelude program or dependent real-time taskset, to generate amultithreaded executable code over a multicore architecture while respecting the original semantic. To do so we have developed a toolbox, SchedMcore, that allows: - the formal verification of schedulability. The verification is based on the exhaustive exploration of the behaviour with a discret time frame. It is possible to analyse on-line policies (FP, gEDF, gLLF et LLREF), as well as to compute a fixed valid priority assignment and a valid off-line sequence.- the multithreaded execution over a multicore target. The framework encodes the same policies as those studied in the first part (the four on-line policies and the generated sequences). The framework provides three usage modes, from temporal simulation to time accurate execution. The executive is compatible with Posix and easily portable on several OS.

L'étude des grands modèles de réseaux biologiques par l'utilisation d'outils d'analyse et de simulation conduit à un grand nombre de prédictions. Cela soulève la question de savoir comment identifier les prédictions intéressantes de nouveaux phénomènes, qui peuvent être confrontés à des données expérimentales. Les techniques de vérification formelle basées sur le model checking constituent une technologie puissante pour faire face à cette augmentation d'échelle et de complexité pour l'analyse de ces réseaux. L'application de ces techniques est par contre difficile, pour plusieurs raisons. Premièrement, le domaine de la biologie des systèmes a mis en évidence quelques propriétés dynamiques du réseau, comme la multi-stabilité et les oscillations, qui ne sont pas facilement exprimables avec les logiques temporelles classiques. Deuxièmement, la difficulté de poser des questions pertinentes et intéressantes en logique temporelle est difficile pour les utilisateurs non-experts. Enfin, la plupart des modèles existants et des outils de simulation ne sont pas capables d'appliquer des techniques de model checking d'une manière transparente. La mise en œuvre des approches développées dans ce travail contribue à enlever des obstacles pour l'utilisation de la technologie de vérification formelle en biologie. Leur application a été validée sur l'analyse et la simulation de deux modèles biologiques complexes. / The study of large models of biological networks by means of analysis and simulation tools leads to large amounts of predictions. This raises the question of how to identify interesting predictions of novel phenomena that can be confronted with experimental data. Formal verification techniques based on model-checking have recently been used to the analysis of these networks, providing a powerful technology to keep up with this increase in scale and complexity. The application of these techniques is hampered, however, by several key issues. First, the systems biology domain brought to the fore a few properties of the network dynamics like multistability and oscillations, that are not easily expressed using classical temporal logics. Second, the problem of posing relevant and interesting questions in temporal logic, is difficult for non-expert users. Finally, most of the existing modeling and simulation tools are not capable of applying model-checking techniques in a transparent way. The approaches developed in this work lower the obstacles to the use of formal verification in systems biology. They have been validated on the analysis and simulation of two real and complex biological models. / O estudo de redes biológicas tem originado o desenvolvimento de modelos cada vez mais complexos e detalhados. O estudo de redes biológicas complexas utilizando ferramentas de análise e simulação origina grandes quantidades de previsões. Isto levanta a questão de como identificar previsões interessantes de novos fenómenos que possam ser comparados com dados experimentais. As técnicas de verificação formal baseadas em model-checking têm sido usadas na análise destas redes, fornecendo uma tecnologia poderosa para acompanhar o aumento de escala e complexidade do problema. A aplicação destas técnicas tem sido dificultada por um conjunto importante de factores. Em primeiro lugar, em biologia de sistemas têm sido tratadas diversas questões acerca da dinâmica da rede, como a multi-estabilidade e oscilações, que não são facilmente expressas usando lógicas temporais clássicas. Em segundo lugar, o problema de como elaborar perguntas relevantes em lógica temporal, é difícil para o utilizador comum. Por último, a maioria das ferramentas de modelação e simulação não estão preparadas para a aplicação de técnicas de model-checking de forma transparente. Os métodos desenvolvidos nesta tese aliviam os obstáculos no uso da verificação formal em biologia de sistemas. Estes métodos foram validados através da análise e simulação de dois modelos biológicos complexos.

Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en agents qui interagissent et qui existent au sein d'un environnement. Ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominantes dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. Non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Nous introduisons une architecture formelle d'agent basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisées d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables. Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator).Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche. / Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely reflexive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as a MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., "every time the agent does X, it will do Y later"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS's and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose w.r.t. the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again.In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into a MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach.

L'objectif principal de cette thèse est de proposer une approche efficace de modélisation et de résolution pour le problème d’ordonnancement, en mettant l’accent sur le partage multi-ressources et sur l’incertitude potentielle d’occurrence de certains événements. L'ordonnancement a pour objectif de réaliser un ensemble de tâches à la fois en respectant des contraintes prédéfinies et en optimisant le temps. Ce travail s’intéresse en particulier à la minimisation du temps total d’exécution. La plupart des approches existantes préconisent une modélisation mathématique exprimant des équations et des contraintes pour décrire et résoudre des problèmes d’ordonnancement. De telles démarches ont une complexité inhérente. Cependant dans l’industrie, la tâche de planification est récurrente et peut requérir des changements fréquents des contraintes. Outre cela, la prise en compte d’événements incertains est peu supportée par les approches existantes; cela peut toutefois augmenter la robustesse d’un ordonnancement. Pour répondre à ces problématiques, après une introduction, le chapitre 2 aborde le problème de l’ordonnancement à travers une démarche de modélisation visuelle, expressive et formelle, s’appuyant sur les automates pondérés et sur la théorie des automates temporisés. L’originalité des modèles proposés réside aussi dans leur capacité de décrire le partage de ressources multiples et proposer une approche de résolution efficace. Ces modèles ont l’avantage d’être directement exploitables par des outils de vérification formelle, à travers une démarche de preuve par contradiction vis-à-vis de l’existence d’une solution. Les résultats effectifs sont obtenus grâce à l’outil UPPAAL. La complexité inhérente à la production d’une solution optimale est abordée à travers un algorithme de recherche et d’amélioration itérative de solutions, offrant une complexité très prometteuse sur la classe de problèmes étudiés. Dans le chapitre 3, une composition synchrone est d’automates pondérés est proposée dans le but de résoudre le problème d’ordonnancement en effectuant une analyse d’atteignabilité optimale directement sur les modèles automates pondérés. Dans le quatrième chapitre, divers comportements incontrôlables tels que le temps de début, la durée de la tâche et l'occurrence d’échec dans un problème d‘ordonnancement sont modélisés par des automates de jeu temporisés. Ensuite, le problème est résolu en effectuant une synthèse de stratégie optimale dans le temps dans l'outil de synthèse TIGA. / The objective of scheduling problems is to find the optimal performing sequence for a set of tasks by respecting predefined constraints and optimizing a cost: time, energy, etc. Despite classical approaches, automata models are expressive and also robust against changes in the parameter setting and against changes in the problem specification. Besides, few studies have used formal verification approaches for addressing scheduling problems; yet none of them considered challenging and practical issues such as multi-resource sharing aspect, uncontrollable environment and reaching the optimal schedule in a reasonable time for industrializing the model. The main objective of this thesis is to propose an efficient modeling and solving approach for the scheduling problem, considering multi-resource sharing and potential uncertainty in occurrence of certain events. For this purpose, after an introduction in Chapter 1, Chapter 2 addresses the problem of scheduling through a visual, expressive and formal modeling approach, based on weighted automata and the theory of timed automata. The originality of the proposed approach lies in ability of handling the sharing of multiple resources and proposing an efficient solving approach. The proposed models have the advantage of being directly exploitable by means of formal verification tools. The results are obtained using the UPPAAL tool. To solve the problem, an algorithm is developed based on iterating reachability analysis to obtain sub-optimal makespan. Results show the proposed model and solving approach provides a very promising complexity on the class of studied problems and can be applied to industrial cases. In Chapter 3, a synchronous composition of weighted automata is proposed to solve the scheduling problem by performing an optimal reachability analysis directly on the weighted automata models. In the fourth chapter, various uncontrollable behaviors such as the start time, the duration of the task and the failure occurrence in a scheduling problem are modeled by timed game automata. Then, the problem is solved by performing an optimal strategy synthesis over time in TIGA as a synthesis tool.

Le véhicule autonome est un véhicule qui se conduira, à terme, sans aucune intervention du conducteur, quelle que soit la situation de conduite. Ce véhicule comprend une nouvelle fonction, nommée fonction AD, pour Autonomous Driving, en charge de la conduite autonome. Cette fonction peut se trouver dans des états différents (Active, Disponible par exemple) selon l'évolution des conditions environnementales. Le changement de ses états est géré par une fonction de Supervision, nommée Supervision AD. Le principal objet de ces travaux consiste à garantir que la fonction AD se trouve constamment dans un état sûr. Ceci revient à s'assurer que la Supervision AD respecte l'ensemble des exigences fonctionnelles et de sûreté qui spécifient son comportement. Ces deux types d'exigences sont émis par deux métiers distincts : l'Architecte Métier Système (AMS) et le pilote Sûreté de Fonctionnement (SdF). Ces deux disciplines d'ingénierie, bien qu'elles contribuent à la conception d'une même fonction, se distinguent en de nombreux points : objectifs, contraintes, planning, outils... Dans notre cas d'étude, ces différences s'illustrent par les exigences considérées : les exigences fonctionnelles sont allouées à la fonction AD globale, tandis que les exigences de sûreté spécifient le comportement de sous-fonctions locales redondantes assurant une continuité de service en cas de défaillance. La mise en cohérence de ces deux perspectives métier au plus tôt dans le cycle de conception et dans un contexte industriel, est la problématique centrale traitée. Les enjeux de SdF soulevés par le véhicule autonome rendent ce problème primordial pour les constructeurs automobiles. Afin de répondre à ces préoccupations, nous avons proposé une démarche outillée et collaborative de conception sûre de la Supervision AD. Cette démarche est intégrée dans les processus normatifs en vigueur (normes ISO 15288 et ISO 26262) ainsi que dans les processus de conception internes chez Renault. Elle est fondée sur la vérification formelle par model checking, la composition parallèle d'automates finis et l'expertise métier. Cette démarche prône l'utilisation d'un même formalisme (l'automate à états finis) par les deux métiers pour mener à bien des activités partageant un objectif de modélisation commun : la vérification d'exigences de comportement en phase amont de conception. Une méthode pour traduire les exigences en propriétés formelles et construire les modèles d'état a été déployée. Il en résulte une consolidation progressive des exigences traitées, initialement rédigées en langage naturel. Les potentielles ambigüités, incohérences et incomplétudes sont exhibées et traitées. / The Autonomous Vehicle is meant to drive itself, without any driver intervention, whatever the driving situation. This vehicle includes a new function, called AD, for Autonomous Driving, function. This function can be in different states (Available, Active for example) according to environmental conditions evolution. This states change is managed by a supervision function, named AD Supervision. The main goal of my works consists in guaranteeing that AD function remains always in a safe state. In other words, the AD Supervision must always respect all the functional and safety requirements that specify its behavior. These two requirements types are produced by two different professions: the System Architect (SA) and the Safety Engineer (SE). These two fields contribute to the design of the same function but distinguish at several aspects: objectives, constraints, planning, tools… In our case study, these differences are illustrated by considered requirements: the functional requirements are allocated to global AD function, while the safety requirements specify the behavior of local redundant sub-functions ensuring a continuous service in case of failure. The consistency of the two perspectives as early as possible in the design phase and in an industrial context, is the central problematic addressed. The safety issues due to Autonomous Vehicle make this topic essential for the automotive manufacturers. To meet these concerns, we proposed a tooled and collaborative approach for safe design of AD Supervision. This approach is integrated in the normative processes (standards ISO 26262 and ISO 15288) as well as in the internal design processes at Renault. It is based on formal verification by model checking, parallel composition of finite sate automata and technical expertise. This approach advocates the utilization of a same formalism (state automata) by the two professions to perform activities sharing a common goal: behavior requirements verification in preliminary design phase. A method to translate requirements into formal properties and to build state models has been deployed. The result is a progressive consolidation of treated requirements, initially expressed in free natural language. The potential ambiguities, inconsistencies and incompleteness are exhibited and treated. Two main contributions are in this way illustrated: highlighting of several formal credible (i.e. validated by expertise) specifications from informal requirements; and precise definition of technical expertise role (milestones, planning). However, this reinforcement – in silos – of the two profession viewpoints does not guarantee that they are mutually consistent. Thus, we proposed a convergence method, relying on expertise and on parallel composition of state automata, for the comparison of local and global views.

Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Ces méthodes sont indispensables pour assurer les plus hauts niveaux de sûreté. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficultés d'ordre pratique et théorique. Les principales difficultés concernent la prise en compte des aspects bas niveau, comme les pointeurs et les interactions avec le matériel spécifique. De plus, le fait que ces systèmes soient concurrents conduit à une augmentation exponentielle du nombre de comportements possibles, ce qui rend plus difficile leur vérification. Dans cette thèse, nous proposons une méthodologie pour la spécification et la vérification par model-checking de ce type de systèmes, en particulier, ceux implémentés en C. Cette méthodologie est basée sur la traduction de la sémantique de C en TLA+, un langage de spécification formel adapté à la modélisation de systèmes concurrents. Nous avons proposé un modèle de mémoire et d'exécution d'un programme C séquentiel en TLA+. En se basant sur ce modèle, nous avons proposé un ensemble de règles de traduction d'un code C en TLA+ que nous avons implémenté dans un outil, appelé C2TLA+. Nous avons montré comment ce modèle peut s'étendre pour modéliser les programmes C concurrents et gérer la synchronisation entre plusieurs processus ainsi que leur ordonnancement. Pour réduire la complexité du model-checking, nous avons proposé une technique permettant de réduire significativement la complexité de la vérification. Cette réduction consiste pour un code C à agglomérer une suite d'instructions lors de la génération du code TLA+, sous réserve d'un ensemble de conditions.Nous avons appliqué la méthodologie proposée dans cette thèse sur un cas d'étude réel issu de l'implémentation d'un micronoyau industriel,sur lequel nous avons vérifié un ensemble de propriétés fonctionnelles. L'application de la réduction a permis de réduire considérablement le temps de la vérification, ce qui la rend utilisable en pratique.Les résultats ont permis d'étudier le comportement du système, de vérifier certaines propriétés et de trouver des bugs indétectables par des simples tests. / Software systems are critical and complex. In order to guarantee their correctness, the use of formal methodsis important. These methods can be defined as mathematically based techniques, languages and tools for specifying and reasoning about systems. But, the application of formal methods to software systems, implemented in C, is challenging due to the presence of pointers, pointer arithmetic andinteraction with hardware. Moreover, software systems are often concurrent, making the verification process infeasible. This work provides a methodology to specify and verify C software systems usingmodel-checking technique. The proposed methodology is based on translating the semantics of Cinto TLA+, a formal specification language for reasoning about concurrent and reactive systems. We define a memory and execution model for a sequential program and a set of translation rules from C to TLA+ that we developed in a tool called C2TLA+. Based on this model, we show that it can be extended to support concurrency, synchronization primitives and process scheduling. Although model-checking is an efficient and automatic technique, it faces the state explosion problem when the system becomes large. To overcome this problem, we propose a state-space reduction technique. The latter is based on agglomerating a set of C instructions during the generation phase of the TLA+ specification. This methodology has been applied to a concrete case study, a microkernel of an industrial real-time operating system, on which a set of functional properties has been verified. The application of the agglomeration technique to the case study shows the usefulness of the proposed technique in reducing the complexity of verification. The obtained results allow us to study the behavior of the system and to find errors undetectable using traditional testing techniques.