As embedded software and platforms become more complicated, many safety properties are left to simulation and testing. MRICDF is a formal polychronous language used to guarantee certain safety properties and alleviate the burden of software development and testing. We propose real-time extensions to MRICDF so that temporal properties of embedded systems can also be proven. We adapt the extended precedence encoding technique of Prelude and expand upon current schedulability analysis techniques for multi-periodic real-time systems. / Master of Science

Embedded controllers coordinate the behaviours of specialised hardware components to satisfy broader application requirements. They are difficult to model and to program. One of the greatest challenges is to express intricate timing behaviours???which arise from the physical characteristics of components???while not precluding efficient implementations on resource-constrained platforms. Aspects of this challenge are addressed by this thesis through four distinct applications of timed automata and the synchronous languages Argos and Esterel. A novel framework for simulating controllers written in an imperative synchronous language is described. It includes a transformation of synchronous models into timed automata that accounts for timing properties which are important in constrained implementations but ignored by the usual assumption of synchrony. The transformation provides an interface between the discrete time of synchronous programs and a continuous model of time. This interface is extended to provide a way for simulating Argos programs within the widely-used Simulink software. Timed automata are well-suited for semantic descriptions, like the aforementioned transformation, and for modelling abstract algorithms and protocols. This thesis also includes a different type of case study. The timing diagram of a small-scale embedded component is modelled in more detail than usual with the aim of studying timing properties in this type of system. Multiple models are constructed, including one of an assembly language controller. Their interrelations are verified in Uppaal using a construction for timed trace inclusion testing. Existing constructions for testing timed trace inclusion do not directly address recent features of the Uppaal modelling language. Novel solutions for the problems presented by selection bindings, quantifiers, and channel arrays in Uppaal are presented in this thesis. The first known implementation of a tool for automatically generating a timed trace inclusion construction is described. The timed automata case study demonstrates one way of implementing application timing behaviours while respecting implementation constraints. A more challenging, but less detailed, example is proposed to evaluate the adequacy of Esterel for such tasks. Since none of the standard techniques are completely adequate, a novel alternative for expressing delays in physical time is proposed. Programs in standard Esterel are recovered through syntactic transformations that account for platform constraints.

Les langages synchrones ont été fondés pour modéliser et implémenter les systèmes réactifs temps-réels critiques. Avec la complexité toujours croissante des systèmes contrôlés, la vitesse d'exécution devient un critère important. Nous sommes donc à la recherche d'une exécution parallèle, combinant efficacité et sûreté.Les langages synchrones ont toujours intégré la notion de parallélisme, mais ce, pour l'expressivité de la modélisation. Leurs compilations visent principalement les circuits ou la génération de code séquentiel. Tous ont une sémantique formelle, qui rend possible la distribution correcte du code. Mais la préservation de cette sémantique peut être un obstacle à l'efficacité du code généré, particulièrement s'il est nécessaire de préserver une notion d'instant global au système.Le modèle sémantique qui nous intéresse est celui des réseaux de Kahn. Ces réseaux modélisent des calculateurs distribués, communiquant au travers de files de taille non bornée. Dans ce cadre, la distribution ne demande aucune communication ni synchronisation supplémentaire. En considérant l'histoire des files de communication, la sémantique de Kahn permet de s'abstraire de l'exécution effective, tout en garantissant le déterminisme du calcul. Pour cela, chaque nœud du réseau doit avoir une sémantique fonctionnelle continue.Le langage que nous développons est Heptagon, un langage synchrone fonctionnel du premier ordre, déscendant de Lustre. Son compilateur est un prototype universitaire, apparenté à l'outil industriel Scade. Grâce à sa sémantique de Kahn, la distribution d'un programme Heptagon ne pose pas de question, son efficacité beaucoup plus.L'efficacité requiert de minimiser les synchronisations. Cela revêt deux aspects non indépendants. Avoir un découplage suffisant des calculs : il y a des délais dans les dépendances entre calculs. Avoir une granularité importante des calculs : un fort ratio temps de calcul sur fréquence de communication. Or la sémantique synchrone et les horloges d'un programme Heptagon reflètent exactement l'inverse. Elles permettent au programmeur de se contenter d'un découplage d'un instant et à chaque instant, au maximum une valeur est calculée. De plus, les instants sont typiquement courts, pour assurer que le système réagit rapidement.Des précédents travaux sur le sujet, nous tirons deux constats.Le premier est que nous souhaitons le contrôle du parallélisme par le programmeur, directement dans le code source. Il doit pouvoir maîtriser à quels instants il y a communication ou synchronisation. La solution que nous proposons dans ce manuscrit est l'utilisation des futures dans Heptagon. Ils fournissent ce pouvoir au programmeur, tout en restant des annotations qui peuvent être supprimées sans changer la sémantique dénotationnelle du programme.Le deuxième constat est que la question de la granularité des calculs est une question profonde, touchant en particulier aux questions de dépendance de données, de choix des horloges et de compilation modulaire. Heptagon, comme ses parents, restreint les réseaux de Kahn qui peuvent être écrits, de telle sorte que ces trois questions se traitent séparément. Pour mieux comprendre le lien entre ces éléments, nous revenons aux réseaux de Kahn. Notre principal résultat est la définition de la sous-classe des réseaux ordonnés réactifs. Ceux-ci sont les seuls pour lesquels nous pouvons décrire modulairement le comportement avec des horloges, sans restreindre les contextes d'appels. Ces réseaux ont une signature d'horloge en forme normale, qui maximise la granularité. Pour l'exprimer, nous introduisons les horloges entières, décrivant la communication de plusieurs valeurs en un seul instant. Nous appliquons ensuite nos résultats pour voir sous un nouveau jour Heptagon, Signal, les politiques des objets de Lucid Synchrone, mais aussi proposer une analyse pleinement modulaire de Lucy-n langage synchrone le plus fidèle aux réseaux de Kahn. / Synchronous languages are used to program critical reactive systems. Today, systems require to find a way to execute them safely and in parallel. Parallelism has always been part of synchronous langages, but for modeling purpose. Their formal semantics allow to distribute them, but preserving the semantics may be ressource costly and prevent good parallel execution.The Kahn networks model is of great interest. It models distributed computers, communicating through unbounded FIFOs, ensuring that the computed values are deterministic, without any need of added synchronization.We develop the langage Heptagon, a first order functional synchronous son of Lustre.The compiler is an academic prototype of the industrial tool Scade. Thanks to its Kahn semantics, it can be distributed. In order to be efficient, one need to maximize the decoupling of computations and maximize the computation granularity. However, synchronous langages allow for very tight computation coupling and usually require thin computation granularity to ensure reactivity of the system.We opt for two research directions. The first one is to give the control of the execution parallelism to the programer. To this mean, we add futures to the source langage Heptagon. They provide control over starting and end of parallel computations, while preserving the functional semantics. Moreover, we provide a compilation for embedded systems, using statically allocated memory. The second one is to study Kahn synchronous semantics to understand data dependencies and maximize granularity of the computations. This touches deeply to the synchronous languages, mixing the usually separated questions of causality and clock calculus. We define the class of reactive ordered Kahn networks. They are the one which may be modularly compiled and whose behavior may be expressed with a clock signature. Moreover, we show that their is a normal form for this signature, maximizing the granularity of the network. To express it, we extend clocks to integer clocks. Then we come back to the synchronous languages we know to understand how to use it. The result is fully used and explained on Lucy-n, the synchronous language closest to Kahn networks.

Since the mid-1990s, formal verification has become increasingly important because it can provide guarantees that a software system is free of bugs and working correctly based on a provided model. Verification of biological and medical systems is a promising application of formal verification. Human neural networks have recently been emulated and studied as a biological system. Some recent research has been done on modelling some crucial neuronal circuits and using model checking techniques to verify their temporal properties. In large case studies, model checkers often cannot prove the given property at the desired level of generality. In this thesis, we provide a model using the Coq proof assistant and prove some properties concerning the dynamic behavior of some basic neuronal structures. Understanding the behavior of these modules is crucial because they constitute the elementary building blocks of bigger neuronal circuits. By using a proof assistant, we guarantee that the properties are true in the general case, that is, true for any input values, any length of input, and any amount of time. In this thesis, we define a model of human neural networks. We verify some properties of this model starting with properties of neurons. Neurons are the smallest unit in a human neuronal network. In the next step, we prove properties about functional structures of human neural networks which are called archetypes. Archetypes consist of two or more neurons connected in a suitable way. They are known for displaying some particular classes of behaviours, and their compositions govern several important functions such as walking, breathing, etc. The next step is verifying properties about structures that couple different archetypes to perform more complicated actions. We prove a property about one of these kinds of compositions. With such a model, there is the potential to detect inactive regions of the human brain and to treat mental disorders. Furthermore, our approach can be generalized to the verification of other kinds of networks, such as regulatory, metabolic, or environmental networks.

La loi de Moore sur semi-conducteurs approche de sa fin. L'evolution de l'architecture de von Neumann à travers les 40 ans d'histoire du microprocesseur a conduit à des circuits d'une insoutenable complexité, à un très faible rendement de calcul par transistor, et une forte consommation énergetique. D'autre-part, le monde du calcul parallèle ne supporte pas la comparaison avec les niveaux de portabilité, d'accessibilité, de productivité et de fiabilité de l'ingénérie du logiciel séquentiel. Ce dangereux fossé se traduit par des défis passionnants pour la recherche en compilation et en langages de programmation pour le calcul à hautes performances, généraliste ou embarqué. Cette thèse motive notre piste pour relever ces défis, introduit nos principales directions de travail, et établit des perspectives de recherche.

Cette thèse étudie la vérification automatique de propriétés de sûreté de systèmes logico-numériques discrets ou hybrides. Ce sont des systèmes ayant des variables booléennes et numériques et des comportements discrets et continus. Notre approche est fondée sur l'analyse statique par interprétation abstraite. Nous adressons les problèmes suivants : les méthodes d'interprétation abstraite numériques exigent l'énumération des états booléens, et par conséquent, ils souffrent du probléme d'explosion d'espace d'états. En outre, il y a une perte de précision due à l'utilisation d'un opérateur d'élargissement afin de garantir la terminaison de l'analyse. Par ailleurs, nous voulons rendre les méthodes d'interprétation abstraite accessibles à des langages de simulation hybrides. Dans cette thèse, nous généralisons d'abord l'accélération abstraite, une méthode qui améliore la précision des invariants numériques inférés. Ensuite, nous montrons comment étendre l'accélération abstraite et l'itération de max-stratégies à des programmes logico-numériques, ce qui aide à améliorer le compromis entre l'efficacité et la précision. En ce qui concerne les systèmes hybrides, nous traduisons le langage de programmation synchrone et hybride Zelus vers les automates hybrides logico-numériques, et nous étendons les méthodes d'analyse logico-numérique aux systèmes hybrides. Enfin, nous avons mis en oeuvre les méthodes proposées dans un outil nommé ReaVer et nous fournissons des résultats expérimentaux. En conclusion, cette thèse propose une approche unifiée à la vérification de systèmes logico-numériques discrets et hybrides fondée sur l'interprétation abstraite qui est capable d'intégrer des méthodes d'interprétation abstraite numériques sophistiquées tout en améliorant le compromis entre l'efficacité et la précision. / This thesis studies the automatic verification of safety properties of logico-numerical discrete and hybrid systems. These systems have Boolean and numerical variables and exhibit discrete and continuous behavior. Our approach is based on static analysis using abstract interpretation. We address the following issues: Numerical abstract interpretation methods require the enumeration of the Boolean states, and hence, they suffer from the state space explosion problem. Moreover, there is a precision loss due to widening operators used to guarantee termination of the analysis. Furthermore, we want to make abstract interpretation-based analysis methods accessible to simulation languages for hybrid systems. In this thesis, we first generalize abstract acceleration, a method that improves the precision of the inferred numerical invariants. Then, we show how to extend abstract acceleration and max-strategy iteration to logico-numerical programs while improving the trade-off between efficiency and precision. Concerning hybrid systems, we translate the Zelus hybrid synchronous programming language to logico-numerical hybrid automata and extend logico-numerical analysis methods to hybrid systems. Finally, we implemented the proposed methods in ReaVer, a REActive System VERification tool, and provide experimental results. Concluding, this thesis proposes a unified approach to the verification of discrete and hybrid logico-numerical systems based on abstract interpretation, which is capable of integrating sophisticated numerical abstract interpretation methods while successfully trading precision for efficiency.

Cette thèse traite de systèmes embarqués contrôlés par un ensemble de processus périodiques non synchronisés. Chaque processus est activé quasi-périodiquement, c'est-à-dire périodiquement avec une gigue bornée. Les délais de communication sont également bornés. De tels systèmes réactifs, appelés 'quasi-périodiques', apparaissent dès que l'on branche ensemble deux processus périodiques. Dans la littérature, ils sont parfois qualifiés de systèmes distribués temps-réels synchrones. Nous nous intéressons aux techniques de conception et d'analyse de ces systèmes qui n'imposent pas de synchronisation globale. Les langages synchrones ont été introduits pour faciliter la conception des systèmes réactifs. Ils offrent un cadre privilégié pour programmer, analyser, et vérifier des systèmes quasi-périodiques. En s'appuyant sur une approche synchrone, les contributions de cette thèse s'organisent selon trois thématiques: vérification,implémentation, et simulation des systèmes quasi périodiques.Vérification: 'L'abstraction quasi-synchrone' est une abstraction discrète proposée par Paul Caspi pour vérifier des propriétés de sûreté des systèmes quasi-périodiques. Nous démontrons que cette abstraction est en général incorrecte et nous donnons des conditions nécessaires et suffisantes sur le graphe de communication et les caractéristiques temps-réel de l'architecture pour assurer sa correction. Ces résultats sont ensuite généralisés aux systèmes multi-périodiques.Implémentation: Les 'LTTAs' sont des protocoles conçus pour assurer l'exécution correcte d'une application sur un système quasi-périodique. Nous proposons d'étudier les LTTA dans un cadre synchrone unifié qui englobe l'application et les contrôleurs introduits par les protocoles. Cette approche nous permet de simplifier les protocoles existants, de proposer des versions optimisées, et de donner de nouvelles preuves de correction. Nous présentons également dans le même cadre un protocole fondé sur une synchronisation d'horloge pour comparer les performances des deux approches.Simulation: Un système quasi-périodique est un exemple de modèle faisant intervenir des caractéristiques temps-réels et des tolérances. Pour ce type de modèle non déterministe, nous proposons une 'simulation symbolique', inspirée des techniques de vérification des automates temporisés. Nous montrons comment compiler un modèle mêlant des composantes temps-réel non déterministes et des contrôleurs discrets en un programme discret qui manipule des ensembles de valeurs. Chaque trace du programme résultant capture un ensemble d'exécutions possibles du programme source. / In this thesis we study embedded controllers implemented as sets of unsynchronized periodic processes. Each process activates quasi-periodically, that is, periodically with bounded jitter, and communicates with bounded transmission delays. Such reactive systems,termed 'quasi-periodic', exist as soon as two periodic processes areconnected together. In the distributed systems literature they arealso known as synchronous real-time models. We focus on techniquesfor the design and analysis of such systems without imposing a globa lclock synchronization. Synchronous languages were introduced as domain specific languages for the design of reactive systems. They offer an ideal framework to program, analyze, and verify quasi-periodic systems. Based on a synchronous approach, this thesis makes contributions to the treatment of quasi-periodic systems along three themes: verification,implementation, and simulation.Verification: The 'quasi-synchronous abstraction' is a discrete abstraction proposed by Paul Caspi for model checking safety properties of quasi-periodic systems. We show that this abstractionis not sound in general and give necessary and sufficient conditionson both the static communication graph of the application and the real-time characteristics of the architecture to recover soundness. We then generalize these results to multirate systems.Implementation: 'Loosely time-triggered architectures' are protocols designed to ensure the correct execution of an application running on a quasi-periodic system. We propose a unified framework that encompasses both the application and the protocol controllers. This framework allows us to simplify existing protocols, propose optimized versions, and give new correctness proofs. We instantiate our framework with a protocol based on clock synchronization to compare the performance of the two approaches.Simulation: Quasi-periodic systems are but one example of timed systems involving real-time characteristics and tolerances. For such nondeterministic models, we propose a 'symbolic simulation' scheme inspired by model checking techniques for timed automata. We show how to compile a model mixing nondeterministic continuous-time and discrete-time dynamics into a discrete program manipulating sets of possible values. Each trace of the resulting program captures a set of possible executions of the source program.