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.
| Identifer | oai:union.ndltd.org:theses.fr/2013GRENM063 |
| Date | 16 September 2013 |
| Creators | Quilbeuf, Jean |
| Contributors | Grenoble, Bozga, Dorel Marius, Sifakis, Joseph |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0076 seconds