N. Benaïssa and D. Méry.
Cryptologic protocols analysis using Event B.
In Alexander Marchuk, editor, Seventh International Andrei
Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS, volume 5947
of Lecture Notes in Computer Science. Springer, 15-19 June 2010.
[ bib ]
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.
Nazim Benaissa and Dominique Méry.
Développement incrémental prouvé de systèmes
répartis : le cas Mondex.
Research Report, 2008.
[ bib |
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.
Dominique Cansell, Dominique Méry, and Cyril Proch.
System-on-chip design by proof-based re International Journal on Software Tools for Technology
Transfer (STTT), 11:217-238, 03 2009.
[ bib |
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  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
Dominique Cansell and Dominique Méry.
Designing old and new distributed algorithms by replaying an
incremental proof-based development.
In Jean-Raymond Abrial and Uwe Glässer, editors, Rigorous
Methods for Software Construction and Analysis - Papers Dedicated to Egon
Börger on the Occasion of His 60th Birthday, number 5115 in Lecture Notes in
Computer Science, 2010.
[ bib ]
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.
|||Pierre Castéran, Vincent Filou, and Mohamed Mosbah. Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant. In Proceedings of Symbolic Computation in Software Science (SCSS 2009) Symbolic Computation in Software Science (SCSS 2009), page To appear, Tunisie, 09 2009. [ bib | http ]|
Pierre Castéran, Vincent Filou, and Mohamed Mosbah.
Formal Proofs of Local Computation Systems.
Rapport de recherche RR-1456-09 - Université Bordeaux 1,
[ bib |
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
|||Bilel Derbel, Mohamed Mosbah, and Akka Zemmari. Sublinear Fully Distributed Partition with Applications. Theory of Computing Systems, pages -, 2009. To appear. [ bib ]|
|||A. El Hibaoui, Y. Métivier, J.-M. Robson, N. Saheb-Djahromi, and A. Zemmari. Analysis of a randomized dynamic timetable handshake algorithm. Pure Mathematics and Applications (PuMA). à paraître. [ bib ]|
|||A. El Hibaoui, J.-M. Robson, N. Saheb-Djahromi, and A. Zemmari. Uniform election in trees and polyominoids. Discrete Applied Mathematics. à paraître. [ bib ]|
Imen Jemili, Abdelfattah Belghith, and Mohamed Mosbah.
Exploiting a clustering mechanism for power saving in ad hoc
networks: Performance evaluation.
In AICCSA 2009 IEEE/ACS International Conference on
Computer Systems and Applications, 2009. AICCSA 2009., pages
717-724, Rabat Maroc, 05 2009. IEEE Computer Science.
[ bib |
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.
|||J.-F. Marckert, N. Saheb-Djahromi, and A. Zemmari. Election algorithms with random delays in trees. In 21st Formal Power Series and Algebraic Combinatorics (FPSAC), 2009. à paraître. [ bib ]|
A simple refinement-based method for constructing algorithms.
SIGCSE Bull., 41(2):51-59, 2009.
[ bib |
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.
Dominique Méry and Neeraj Kumar Singh.
Pacemaker's Functional Behaviors in Event-B.
Research report, 2009.
[ bib |
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
|||Y. Métivier, J.-M. Robson, N. Saheb-Djahromi, and A. Zemmari. Analysis of an optimal bit complexity randomised distributed vertex colouring algorithm. In 13th International Conference On Principles Of DIstributed Systems (OPODIS 2009), 2009. à paraître. [ bib ]|
|||Y. Métivier, J.-M. Robson, N. Saheb-Djahromi, and A. Zemmari. A bit complexity efficient randomized distributed mis algorithm. In 16th International Colloquium on Structural Information and Communication Complexity (SIROCCO 2009), 2009. [ bib ]|
|||Mohamed Mosbah and Mohamed Tounsi. Automatic Implementation of Distributed Algorithms Specified in Event-B. In proceedings of Symbolic Computation in Software Science ( SCSS 2009) Symbolic Computation in Software Science (SCSS 2009), page To appear, Tunisie, 09 2009. [ bib | http ]|
|||Mohamed Tounsi, Ahmed Hadj Kacem, Mohamed Mosbah, and Dominique Méry. A Refinement Approach for Proving Distributed Algorithms : Examples of Spanning Tree Problems. In Integration of Model based Formal Methods and Tools(IMFMT 2009), Düsseldorf Allemagne, 2009. [ bib ]|
This file has been generated by bibtex2html 1.87.