Letteratura scientifica selezionata sul tema "Raffinement et preuve"

International audience We examine the $q=1$ and $t=0$ special cases of the parking functions conjecture. The parking functions conjecture states that the Hilbert series for the space of diagonal harmonics is equal to the bivariate generating function of $area$ and $dinv$ over the set of parking functions. Haglund recently proved that the Hilbert series for the space of diagonal harmonics is equal to a bivariate generating function over the set of Tesler matrices–upper-triangular matrices with every hook sum equal to one. We give a combinatorial interpretation of the Haglund generating function at $q=1$ and prove the corresponding case of the parking functions conjecture (first proven by Garsia and Haiman). We also discuss a possible proof of the $t = 0$ case consistent with this combinatorial interpretation. We conclude by briefly discussing possible refinements of the parking functions conjecture arising from this research and point of view. $\textbf{Note added in proof}$: We have since found such a proof of the $t = 0$ case and conjectured more detailed refinements. This research will most likely be presented in full in a forthcoming article. On examine les cas spéciaux $q=1$ et $t=0$ de la conjecture des fonctions de stationnement. Cette conjecture déclare que la série de Hilbert pour l'espace des harmoniques diagonaux est égale à la fonction génératrice bivariée (paramètres $area$ et $dinv$) sur l'ensemble des fonctions de stationnement. Haglund a prouvé récemment que la série de Hilbert pour l'espace des harmoniques diagonaux est égale à une fonction génératrice bivariée sur l'ensemble des matrices de Tesler triangulaires supérieures dont la somme de chaque équerre vaut un. On donne une interprétation combinatoire de la fonction génératrice de Haglund pour $q=1$ et on prouve le cas correspondant de la conjecture dans le cas des fonctions de stationnement (prouvé d'abord par Garsia et Haiman). On discute aussi d'une preuve possible du cas $t=0$, cohérente avec cette interprétation combinatoire. On conclut en discutant brièvement les raffinements possibles de la conjecture des fonctions de stationnement de ce point de vue. $\textbf{Note ajoutée sur épreuve}$: j'ai trouvé depuis cet article une preuve du cas $t=0$ et conjecturé des raffinements possibles. Ces résultats seront probablement présentés dans un article ultérieur.

International audience It was proved by Rubey that the number of fillings with zeros and ones of a given moon polyomino thatdo not contain a northeast chain of a fixed size depends only on the set of column lengths of the polyomino. Rubey’sproof uses an adaption of jeu de taquin and promotion for arbitrary fillings of moon polyominoes and deduces theresult for 01-fillings via a variation of the pigeonhole principle. In this paper we present the first completely bijectiveproof of this result by considering fillings of almost-moon polyominoes, which are moon polyominoes after removingone of the rows. More precisely, we construct a simple bijection which preserves the size of the largest northeast chainof the fillings when two adjacent rows of the polyomino are exchanged. This bijection also preserves the column sumof the fillings. In addition, we also present a simple bijection that preserves the size of the largest northeast chains, therow sum and the column sum if every row of the filling has at most one 1. Thereby, we not only provide a bijectiveproof of Rubey’s result but also two refinements of it. Rubey a montré que le nombre de remplissages d’un polyomino lunaire donné par des zéros et des uns quine contiennent pas de chaîne nord-est d’une taille fixée ne dépend que de l’ensemble des longueurs des colonnesdu polyomino. La preuve de Rubey utilise une adaptation du jeu de taquin et de la promotion sur des remplissagesarbitraires de polyominos lunaires et déduit le résultat pour les remplissages 0/1 par inclusion-exclusion. Dans cetarticle, nous présentons la première preuve bijective de ce résultat en considérant des remplissages de polyominospresque lunaires, qui sont des polyominos lunaires dont on a supprimé une ligne. Plus précisément, nous construisonsune bijection simple qui préserve la taille de la plus longue chaîne nord-est des remplissages lorsque deux lignesadjacentes du polyomino sont échangées. Cette bijection préserve aussi la somme des colonnes des remplissages. Enoutre, nous présentons aussi une bijection simple qui préserve la taille de la plus longue chaîne nord-est, la sommedes lignes et la somme des colonnes si chaque ligne du remplissage contient au plus un 1. Nous fournissons donc nonseulement une preuve bijective du résultat de Rubey, mais aussi deux raffinements de celui-ci.

Le sujet de cette thèse est l'étude de la vérification et de la correction de spécifications B dans le contexte d'une approche CBSE ("Component-Based Software Engineering"). La méthode B est reconnue comme une méthode formelle bien outillée pour développer formellement des logiciels, elle dispose du raffinement et de prouveurs permettant un développement rigoureux. L'approche CBSE consiste à développer des logiciels par assemblage de composants, elle trouve son intérêt pour des systèmes de grandes tailles. Cette thèse comprend trois contributions principales. La première est la mise en évidence de schémas de constructions B basés sur le raffinement et l'inclusion de machines B ainsi que l'étude de ces schémas pour modéliser des relations entre des Systèmes de Transitions Etiquetés (STEs). La deuxième contribution consiste en l'utilisation de deux formalismes : (i) le formalisme UML pour spécifier l'assemblage de deux interfaces (fournie et requise) et de plusieurs composants ainsi que les communications entre composants, (ii) le formalisme B pour vérifier les assemblages. La troisième contribution étudie l'aide à la correction des spécifications B à partir de l'échec de la preuve en B. Cette étude est d'abord générale et indépendante du contexte, puis elle tient compte du contexte CBSE et s'intérresse à la détection et la correction des incompatibilités : pour l'assemblage de deux interfaces, on corrige les adaptateurs en considérant les trois niveaux syntaxique, sémantique et protocole, pour l'assemblage et la coordination de plusieurs composants, on corrige les médiateurs en considérant les niveaux syntaxique et protocole.

Ce travail concerne la vérification statique de programmes Java Card annotés formellement, par des méthodes déductives. Il contribue à rendre cette approche praticable dans un contexte industriel. Ce travail a donné lieu à des implantations au sein du prototype Krakatoa, et des expérimentations sur des applets industrielles. La première partie concerne le renforcement du degré d'automatisation de l'étape de vérification. La première contribution est l'interprétation fine de traits de la sémantique du langage Java Card: transactions et arrachage de la carte. La deuxième contribution propose une politique de références non-null par défaut qui permet de vérifier la validité des accès mémoire par typage statique. La troisième contribution est une analyse inter-procédurale d'inférence d'annotations par interprétation abstraite, qui permet d'obtenir des invariants de boucle, ainsi que des préconditions et des postconditions de méthodes. La seconde partie concerne la phase amont c'est-à-dire la conception des spécifications. La première contribution propose des liens entre les annotations à la JML et des spécifications abstraites. Des propriétés fonctionnelles sont exprimées à l'aide de spécifications algébriques, dont le lien avec un programme annoté est défini par une relation de raffinement. La deuxième contribution propose une utilisation structurée de diagrammes UML permettant d'engendrer des annotations, pour vérifier des propriétés de sûreté spécifiques (e. G. Invariants de structure, utilisation de protocoles). Enfin, une perspective est ouverte sur la définition et la propagation automatique d'annotations pour aider à l'audit de sécurité des applets Java Card<br>This work is about static verification of formally-annotated Java Card programs, by deductive methods. It aims at making such an approach practicable in an industrial setting. Implementations have been performed inside the Krakatoa prototype, and experiments were conducted on industrial applets. The first part concerns the improvement of the automation in the verification step. The first contribution is a precise interpretation of the semantics of the Java Card language: transactions and card tear. The second contribution proposes a policy of non-null references, allowing to verify the validity of memory accesses by static typing. The third contribution is an interprocedural analysis for inferring annotations, by abstract interpretation, allowing to obtain loop invariants, and pre- and post-conditions for methods. The second part is about the design of specifications. The first contribution proposes links between JML-like annotations and abstract specifications. Functional properties are expressed using algebraic specifications, whose link with the program is defined by a refinement relation. The second contribution proposes a structured use of UML diagrams allowing to generate annotations, to verify specific safety properties (e. G. Structural invariants, protocol descriptions). Finally, a perspective is opened towards the definition and the automatic propagation of annotations to assist security audits of Java Card applets

Les interfaces homme-machine (IHM) multimodales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un système. Plus particulièrement, en sortie, les IHM multimodales permettent au système de restituer à l’utilisateur, l’information produite par le noyau fonctionnel en combinant sémantiquement plusieurs modalités. Dans l’optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel de conception des interfaces multimodales en sortie. Le modèle proposé se décompose en deux modèles : le modèle de fission sémantique qui décrit la décomposition de l’information à restituer en informations élémentaires, et le modèle d’allocation qui spécifie l’allocation des modalités et médias aux informations élémentaires. Nous avons également développé une formalisation B Événementiel détaillée des deux modèles : fission sémantique et allocation. Cette formalisation a été instanciée sur des études de cas puis généralisée dans un processus de développement B Événementiel cadre dans lequel s’inscrivent les modèles de fission sémantique et d’allocation. Cette formalisation a permis de procéder à la vérification de propriétés de sûreté, de vivacité et d’utilisabilité<br>Multimodal Human-Computer Interfaces (HCI) offer to users the possibility to combine interaction modalities in order to increase user interface robustness and usability. Specifically, output multimodal HCI allow system to return to the user, the information generated by the functional core by combining semantically different modalities. In order to design such interfaces for critical systems, we proposed a formal model for the design of output multimodal interfaces. The proposed model consists of two models: the semantic fission model describes the decomposition of the information to return into elementary information and the allocation model specifies the allocation of the elementary information with modalities and media. We have also developed a detailed Event B formalization for the two models: semantic fission and allocation. This formalization has been instantiated on case studies and generalized in an Event B development process framework including semantic fission and allocation models. This formalization allows to carry out safety, liveness and usability properties verification

Les systèmes informatiques envahissent notre vie quotidienne et sont devenus des éléments essentiels de chacun de nos instants de vie. La technologie de l'information est un secteur d'activités offrant des opportunités considérables pour l'innovation et cet aspect paraît sans limite. Cependant, des systèmes à logiciel intégré ont donné des résultats décevants. Selon les constats, ils étaient non fiables, parfois dangereux et ne fournissaient pas les résultats attendus. La faiblesse des pratiques de développement constitue la principale raison des échecs de ces systèmes. Ceci est dû à la complexité des logiciels modernes et au manque de connaissances adéquates et propres. Le développement logiciel fournit un cadre contribuant à simplifier la conception de systèmes complexes, afin d'en obtenir une meilleure compréhension et d'assurer une très grande qualité à un coût moindre. Dans les domaines de l'automatique, de la surveillance médicale, de l'avionique..., les systèmes embarqués hautement critiques sont candidats aux erreurs pouvant conduire à des conséquences graves en cas d'échecs. La thèse vise à résoudre ce problème, en fournissant un ensemble de techniques, d'outils et un cadre pour développer des systèmes hautement critiques, en utilisant des techniques formelles à partir de l'analyse des exigences jusqu'à la production automatique de code source, en considérant plusieurs niveaux intermédiaires. Elle est structurée en deux parties: d'une part des techniques et des outils et d'autre part des études de cas. La partie concernant des techniques et des outils présente une structure intégrant un animateur de modèles en temps-réel, un cadre de correction de modèles et le concept de charte de raffinement, un cadre de modélisation en vue de la certification, un modèle du coeur pour la modélisation en boucle fermée et des outils de générations automatiques de code. Ces cadres et outils sont utilisés pour développer les systèmes critiques à partir de l'analyse des exigences jusqu'à la production du code, en vérifiant et en validant les étapes intermédiaires en vue de fournir un modèle formel correct satisfaisant les propriétés souhaitées attendues au niveau le plus concret. L'introduction de nouveaux outils concourt à améliorer la vérification des propriétés souhaitées qui ne sont pas apparentes aux étapes initiales du développement du système. Nous évaluons les propositions faites au travers de cas d'études du domaine médical et du domaine des transports. De plus, le travail de cette thèse a étudié la représentation formelle des protocoles médicaux, afin d'améliorer les protocoles existants. Nous avons complètement formalisé un protocole réel d'interprétation des ECG, en vue d'analyser si la formalisation était conforme à certaines propriétés relevant du protocole. Le processus de vérification formelle a mis en évidence des anomalies dans les protocoles existants. Nous avons aussi découvert une structure hiérarchique pour une interprétation efficace permettant de découvrir un ensemble de conditions qui peuvent être utiles pour diagnostiquer des maladies particulières à un stade précoce. L'objectif principal du formalisme développé est de tester la correction et la consistance du protocole médical<br>Software systems are pervasive in all walks of our life and have become an essential part of our daily life. Information technology is one major area, which provides powerful and adaptable opportunities for innovation, and it seems boundless. However, systems developed using computer-based logic have produced disappointing results. According to stakeholders, they are unreliable, at times dangerous, and fail to provide the desired outcomes. Most significant reasons of system failures are the poor development practices for system development. This is due to the complex nature of modern software and lack of adequate and proper understanding. Software development provides a framework for simplifying the complex system to get a better understanding and to develop the higher fidelity quality systems at lower cost. Highly embedded critical systems, in areas such as automation, medical surveillance, avionics, etc., are susceptible to errors, which can lead to grave consequences in case of failures. This thesis intends to contribute to further the use of formal techniques for the development computing systems with high integrity. Specifically, it addresses that formal methods are not well integrated into established critical systems development processes by defining a new development life-cycle, and a set of associated techniques and tools to develop highly critical systems using formal techniques from requirements analysis to automatic source code generation using several intermediate layers with rigorous safety assessment approach. The approach has been realised using the Event-B formalism. This thesis has mainly two parts: techniques and tools and case studies. The techniques and tools section consists of development life-cycle methodology, a framework for real-time animator, refinement chart, a set of automatic code generation tools and formal logic based heart model for close loop modeling. New development methodology, and a set of associated techniques and tools are used for developing the critical systems from requirements analysis to code implementation, where verification and validation tasks are used as intermediate layers for providing a correct formal model with desired system behavior at the concrete level. Introducing new tools help to verify desired properties, which are hidden at the early stage of the system development. We also critically evaluate the proposed development methodology and developed techniques and tools through case studies in the medical and automotive domains. In addition, the thesis work tries to address the formal representation of medical protocols, which is useful for improving the existing medical protocols. We have fully formalised a real-world medical protocol (ECG interpretation) to analyse whether the formalisation complies with certain medically relevant protocol properties. The formal verification process has discovered a number of anomalies in the existing protocols. We have also discovered a hierarchical structure for the ECG interpretation efficiently that helps to find a set of conditions that can be very helpful to diagnose particular disease at the early stage. The main objective of the developed formalism is to test correctness and consistency of the medical protocol

Notre thèse se situe dans le domaine des méthodes formelles appliquées aux systèmes réactifs. Nous modélisons et traitons ces systèmes, en continuelle interaction avec leur environnement, grâce au langage synchrone Lustre. D'abord, sur la base d'un travail précurseur, nous établissons pour Lustre une méthode de preuve inductive des propriétés de sûreté. Cette méthode est optimisée, afin de prendre en compte au mieux la dynamique des systèmes. Elle est implémentée dans un outil de preuve, Gloups. Ensuite, suivant le modèle de la méthode B, nous définissons un calcul de raffinement pour Lustre. Ce calcul est à la fois adapté à Lustre et exprimé en ce langage. Les obligations de preuve qui assurent la correction du raffinement peuvent être traitées par Gloups. Pour faciliter le développement, un autre outil, Flush, génère automatiquement les obligations pour Gloups. Ainsi, nous utilisons Lustre à la fois comme langage de programmation et comme cadre formel d'un développement maîtrisé. L'intérêt de ce procédé réside dans la simplicité du langage et dans son adaptation aux systèmes réactifs : en ce domaine, notre méthode de raffinement est suffisamment expressive, sans être inutilement compliquée. Des exemples viennent démontrer l'intérêt de la méthode<br>This thesis is set into the domain of formal methods applied to reactive systems. These systems, characterized by their continuous interaction with their environment, are modeled and managed by the means of the synchronous programming language Lustre. Firstly, thanks to a previous work, we build an induction-based proof method of Lustre safety properties. The method is optimized in that it takes into account the dynamics of the systems in the best possible way. We implemented it in the Gloups proof tool. Then we define a refinement calculus for Lustre which follows the B method model. The calculus is both adapted to and expressed in Lustre. The proof obligations which ensure the refinement correctness can be handled by Gloups. In order to simplify the development, another tool called Flush automatically generates the proof obligations for Gloups. Thus we use Lustre as both a programming language and a formal development framework. The interest of our method stems from the simplicity of Lustre and its adaptation to the reactive systems: in this domain, our refinement method is expressive enough, yet not exceedingly complex. To finish, we show the interest on some examples

De nos jours, nous sommes entourés de systèmes critiques complexes tels que les microprocesseurs, les trains, les appareils intelligents, les robots, les avions, etc. Ces systèmes sont extrêmement complexes et critiques en termes de sûreté, et doivent donc être vérifiés et validés. L'utilisation de méthodes formelles à états s'est avérée efficace pour concevoir des systèmes complexes. Event-B a joué un rôle clé dans le développement de tels systèmes. Event-B est une méthode formelle de conception de systèmes à états avec une approche correcte par construction, qui met l'accent sur la preuve et le raffinement. Event-B facilite la vérification de propriétés telles que la préservation des invariants, la convergence et le raffinement en générant des obligations de preuve et en permettant de les décharger.Certaines propriétés additionnelles du système, telles que l'absence d'inter-blocage, l'atteignabilité ou encore la vivacité, doivent être explicitement encodées et vérifiées par le concepteur, ou formalisées à l'aide d'une autre méthode formelle. Une telle approche pénalise la réutilisabilité des modèles et des techniques, et peut introduire des erreurs, en particulier dans les systèmes complexes.Pour pallier cela, nous avons introduit un "framework" réflexif EB4EB, formalisé au sein de Event-B. Dans ce cadre, chacun des concepts d'Event-B est formalisé comme un objet de première classe en utilisant la logique du premier ordre (FOL) et la théorie des ensembles. EB4EB permet la manipulation et l'analyse de modèles Event-B, et permet la définition d'extensions afin de réaliser des analyses supplémentaires non intrusives sur des modèles, telles que la validation de propriétés temporelles, l'analyse de la couverture d'un invariant, ou encore l'absence de blocage. Ce framework est réalisé grâce aux théories d'Event-B, qui étendent le langage d'Event-B avec des éléments définis dans des théories, et aussi en formalisant de nouvelles obligations de preuves, qui ne sont pas présentes initialement dans Event-B.De plus, la sémantique opérationnelle d'Event-B (basée sur les traces) a été formalisée, de même qu'un cadre qui sert à garantir la correction des théorèmes définis, y compris les opérateurs et les obligations de preuve. Enfin, le cadre proposé et ses extensions ont été validés dans de multiples études de cas, notamment l'horloge de Lamport, le problème du lecteur/rédacteur, l'algorithme de Peterson, les distributeurs automatiques de billets (DAB), les véhicules autonomes, etc<br>Nowadays, we are surrounded by complex critical systems such as microprocessors, railways, home appliances, robots, aeroplanes, and so on. These systems are extremely complex and are safety-critical, and they must be verified and validated. The use of state-based formal methods has proven to be effective in designing complex systems. Event-B has played a key role in the development of such systems. Event-B is a formal system design method that is state-based and correct-by-construction, with a focus on proof and refinement. Event-B facilitates verification of properties such as invariant preservation, convergence, and refinement by generating and discharging proof obligations.Additional properties for system verification, such as deadlock-freeness, reachability, and liveness, must be explicitly defined and verified by the designer or formalised using another formal method. Such an approach reduces re-usability and may introduce errors, particularly in complex systems.To tackle these challenges, we introduced the reflexive EB4EB framework in Event-B. In this framework, each Event-B concept is formalised as a first-class object using First Order Logic (FOL) and set theory. This framework allows for the manipulation and analysis of Event-B models, with extensions for additional, non-intrusive analyses such as temporal properties, weak invariants, deadlock freeness, and so on. This is accomplished through Event-B Theories, which extend the Event-B language with the theory's defined elements, and also by formalising and articulating new proof obligations that are not present in traditional Event-B. Furthermore, Event-B's operational semantics (based on traces) have been formalised, along with a framework for guaranteeing the soundness of the defined theorems, including operators and proof obligations. Finally, the proposed framework and its extensions have been validated across multiple case studies, including Lamport's clock case study, read/write processes, the Peterson algorithm, Automated Teller Machine (ATM), autonomous vehicles, and so on

La possibilité de composer des services préexistants pour offrir des fonctionnalités plus complexes est l'un des apports principaux des architectures SOA. Ce processus de composition de services, en particulier les services Web, est généralement défini par une chorégraphie ou une orchestration de services atomiques. Ces compositions sont vues comme un système états-transitions exprimant le protocole de communication entre les services participants. Les langages de description de Workflows de services, exprimant ces compositions, souffrent de l'absence de sémantique formelle et de la présence d'ambiguïtés dans la définition de leurs constructeurs au sein des standards définissant ces langages. Les outils associés à ces langages n'offrent pas la possibilité de vérifier et de valider formellement le comportement et les propriétés des services composés obtenus. Cette thèse s'intéresse à la modélisation et à la vérification formelles de la composition de services web décrite avec le standard BPEL en utilisant la méthode B Evénementiel. L'approche proposée modélise les parties statique et dynamique de BPEL et se base sur le raffinement pour la structuration du développement d'un processus BPEL. La technique de la preuve de théorème est utilisée pour l'établissement des propriétés. Un lien un-à-un est garanti entre les éléments de BPEL et leur correspondant B Evénementiel. Cette correspondance offre un assistance aux développeurs pour l'amélioration de la qualité du processus BPEL. Cette approche a été implémentée dans l'outil BPEL2B<br>The ability to compose existing services to provide more complex functionality is one of the main benefits of SOA architecture. This services compositions process, especially Web services, is generally defined by a choreography or an orchestration of atomic services. These compositions are seen as a states-transitions systems expressing the communication protocol between the participating services. Services Workflows description languages, expressing these compositions, suffer from the lack of formal semantics and the presence of ambiguities in their constructors definitions in standards defining these languages. The associated tools do not offer the possibility to formally verify and validate the behaviour and the obtained services compositions properties. This thesis focuses on modelling and formal verification of the Web services composition described with the BPEL standard using the B event method. The proposed approach models the static and dynamic parts of BPEL and is based on refinement for structuring the BPEL process development. The theorem proving technique is used for setting properties. One-to-one link is guaranteed between the BPEL elements and their B Event corresponding. This correspondence provides assistance to developers to improve the quality of the BPEL process. This approach has been implemented in the BPEL2B tool

Dans cette thèse, nous présentons des approches formelles permettant de simplifier la modélisation et la preuve du calcul distribué. Un système distribué est défini par une collection d’entités de calcul autonomes,qui communiquent ensemble pour accomplir une tâche commune. Chaque entité exécute localement son calcul et ne peut interagir qu’avec ses voisins.Le développement et la preuve du calcul distribué est un défi qui nécessite l’utilisation de méthodes et outils avancés. Dans nos travaux de thèse,nous étudions quelques problèmes fondamentaux du distribués, en utilisant Event-B, et nous proposons des schémas de preuve basés sur une approche“correct-par-construction”. Nous considérons un système distribué défini par réseau fiable, de processus anonymes et avec un modèle de communication basé sur l’échange de messages. Dans certains cas, nous faisons abstraction du modèle de communications en utilisant le modèle des calculs locaux. Nous nous focalisons d’abord sur le problème de détection de terminaison du calcul distribué. Nous proposons un patron formel permettant de transformer des algorithmes “avec détection de terminaison locale” en des algorithmes“avec détection de terminaison globale”. Ensuite, nous explicitons les preuves de correction d’un algorithme d’énumération. Nous proposons un développement formel qui servirait de point de départ aux calculs qui nécessitent l’hypothèse d’identification unique des processus. Enfin, nous étudions le problème du snapshot et du calcul d’état global. Nous proposons une solution basée sur une composition d’algorithmes existants<br>In this work, we propose formal approaches for modeling andproving distributed algorithms. Such computations are designed to run oninterconnected autonomous computing entities for achieving a common task :each entity executes asynchronously the same code and interacts locally withits immediate neighbors. Correctness of distributed algorithms is a difficulttask and requires advancing methods and tools. In this thesis, we focus onsome basic problems of distributed computing, and we propose Event-B solutionsbased on the ”correct-by-construction” approach. We consider reliablesystems. We also assume that the network is anonymous and processes communicatewith asynchronous messages. In some cases, we refer to local computationsmodel to provide an abstraction of the distributed computations.We propose a formal framework enhancing the termination detection propertyof distributed algorithms. By relying on refinement and composition,we show that an algorithm specified with “local termination detection”, canbe reused in order to compute the same algorithm with “global terminationdetection”. We then focus on the enumeration problem : we start with anabstract initial specification of the problem, and we enrich it gradually bya progressive and incremental refinement. The computed result constitutesbasic initial steps of others distributed algorithms which assume that processeshave unique identifiers. We therefore focus on snapshot problems, andwe propose to investigate how existing algorithms can be composed, withrefinement, in order to compute a global state in an anonymous network

Les systèmes informatiques envahissent notre vie quotidienne et sont devenus des éléments essentiels de chacun de nos instants de vie. La technologie de l'information est un secteur d'activités offrant des opportunités considérables pour l'innovation et cet aspect paraît sans limite. Cependant, des systèmes à logiciel intégré ont donné des résultats décevants. Selon les constats, ils étaient non fiables, parfois dangereux et ne fournissaient pas les résultats attendus. La faiblesse des pratiques de développement constitue la principale raison des échecs de ces systèmes. Ceci est dû à la complexité des logiciels modernes et au manque de connaissances adéquates et propres. Le développement logiciel fournit un cadre contribuant à simplifier la conception de systèmes complexes, afin d'en obtenir une meilleure compréhension et d'assurer une très grande qualité à un coût moindre. Dans les domaines de l'automatique, de la surveillance médicale, de l'avionique..., les systèmes embarqués hautement critiques sont candidats aux erreurs pouvant conduire à des conséquences graves en cas d'échecs. La thèse vise à résoudre ce problème, en fournissant un ensemble de techniques, d'outils et un cadre pour développer des systèmes hautement critiques, en utilisant des techniques formelles à partir de l'analyse des exigences jusqu'à la production automatique de code source, en considérant plusieurs niveaux intermédiaires. Elle est structurée en deux parties: d'une part des techniques et des outils et d'autre part des études de cas. La partie concernant des techniques et des outils présente une structure intégrant un animateur de modèles en temps-réel, un cadre de correction de modèles et le concept de charte de raffinement, un cadre de modélisation en vue de la certification, un modèle du coeur pour la modélisation en boucle fermée et des outils de générations automatiques de code. Ces cadres et outils sont utilisés pour développer les systèmes critiques à partir de l'analyse des exigences jusqu'à la production du code, en vérifiant et en validant les étapes intermédiaires en vue de fournir un modèle formel correct satisfaisant les propriétés souhaitées attendues au niveau le plus concret. L'introduction de nouveaux outils concourt à améliorer la vérification des propriétés souhaitées qui ne sont pas apparentes aux étapes initiales du développement du système. Nous évaluons les propositions faites au travers de cas d'études du domaine médical et du domaine des transports. De plus, le travail de cette thèse a étudié la représentation formelle des protocoles médicaux, afin d'améliorer les protocoles existants. Nous avons complètement formalisé un protocole réel d'interprétation des ECG, en vue d'analyser si la formalisation était conforme à certaines propriétés relevant du protocole. Le processus de vérification formelle a mis en évidence des anomalies dans les protocoles existants. Nous avons aussi découvert une structure hiérarchique pour une interprétation efficace permettant de découvrir un ensemble de conditions qui peuvent être utiles pour diagnostiquer des maladies particulières à un stade précoce. L'objectif principal du formalisme développé est de tester la correction et la consistance du protocole médical<br>Software systems are pervasive in all walks of our life and have become an essential part of our daily life. Information technology is one major area, which provides powerful and adaptable opportunities for innovation, and it seems boundless. However, systems developed using computer-based logic have produced disappointing results. According to stakeholders, they are unreliable, at times dangerous, and fail to provide the desired outcomes. Most significant reasons of system failures are the poor development practices for system development. This is due to the complex nature of modern software and lack of adequate and proper understanding. Software development provides a framework for simplifying the complex system to get a better understanding and to develop the higher fidelity quality systems at lower cost. Highly embedded critical systems, in areas such as automation, medical surveillance, avionics, etc., are susceptible to errors, which can lead to grave consequences in case of failures. This thesis intends to contribute to further the use of formal techniques for the development computing systems with high integrity. Specifically, it addresses that formal methods are not well integrated into established critical systems development processes by defining a new development life-cycle, and a set of associated techniques and tools to develop highly critical systems using formal techniques from requirements analysis to automatic source code generation using several intermediate layers with rigorous safety assessment approach. The approach has been realised using the Event-B formalism. This thesis has mainly two parts: techniques and tools and case studies. The techniques and tools section consists of development life-cycle methodology, a framework for real-time animator, refinement chart, a set of automatic code generation tools and formal logic based heart model for close loop modeling. New development methodology, and a set of associated techniques and tools are used for developing the critical systems from requirements analysis to code implementation, where verification and validation tasks are used as intermediate layers for providing a correct formal model with desired system behavior at the concrete level. Introducing new tools help to verify desired properties, which are hidden at the early stage of the system development. We also critically evaluate the proposed development methodology and developed techniques and tools through case studies in the medical and automotive domains. In addition, the thesis work tries to address the formal representation of medical protocols, which is useful for improving the existing medical protocols. We have fully formalised a real-world medical protocol (ECG interpretation) to analyse whether the formalisation complies with certain medically relevant protocol properties. The formal verification process has discovered a number of anomalies in the existing protocols. We have also discovered a hierarchical structure for the ECG interpretation efficiently that helps to find a set of conditions that can be very helpful to diagnose particular disease at the early stage. The main objective of the developed formalism is to test correctness and consistency of the medical protocol

Ce travail concerne les premières étapes du développement de logiciels et notamment l'activité de spécification. Il consiste en l'étude de deux formalismes : la méthode B et le langage UML. Il s'appuit sur la complémentarité de ces deux approches et contribue au rapprochement des langages formels et des notations graphiques à objets. Notre sujet de thèse vise à étudier et à mettre en oeuvre des techniques de construction qui permettent de faciliter le développement de spécifications formelles dans le langage B. Nous proposons pour cela d'utiliser l'ensemble des notations UML pour faciliter et documenter la spécification formelle. Le développement est fondé sur deux vues complémentaires : une vue UML qui décrit de manière synthétique et intuitive les différents aspects du futur systrème, une vue BG qui sert de support pour la vérification et permet l'étude rigoureuse des composants spécifiés. Notre modèle de développement est basé sur la construction initiale d'un modèle UML constitué de diagrammes de classes et de diagrammes d'états-transitions. Ce modèle est transformé à l'aide de schémas de dérivation ou une spécification formelle B qui sera complétée par la suite au niveau de la définition de ses opérations et/ou par des contraintes qui ne figurent pas dans les diagrammes UML. La conception des modèles peut être facilitée par l'utilisation de patterns largement répandus au niveau du développement par objets. Nous fournissons ainsi une démarche qui permet l'utilisation de patterns pour la spécification conjointe en B et en UML. Finalement, nous proposons de générer et de prouver des obligations de preuves complémentaires à la méthode B. Le rôle de celles-ci est de vérifier des contraintes liées à l'utilisation des objets<br>This work concerns the first stages of the development of software in particular the activity of specification. He(it) consists of the study of two formalisms: the method B and the language UML. He(it) appuit on the complementarity of these two approaches and contributes to the link(merger) of the formal languages and the graphic notations with objects. Our thesis subject aims at studying and at implementing(operating) techniques of construction which allow to facilitate the development of formal specifications in the language B. We suggest for it using all the notations UML to facilitate and document the formal specification. The development is based(established) on two complementary(additional) views(sights) : A view(sight) UML which describes in a synthetic and intuitive way the various aspects of future systrème, a view(sight) BG which serves as support(medium) for the check and allows the rigorous study of the specified components. Our model of development is based on the initial construction of a model UML established(constituted) by diagrams of classes and by diagrams of states-transition. This model is transformed by means of plans of diversion or a formal specification B which will be afterward completed at the level of the definition of its operations and/or by constraints which do not appear in diagrams UML. The conception(design) of the models can be facilitated by the use of patterns widely spread at the level of the development by objects. Finally, we suggest generating and proving obligations of complementary proofs to the method B. The role of these is to verify constraints bound to the use of objects