Abstract. We consider the proof-based development of cryptographic protocols satisfying security properties. For instance, the model of Dolev- Yao provides a way to integrate a description of possible attacks, when designing a protocol. We use existing protocols and want to provide a systematic way to prove but also to design cryptographic protocols; moreover, we would like to provide proof-based guidelines or patterns for integrating cryptographic elements in an existing protocol. The goal of the paper is to present a first attempt to mix design patterns (as in software engineering) and formal methods (as a verification tool). We illustrate the technique on the well known Needham-Schroeder public key protocol and Blake-Wilson-Menezes key transport protocol. The un- derlying modelling language is Event B and is supported by the RODIN platform, which is used to validate models.

Notre travail se situe dans le cadre du développement incrémental prouvé de systèmes distribués communiquant par des canaux non fiables, en particulier des protocoles de communication utilisés dans les porte-monnaie électroniques. L'approche B événementielle est mise en application sur une étude de cas réputée du Grand Challenge et appelée Mondex. Ce travail met en avant une explication des mécanismes sous-jacents qui permettent à ce système de satisfaire les exigences initiales résumées sous la forme suivante: il n'y a pas de perte d'argent ni de création d'argent lors des transferts. Le développement permet de préserver cette propriété de sûreté attendue du système final et identifie des relations de communication spécifiques pour assurer la mise en oeuvre du protocole. Ainsi, un premier modèle énonce la spécification globale de sûreté; un second modèle raffiné décrit le comportement détaillé des différents protagonistes; un troisième modèle localise les données; un quatrième modèle élimine des variables utiles pour faciliter les preuves. Cette étude nous permet de vérifier la robustesse du protocole à la perte de messages.

Systems-on-chip (SoCs) and SoC architectures provide a collection of challenging problems related to spec- i%Gï¬%@cation, modelling techniques, security issues and structur- ing questions. We describe a design methodology integrating the event B method and characterized by the incremental and proof-controlled construction of SoC models. The essence of the methodology is the re%Gï¬%@nement of models, starting from system requirements and producing event B models for char- acterizing the system under development. The re%Gï¬%@nement is a unifying concept that ensures the consistency of the differ- ent models produced and our contribution is an illustration through a case study, namely a system for measuring the parameters of audio/video quality in the digital video broad- casting (DVB) set of digital TV standards. The %Gï¬%@rst part is the derivation of an architecture of parameters from the docu- ment ETSI TR 101 290 and the validation of the architecture using invariants of B models. The second part is the proposal of B models of the SystemC scheduler and an instantiation of these abstract models of the simulation semantics by param- eters of the SystemC codes automatically translated from the B models of the DVB system. Finally, the third part relies upon a proof-based methodology for deriving an operational semantics of a given system that is expressed by an event B model including invariant properties. 1 Introduction The design of safe and secure systems-on-chip (SoCs)can be improved through the use of formal methods, and our work is based on the development of a system [1] that measures the quality of audio/video signals in digital video broadcast- ing (DVB). The purpose of the paper is not to describe the complete development of the system but to present a part of the methodology based on the event B method [3, 12] used while developing the system. Our report is focussed on the integration of the re%Gï¬%@nement process into the validation of the resulting SystemC programs derived from the event B models; the validation is carried out through a modelling of the SystemC scheduler, and the scheduler models are derived by re%Gï¬%@nement. Figure 1 summarizes the complete process for integrat- ing the event B method into the SoC design; the key con- cept is re%Gï¬%@nement, which is a way to have a progressive view of a system while adding details; each step is validated by a proof built, either interactively, or automatically, and checked by a tool called Click'n'Prove [4, 17]. The progres- sive and proved transformation process is applied both for developing models of the system and models of the sched-

Keywords: Event B method ; Refinement ; System-on-chip ; Proof - Formal modelling ; SystemC ; Simulation ; Operational semantics

Abstract. The paper reports on practical experience with the event B method, when developing case studies, especially distributed algorithms, which are very complex to verify in practice. Using the event B method, we develop a famous distributed algorithm, namely the leader election protocol for an acyclic network, generally known as the IEEE 1394. The algorithm exists and the refinement helps us to model it entirely in an elegant way. The final model is very close to the real algorithm. Only the termination proof is missing, since it is a probabilistic algorithm, as well as the contention resolution, which is solved at a global abstract level. Modelling is clearly fundamental and complex; it should be carried out by persons able to use refinement and to manage abstractions or more precisely abstract models and proofs. Advantages of such an incremental development are multiple what we quote here and that will be explained in detail. We replay the development to improve the proof process and we obtain new distributed algorithms solving the leader election proto- col problem. Two strategies are used to build the new algorithms; a first strategy is called the contention resolution; a second strategy is called the contention prevention and is based on a priority among possible nodes of the network. The two resulting algorithms are cheaper than the original IEEE 1394 protocol and neither acknowledgement, nor confirmation is required. We show how the techniques of localisation help in deriving the final distributed algorithm. The paper is an extended version of the com- plete development of the two new algorithms and it aims to emphasize methodological aspects related to the event B development.

Keywords: Key-words: Formal method, B event-based method, refinement,safety, proofs, distributed systems.

This paper describes the structure of a library for certifying distributed algorithms, contributed by Pierre Castéran and Vincent Filou. We formalize in the Coq proof assistant the behaviour of a subclass of local computation systems, namely the LC0 graph relabeling systems. We show how this formalization allows not only to build certified LC0 systems, but also study the limitations of their control structure.

Keywords: Formal proofs, distributed algorithms, local computations, Coq

Designing power aware protocols becomes a pre-requisite to conserve energy and extend network life time. In fact, many target applications may require such features when being deployed for long periods in hostile environments, such as rescue or military operations. To assure power saving while preserving network capacity, relaying on a virtual backbone seems a promising approach. Through keeping a subset of nodes active for communication tasks, we allow other nodes to switch to sleep mode reducing consequently energy waste. However, the benefits of clustering come at a cost in terms of time and the prohibitive overhead incurred during the clusters' establishment and maintenance. In this paper, we investigate the influence of the underlying clustering algorithm on the performance of a power saving mechanism. The conducted simulations confirm the importance given to the choice of an efficient clustering algorithm to achieve energy efficiency while preserving network capacity.

The Event B modelling language provides a framework for teaching programming methodology based on the famous pre/post-specifications, together with the refinement. We illustrate the call-as-event pattern for helping users to use Event B. As teacher, we are using students to evaluate our methodology and we give comments in italic, when we have got reactions from our students: a given definition, a concept related to our methodology, for instance. We discuss points related to our lectures at different levels of the university, mainly master. Simple case studies illustrate the teaching methodology based on interactive proofs.

Test and Simulation are the only verification techniques used for any biomedical devices such as pacemaker system, implantable cardioverter/defibrillators (ICDs) etc. The construction of formal models of Pacemaker systems is a considerable practical challenge. Formal modeling of an artificial Pacemaker system is a case study proposed by the software quality research laboratory at McMaster University in the Grand Challenge Initiative. Using an incremental proof-based approach, we model functionalities of the Pacemaker. The approach is illustrated by developing a new formal model of the cardiac pacemaker system. Our contribution are in this report to model the single electrode pacemaker system using Event-B and prove it. The incremental proof-based development is mainly driven by the refinement between an abstract model of the system and its detailed design through a series of refinements. A series of refinements is progressively added the functional and the timing properties to the abstract system-level specifications using some intermediate models. The properties express system architecture, action-reaction and timing behavior. This paper uses all possible operational modes of a single electrode Pacemaker system that helps to develop better hardware. Every stage of refinement includes the detail information about operating modes. The models are expressed in Event-B modeling language and validated primarily by the ProB tool in different situation such as hysteresis and rate adapting pacing under real-time constraints. In each stages of refinements include the detail information and more events are introduced. The final step of refinement completely localized the events and similar to implementation of single electrode pacemaker operating modes system. The stepwise refinement of the single electrode Pacemaker system contributes to achieve a high degree of automatic proof.

Keywords: Abstract model, Event-B, Event-driven approach, Proof-based development, Refinement, Pacemaker, Electrode, Heart