A significant part of the System-on-a-Chip (SoC) design problem is in the correct composition of intellectual property (IP) blocks. Ever increasing clock frequencies make it impossible for signals to reach from one end of the chip to the other end within a clock cycle; this invalidates the so-called synchrony assumption, where the timing of computation and communication are assumed to be negligible, and happen within a clock cycle. Missing the timing deadline causes this violation, and may have ramifications on the overall system reliability. Although latency insensitive protocols (LIPs) have been proposed as a solution to the problem of signal propagation over long interconnects, they have their own limitations. A more generic solution comes in the form of globally asynchronous locally synchronous (GALS) designs. However, composing synchronous IP blocks either over long multicycle delay interconnects or over asynchronous communication links for a GALS design is a challenging task, especially for ensuring the functional correctness of the overall design. In this thesis, we analyze various solutions for solving the synchronization problems related with IP composition. We present alternative LIPs, and provide a validation framework for ensuring their correctness. Our notion of correctness is that of latency equivalence between a latency insensitive design and its synchronous counterpart. We propose a trace-based framework for analyzing synchronous behaviors of different IPs, and provide a correct-by-construction protocol for their transformation to a GALS design. We also present a design framework for facilitating GALS designs. In the framework, Kahn process network specifications are refined into correct-by-construction GALS designs. We present formal definitions for the refinements towards different GALS architectures. For facilitating GALS in distributed embedded software, we analyze certain subclasses of synchronous designs using a Pomset-based semantic model that allows for desynchronization toward GALS. / Ph. D.

The development of high integrity embedded systems remains an arduous and error-prone task, despite the efforts by researchers in inventing tools and techniques for design automation. Much of the problem arises from the fact that the semantics of the modeling languages for the various tools, are often distinct, and the semantics gaps are often filled manually through the engineer's understanding of one model or an abstraction. This provides an opportunity for bugs to creep in, other than standardizing software engineering errors germane to such complex system engineering. Since embedded systems applications such as avionics, automotive, or industrial automation are safety critical, it is very important to invent tools, and methodologies for safe and reliable system design. Much of the tools, and techniques deal with either the design of embedded platforms (hardware, networking, firmware etc), and software stack separately. The problem of the semantic gap between these two, as well as between models of computation used to capture semantics must be solved in order to design safer embedded systems. In this dissertation we propose a methodology for the end-to-end modeling and analysis of safety-critical embedded systems. Our approach consists of formal platform modeling, and analysis; formal application modeling; and 'correct-by-construction' code synthesis with the aim of bridging semantic gaps between the various abstractions and models required for the end-to-end system design. While the platform modeling language AADL has formal semantics, and analysis tools for real-time, and performance verification, the application behavior modeling in AADL is weak and part of an annex. In our work, we create the APECS (AADL and Polychrony based Embedded Computing Synthesis) methodology to allow an embedded system design specification all the way from platform architecture and platform components, the real-time behavior, non-functional properties, as well as the application software modeling. Our main contribution is to integrate a polychronous application software modeling language, and synthesis algorithms in order for synthesis of the embedded software running on the target platform, with the required constraints being met. We believe that a polychronous approach is particularly well suited for a multiprocessor/multi-controller distributed platform where different components often operate at independent rates and concurrently. Further, the use of a formal polychronous language will allow for formal validation of the software prior to code generation. We present a prototype framework that implements this approach, which we refer to as the AADL and Polychrony based Embedded Computing System (APECS). Our prototype utilizes an extended version of Ocarina to provide code generation for the AADL model. Our polychronous modeling language is MRICDF. Our prototype extends Ocarina to support software specification in MRICDF and generate multi-threaded software. Additionally, we implement an automated translation from Simulink to MRICDF, allowing designers to benefit from its formal semantics and exploit engineers' familiarity with Simulink tools, and legacy models. We present case studies utilizing APECS to implement safety critical systems both natively in MRICDF and in Simulink through automated translation. / Ph. D.

L'objectif du travail présenté dans cette thèse est de répondre à un verrou fondamental, qui est «comment programmer d'une manière rigoureuse et efficace des applications embarquées sur des plateformes multi-coeurs?». Cette problématique pose plusieurs défis: 1) le développement d'une approche rigoureuse basée sur les modèles pour pouvoir garantir la correction; 2) le « mariage » entre modèle physique et modèle de calcul, c'est-à-dire, l'intégration du fonctionnel et non-fonctionnel; 3) l'adaptabilité. Pour s'attaquer à ces défis, nous avons développé un flot de conception rigoureux autour du langage BIP. Ce flot de conception permet l'exploration de l'espace de conception, le traitement à diffèrent niveaux d'abstraction à la fois pour la plate-forme et l'application, la génération du code et le déploiement sur des plates-formes multi-cœurs. La méthode utilisée s'appuie sur des transformations source-vers-source des modèles BIP. Ces transformations sont correctes-par-construction. Nous illustrons ce flot de conception avec la modélisation et le déploiement de plusieurs applications sur deux plates-formes différentes. La première plate-forme considérée est MPARM, une plate-forme virtuelle, basée sur des processeurs ARM et structurée avec des clusters, où chacun contient plusieurs cœurs. Pour cette plate-forme, nous avons considérée les applications suivantes: la factorisation de Cholesky, le décodage MPEG-2, le décodage MJPEG, la Transformée de Fourier Rapide et un algorithme de demosaicing. La seconde plate-forme est P2012/STHORM, une plate-forme multi-cœur, basée sur plusieurs clusters capable d'une gestion énergétique efficace. L'application considérée sur P2012/STHORM est l'algorithme HMAX. Les résultats expérimentaux montrent l'intérêt du flot de conception, notamment l'analyse rapide des performances ainsi que la modélisation au niveau du système, la génération de code et le déploiement. / The advent of many-core platforms is nowadays challenging our capabilities for efficient and predictable design. To meet this challenge, designers need methods and tools for guaranteeing essential properties and determining tradeoffs between performance and efficient resource management. In the process of designing a mixed software/hardware system, functional constraints and also extra-functional specifications should be taken into account as an essential part for the design of embedded systems. The impact of design choices on the overall behavior of the system should also be analyzed. This implies a deep understanding of the interaction between application software and the underlying execution platform. We present a rigorous model-based design flow for building parallel applications running on top of many-core platforms. The flow is based on the BIP - Behavior, Interaction, Priority - component framework and its associated toolbox. The method allows generation of a correct-by-construction mixed hardware/software system model for manycore platforms from an application software and a mapping. It is based on source-to-source correct-by-construction transformations of BIP models. It provides full support for modeling application software and validation of its functional correctness, modeling and performance analysis of system-level models, code generation and deployment on target many-core platforms. Our design flow is illustrated through the modeling and deployment of various software applications on two different hardware platforms; MPARM and platform P2012/STHORM. MPARM is a virtual ARM-based multi-cluster manycore platform, configured by the number of clusters, the number of ARM cores per cluster, and their interconnections. On MPARM, the software applications considered are the Cholesky factorization, the MPEG-2 decoding, the MJPEG decoding, the Fast Fourier Transform and the Demosaicing algorithm. Platform 2012 (P2012/STHORM) is a power efficient manycore computing fabric, which is highly modular and based on multiple clusters capable of aggressive fine-grained power management. As a case study on P2012/STHORM, we used the HMAX algorithm. Experimental results show the merits of the design flow, notably performance analysis as well as correct-by-construction system level modeling, code generation and efficient deployment.

Nous présentons dans cette thèse intitulée "Développement d'algorithmes répartis corrects par construction" nos travaux sur le développement et la vérification formels d'algorithmes répartis. Nous nous intéressons à ces algorithmes, à cause de la difficulté de leur vérification et validation. Pour analyser ces algorithmes, nous avons choisi d'utiliser Event B pour le raffinement de modèles, la vérification de propriétés de sûreté, et TLA, pour la vérification des propriétés temporelles (vivacité et équité). Nous nous sommes focalisé sur le paradigme de correction-par-construction, basé sur la modélisation par raffinement, la preuve de propriétés, ainsi que la réutilisation de modèles/preuves/propriétés (~ patrons de conception) pour guider le développement formel des algorithmes étudiés. Nous avons mis en place un paradigme de développement lors duquel un algorithme réparti est dans un premier temps caractérisé par les services qu'il fournit, et qui sont ensuite exprimés par des propriétés de vivacité, guidant la construction des modèles Event B de cet algorithme. Les règles d'inférence de TLA nous permettent ensuite de détailler les propriétés de vivacité, et de guider le développement formel par raffinement de l'algorithme. Ce paradigme, appelé "service-as-event", est caractérisé par des diagrammes d'assertions permettant de représenter les propriétés de vivacité (en prenant en compte l'équité) des algorithmes répartis étudiés, de comprendre leurs mécanismes. Ce paradigme nous a permis d'analyser des algorithmes de routage (Anycast RP de Cisco Systems et XY pour les réseaux-sur-puce (NoC)), des algorithmes de snapshot et des algorithmes d'auto-stabilisation. / The subject of this thesis is the formal development and verification of distributed algorithms. We are interested in this topic, because proving that a distributed algorithm satisfies given specification and properties is a difficult task. We choose to use the Event B method (refinement, safety properties) and the temporal logic TLA (fairness, liveness properties) for modelling the distributed algorithms. There are several existing approaches for formalising distributed algorithms, and we choose to focus on the "correct-by-construction" paradigm, which is characterised by the use of model refinement, proof of properties (safety, liveness) and reuse of formal models/proofs/properties, developments (~ design patterns) for modelling distributed algorithms. Our works introduce a paradigm which allows us to describe an algorithm with a set of services/functionalities, which are then expressed using liveness properties. These properties guide us in developing the formal Event B models of the studied algorithms. Inference rules from TLA allow to decompose the liveness properties, therefore detailing the services and guiding the refinement process. This paradigm, called "service-as-event" is also characterized by (assertions) diagrams, which allow to graphically represent liveness properties (with respect to fairness hypotheses) and detail the mecanisms and functioning of the studied distributed algorithms. The "service-as-event" paradigm allowed us to develop and verify the following algorithms : routing algorithms, such as Anycast RP (Cisco Systems), XY for Networks-on-Chip (NoC), snapshot and self-* algorithms.

Les systèmes critiques dépendent du fait que leurs composants logiciels fournissent des services aux comportements corrects (c'est-à-dire satisfaisant leurs exigences). De plus, dans de nombreux cas, ces systèmes doivent être adaptés ou reconfigurés en cas de pannes ou quand des évolutions d'exigences ou de qualité de service se produisent. Quand ces évolutions peuvent être capturées au niveau logiciel, il devient possible de les traiter en utilisant la notion de substitution. En effet, le composant logiciel du système source peut être substitué par un autre composant logiciel pour construire un nouveau système cible. Dans le cas de systèmes critiques, cette opération impose que le nouveau système cible se comporte correctement en préservant, autant que possible, les propriétés de sécurité et de sûreté du système source pendant et après l'opération de substitution. Dans cette thèse, les systèmes étudiés sont modélisés par des systèmes états-transitions. Pour modéliser la substitution de systèmes, la méthode Event-B a été choisie car elle est adaptée à la modélisation de systèmes états-transitions et permet de bénéficier des avantages du raffinement, de la preuve et de la disponibilité d'un outil puissant avec la plate-forme Rodin.Cette thèse fournit un modèle générique pour la substitution de systèmes qui inclut différentes situations comme le démarrage à froid et le démarrage à chaud, mais aussi la possibilité de dégradation ou d'extension de systèmes ou de substitution équivalente. Cette approche est d'abord utilisée pour formaliser la substitution dans le cas de systèmes discrets appliqués à la compensation de Services Web. Elle permet de modéliser la compensation correcte. Par la suite, cette approche est mise en œuvre dans le cas des systèmes caractérisés par des comportements continus comme les systèmes hybrides. Pour modéliser des comportements continus avec Event-B, le plug-in Theory pour Rodin est examiné et s'avère performant pour modéliser des systèmes hybrides. Cela nous permet de proposer un mécanisme de substitution correct pour des systèmes avec des comportements continus. L'exigence de sûreté devient alors le maintien de la sortie du système dans une enveloppe de sûreté. Pour finir, l'approche proposée est généralisée, permettant la dérivation des modèles précédemment définis pour la compensation de Services Web par le raffinement et la réutilisation de preuves entre des modèles de systèmes. / Safety-critical systems depend on the fact that their software components provide services that behave correctly (i.e. satisfy their requirements). Additionally, in many cases, these systems have to be adapted or reconfigured in case of failures or when changes in requirements or in quality of service occur. When these changes appear at the software level, they can be handled by the notion of substitution. Indeed, the software component of the source system can be substituted by another software component to build a new target system. In the case of safety-critical systems, it is mandatory that this operation enforces that the new target system behaves correctly by preserving the safety properties of the source system during and after the substitution operation.In this thesis, the studied systems are modeled as state-transition systems. In order to model system substitution, the Event-B method has been selected as it is well suited to model such state-transition systems and it provides the benefits of refinement, proof and the availability of a strong tooling with the Rodin Platform.This thesis provides a generic model for system substitution that entails different situations like cold start and warm start as well as the possibility of system degradation, upgrade or equivalence substitutions. This proposal is first used to formalize substitution in the case of discrete systems applied to web services compensation and allowed modeling correct compensation. Then, it is also used for systems characterized by continuous behaviors like hybrid systems. To model continuous behaviors with Event-B, the Theory plugin for Rodin is investigated and proved successful for modeling hybrid systems. Afterwards, a correct substitution mechanism for systems with continuous behaviors is proposed. A safety envelope for the output of the system is taken as the safety requirement. Finally, the proposed approach is generalized, enabling the derivation of the previously defined models for web services compensation through refinement, and the reuse of proofs across system models.

Les nouveaux systèmes ont souvent recours à une implémentation distribuée du logiciel, pour des raisons d'efficacité et à cause de l'emplacement physique de certains capteurs et actuateurs. S'assurer de la correction d'un logiciel distribué est difficile car cela impose de considérer tous les enchevêtrements possibles des actions exécutées par des processus distincts. Cette thèse propose une méthode pour générer, à partir d'un modèle d'application haut niveau, une implémentation distribuée correcte et efficace. Le modèle de l'application comporte des composants communiquant au moyen d'interactions multiparties avec priorités. L'exécution d'une interaction multipartie, qui correspond à un pas de la sémantique, change de façon atomique l'état de tous les composants participant à l'interaction. On définit une implantation distribuée comme un ensemble de processus communiquant par envoi de message asynchrone. La principale difficulté est de produire une implémentation correcte et efficace des interactions multiparties avec priorités, en utilisant uniquement l'envoi de message comme primitive. La méthode se fonde sur un flot de conception rigoureux qui raffine progressivement le modèle haut niveau en un modèle bas niveau, à partir duquel le code pour une plateforme particulière est généré. Tous les modèles intermédiaires apparaissant dans le flot sont exprimés avec la même sémantique que le modèle original. À chaque étape du flot, les interactions complexes sont remplacés par des constructions utilisant des interactions plus simples. En particulier, le dernier modèle obtenu avant la génération du code ne contient que des interactions modélisant l'envoi de message. La correction de l'implémentation est obtenue par construction. L'utilisation des interactions multiparties comme primitives dans le modèle de l'application permet de réduire très significativement l'ensemble des états atteignables, par rapport à un modèle équivalent mais utilisant des primitives de communication plus simples. Les propriétés essentielles du système sont vérifiées à ce niveau d'abstraction. Chaque transformation constituante du flot de conception est suffisamment simple pour être complètement formalisée et prouvée, en termes d'équivalence observationelle ou d'équivalence de trace entre le modèles avant et après transformation. L'implémentation ainsi obtenue est correcte par rapport au modèle original, ce qui évite une coûteuse vérification a posteriori. Concernant l'efficacité, la performance de l'implémentation peut être optimisée en choisissant les paramètres adéquats pour les transformations, ou en augmentant la connaissance des composants. Cette dernière solution requiert une analyse du modèle de départ afin de calculer la connaissance qui est réutilisée pour les étapes ultérieures du flot de conception. Les différentes transformations et optimisations constituant le flot de conception ont été implémentées dans le cadre de BIP. Cette implémentation a permis d'évaluer les différentes possibilités ainsi que l'influence des différents paramètres, sur la performance de l'implémentation obtenue avec plusieurs exemples. Le code généré utilise les primitives fournies par les sockets POSIX, MPI ou les pthreads pour envoyer des messages entre les processus. / Distributed software is often required for new systems, because of efficiency and physical distribution and sensors and actuators. Ensuring correctness of a distributed implementation is hard due to the interleaving of actions belonging to distinct processes. This thesis proposes a method for generating a correct and efficient distributed implementation from a high-level model of an application. The input model is described as a set of components communicating through prioritized multiparty interactions. Such primitives change the state of all components involved in an interaction during a single atomic execution step. We assume that a distributed implementation is a set of processes communicating through asynchronous message-passing. The main challenge is to produce a correct and efficient distributed implementation of prioritized multiparty interactions, relying only on message-passing. The method relies on a rigorous design flow refining the high-level model of the application into a low-level model, from which code for a given platform is generated. All intermediate models appearing in the flow are expressed using the same semantics as the input model. Complex interactions are replaced with constructs using simpler interactions at each step of the design flow. In particular, the last model obtained before code generation contains only interactions modeling asynchronous message passing. The correctness of the implementation is obtained by construction. Using multiparty interaction reduces drastically the set of reachable states, compared to an equivalent model expressed with lower level primitives. Essential properties of the system are checked at this abstraction level. Each transformation of the design flow is simple enough to be fully formalized and proved by showing observational equivalence or trace equivalence between the input and output models. The obtained implementation is correct with respect to the original model, which avoids an expensive a posteriori verification. Performance can be optimized through adequate choice of the transformation parameters, or by augmenting the knowledge of components. The latter solution requires to analyze the original model to compute the knowledge, that is reused at subsequent steps of the decentralization. The various transformations and optimizations constituting the design flow have been implemented using the BIP framework. The implementation has been used to evaluate the different possibilities, as well the influence of parameters of the design flow, on several examples. The generated code uses either Unix sockets, MPI or pthreads primitives for communication between processes.

Les systèmes cyber-physiques mélangent des comportements physiques continus, tel la vitesse d'un véhicule, et des comportement discrets, tel que le régulateur de vitesse d'un véhicule. Ils sont désormais omniprésents dans notre société. Un grand nombre de ces systèmes sont dits critiques, i.e. une mauvaise conception entraînant un comportement non prévu, un bug, peut mettre en danger des êtres humains. Il est nécessaire de développer des méthodes pour garantir le bon fonctionnement de tels systèmes. Les méthodes formelles regroupent des procédés mathématiques pour garantir qu'un système se comporte comme attendu, par exemple que le régulateur de vitesse n'autorise pas de dépasser la vitesse maximale autorisée. De récents travaux ont permis des progrès significatifs dans ce domaine, mais l'approche adoptée est encore monolithique, i.e. que le système est modélisé d'un seul tenant et est ensuite soumis à la preuve. Notre problématique est comment modéliser efficacement des systèmes cyber-physiques dont la complexité réside dans une répétition de morceaux élémentaires. Et une fois que l'on a obtenu une modélisation, comment garantir le bon fonctionnement de tels systèmes. Notre approche consiste à modéliser le système de manière compositionnelle. Plutôt que de vouloir le modéliser d'un seul tenant, il faut le faire morceaux par morceaux, appelés composants. Chaque composant correspond à un sous-système du système final qu'il est simple de modéliser. On obtient le système complet en assemblant les composants ensembles. Ainsi une usine de traitement des eaux est obtenue en assemblant différentes cuves. L'intérêt de cette méthode est qu'elle correspond à l'approche des ingénieurs dans l'industrie : considérer des éléments séparés que l'on compose ensuite. Mais cette approche seule ne résout pas le problème de la preuve de bon fonctionnement du système. Il faut aussi rendre la preuve compositionnelle. Pour cela, on associe à chaque composant des propriétés sur ses entrées et sortie, et on prouve qu'elles sont respectées. Cette preuve peut être effectué par un expert, mais aussi par un ordinateur si les composants sont de tailles raisonnables. Il faut ensuite nous assurer que lors de l'assemblage des composants, les propriétés continuent à être respectées. Ainsi, la charge de la preuve est reportée sur les composants élémentaires, l'assurance du respect des propriétés désirées est conservée lors des étapes de composition. On peut alors obtenir une preuve du bon fonctionnement de systèmes industriels avec un coût de preuve réduit. Notre contribution majeure est de proposer une telle approche compositionnelle à la fois pour modéliser des systèmes cyber-physiques, mais aussi pour prouver qu'ils respectent les propriétés voulues. Ainsi, à chaque étape de la conception, on s'assure que les propriétés sont conservées, si possible à l'aide d'un ordinateur. Le système résultant est correct par construction. De ce résultat, nous avons proposé plusieurs outils pour aider à la conception de systèmes cyber-physiques de manière modulaire. On peut raisonner sur les propriétés temporelles de tels systèmes, par exemple est-ce que le temps de réaction d'un contrôleur est suffisamment court pour garantir le bon fonctionnement. On peut aussi raisonner sur des systèmes où un mode nominal cohabite avec un mode d'urgence. / Cyber-physical systems mix continuous physical behaviors, e.g. the velocity of a vehicle, and discrete behaviors, e.g. the cruise-controller of the vehicle. They are pervasive in our society. Numerous of such systems are safety-critical, i.e. a design error which leads to an unexpected behavior can harm humans. It is mandatory to develop methods to ensure the correct functioning of such systems. Formal methods is a set of mathematical methods that are used to guarantee that a system behaves as expected, e.g. that the cruise-controller does not allow the vehicle to exceed the speed limit. Recent works have allowed significant progress in the domain of the verification of cyber-physical systems, but the approach is still monolithic. The system under consideration is modeled in one block. Our problematic is how to efficiently model cyber-physical systems where the complexity lies in a repetition of elementary blocks. And once this modeling done, how guaranteeing the correct functioning of such systems. Our approach is to model the system in a compositional manner. Rather than modeling it in one block, we model it pieces by pieces, called components. Each component correspond to a subsystem of the final system and are easier to model due to their reasonable size. We obtain the complete system by assembling the different components. A water-plant will thus be obtained by the composition of several water-tanks. The main advantage of this method is that it corresponds to the work-flow in the industry : consider each elements separately and compose them later. But this approach does not solve the problem of the proof of correct functioning of the system. We have to make the proof compositional too. To achieve it, we associate to each component properties on its inputs and outputs, then prove that they are satisfied. This step can be done by a domain expert, but also by a computer program if the component is of a reasonable size. We have then to ensure that the properties are preserved through the composition. Thus, the proof effort is reported to elementary components. It is possible to obtain a proof of the correct functioning of industrial systems with a reduced proof effort. Our main contribution is the development of such approach in Differential Dynamic Logic. We are able to modularly model cyber-physical systems, but also prove their correct functioning. Then, at each stage of the design, we can verify that the desired properties are still guaranteed. The resulting system is correct-by-construction. From this result, we have developed several tools to help for the modular reasoning on cyber-physical systems. We have proposed a methodology to reason on temporal properties, e.g. if the execution period of a controller is small enough to effectively regulate the continuous behavior. We have also showed how we can reason on functioning modes in our framework.

Dans cette thèse, nous avons étudié et développé un environnement de preuve pour les algorithmes distribués. Nous avons choisi de combiner d’une part l’approche "correct-par-construction" basée sur la méthode "B évènementielle" et d’autre part les calculs locaux comme un outil de codage et de preuve d’algorithmes distribués. Ainsi, nous avons proposé un patron et une approche qui caractérisent d’une façon incrémentale une démarche générale de preuve de plusieurs classes d’algorithmes distribués. Les solutions proposées sont validées et implémentées par un outil de preuve appelé B2Visidia. / In this thesis, we have studied and developed a proof environment for distributed algorithms. We have chosen to combine the “correct-by-construction” approach based on the “Event-B” method and the local computations models. These models define abstract computing processes for solving problems by distributed algorithms. Thus, we have proposed a pattern and an approach to characterize a general approach to prove several classes of distributed algorithms. The proposed solutions are implemented by a tool called B2Visidia.

Dependent type theories are a kind of mathematical foundations investigated both for the formalisation of mathematics and for reasoning about programs. They are implemented as the kernel of many proof assistants and programming languages with proofs (Coq, Agda, Idris, Dedukti, Matita, etc). Dependent types allow to encode elegantly and constructively the universal and existential quantifications of higher-order logics and are therefore adapted for writing logical propositions and proofs. However, their usage is not limited to the area of pure logic. Indeed, some recent work has shown that they can also be powerful for driving the construction of programs. Using more precise types not only helps to gain confidence about the program built, but it can also help its construction, giving rise to a new style of programming called Type-Driven Development. However, one difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories (like CIC and ML) from the fact that in a non-empty context, the propositional equality allows us to prove as equal (with the induction principles) terms that are not judgementally equal, which implies that the typechecker can't always obtain equality proofs by reduction. As far as possible, we would like to solve such proof obligations automatically, and we absolutely need it if we want dependent types to be use more broadly, and perhaps one day to become the standard in functional programming. In this thesis, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. However, the method that we follow is independent from the language being used, and this work could be reproduced in any dependently-typed language. We present an original type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression that they represent, and show how it allows us to easily construct and manipulate proofs. We build a hierarchy of correct-by-construction tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs. Finally, and as a conclusion, we discuss the trust we can have in such machine-checked proofs.

As technological advancements and manufacturing techniques continues to bring us more complex and powerful hardware, software engineers struggle to keep up with this rapid progress and reap the benefits brought by this hardware. In the field of safety-critical system development, where a thorough understanding and deterministic nature of the hardware often is required, the cost of development closely relates to the complexity of the hardware used. For software developers to be able to reap the benefits of the technological advancement in hardware design, a Correct-by-Construction with a model- based design flow seem promising. Even though there seem to be significant benefits in using a Correct-by-Construction workflow for developing safety- critical systems, it is far from exclusively used within the industry. Therefore, this thesis illustrates how a model-based design flow should be applied when developing safety-critical systems for usage in the rail transport sector. This thesis also explores the benefits Correct-by-Construction can bring to the development process of safety-critical systems. Within this thesis, two different modeling tools, ForSyDe and Simulink, were used to achieve a model-based design flow. The functionality of these tools is investigated to see how they can be used for developing safety-critical systems, meeting the EN 50128 standard. The result presented is an example of how these tools can be used within a model-based design flow which meets the EN 50128 standard for developing Safety Integrity Level (SIL) 4 systems. The thesis also compares the tools investigated and highlights their differences. Finally, future work required to create a complete Correct-by-Construction workflow that complies with the EN 50128 standard requirements for system development is identified. / Allt eftersom teknologiska framsteg och tillverkningstekniker fortsätter att ge oss tillgång till mer komplex och kraftfull hårdvara så kämpar mjukvaruingenjörer fibrilit med att kunna hänga med i denna utvecklingstakt och kunna utnyttja de nya möjligheterna som denna nya hårdvara ger. Inom fältet för säkerhetskritiska system, där en genomgående förståelse av och deterministiska egenskaper för hårdvara ofta krävs, så är kostnaden för utveckling nära relaterat till komplexiteten för hårdvaran som används. För att kunna ta till vara på de fördelar som dessa nya teknologiska framsteg för med sig så föreslås ofta användningen av utvecklingsprocessen Korrektvid- Konstruktion. Även fast det verkar finnas stora fördelar med att använda Korrekt-vid-Konstruktion som utvecklingsprocess så har det inte sett en bred användning inom industrin. På grund av detta så försöker denna avhandling svara på hur ett modelleringsbaserat utvecklingsflöde kan användas vid utveckling av säkerhetskritiska system för tågtransportsektorn. Arbetet undersöker även fördelarna med användningen av Korrekt-vid-Konstruktion vid utveckling av säkerhetskritiska system. Arbetet i denna avhandling undersöker hur två olika modeleringsverktyg, ForSyDe och Simulink, kan användas i ett modeleringsbasert utvecklingsflöde. Funktionaliteten för dessa modeleringsverktyg undersöks för att se hur dem kan användas för utveckling av säkerhetskritiska system på ett sätt som klarar av kraven i EN 50128 standarden. Resultaten som presenteras är ett exempel på hur dessa verktyg kan användas i ett modeleringsbaserat utvecklingsflöde som möter kraven i EN 50128 standarden för utveckling av SIL 4 system. Arbetet jämför även de undersökta modeleringsverktygen för att påvisa deras skillnader. Till sist så beskrivs det framtida arbete som krävs för att få till en komplett utvecklingsprocess som är Korrekt-vid-Konstruktion och även möter systemutvecklingskraven i EN 50128 standarden.