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.