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
|||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 ]|
|||Jean-François Marckert, Nasser Saheb Djahromi, and Akka Zemmari. Election Algorithms with Random Delays in Trees. In Procedings of the 21st International Conference on Formal Power Series and Algebraic Combinatorics (FPSAC 2009) In 21st International Conference on Formal Power Series and Algebraic Combinatorics (FPSAC 2009), Discrete Mathematics and Theoretical Computer Science, pages 00-00, Hagenberg Autriche, 2009. [ bib | http ]|
|||Bilel Derbel, Mohamed Mosbah, and Akka Zemmari. Sublinear Fully Distributed Partition with Applications. Theory of Computing Systems, pages -, 2009. To appear. [ bib | http ]|
|||Yves Métivier, John Michael Robson, Nasser Saheb Djahromi, and Akka Zemmari. An optimal bit complexity randomised distributed MIS algorithm. In Structural Information and Communication Complexity International Colloquium on Structural Information and Communication Complexity, Lecture notes in computer science, pages 1-15, Piran Slovénie, 05 2009. Springer-Verlag. [ bib | http ]|
|||A. El Hibaoui, Yves Métivier, John Michael Robson, Nasser Saheb Djahromi, and Akka Zemmari. Analysis of a Randomized Dynamic Timetable Handshake Algorithm. Pure Mathematics and Applications (Algebra and Theoretical Computer Science), pages -, 2009. To appear. [ bib | http ]|
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
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.
Refinement-based guidelines for algorithmic systems.
International Journal of Software and Informatics,
3(2-3):197-239, June/September 2009.
[ bib ]
Abstract The correct-by-construction approach can be supported by a progressive and incremental process controlled by the refinement of models of programs. We explore the EVENT B modelling language to illustrate the expression of our methodological proposal using proof-based patterns called guidelines. The main ob jective is to facilitate the correct- by-construction approach for designing classical sequential algorithms. We address the de- scription of guidelines for the design of programs and algorithms and the integration of proof-based aspects using the RODIN platform. More precisely, we introduce several method- ological steps identified during the development of case studies, and we propose auxiliary notions, such as refinement diagrams, for guiding users during problem analysis. A general structure characterizes the relationship between the contract, the EVENT B, and the devel- oped algorithm using a specific c application of EVENT B models and refinement. We simplify the translation of EVENT B models into algorithmic elements by promoting the use of recur- sive constructs. The resulting algorithm is proved to be sound with respect to the pre/post specification, namely, the contract. Applications rely on a dynamic programming technique that illustrates the applicability of these patterns based on a call-as-event relationship. Each proof-based development is validated using the RODIN platform. Our paper contributes to the development of patterns for assisting the proof-based development of algorithmic systems.
Keywords: Key words: EVENT B; modelling; refinement; algorithm; pattern; proof; formal method; proof-based development; correct by construction.
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 reelegant way. 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 reprecisely 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 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 conrequired. We show how the techniques of localisation help in deriving the plete development of the two new algorithms and it aims to emphasize methodological aspects related to the event B development.
Keywords: Formal method, B event-based method, refinement,safety, proofs, distributed systems.
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 to
appear 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 software engineering) and formal methods (as a veriillustrate 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.
This file has been generated by bibtex2html 1.87.