[1]  Laboratoire LABRI. Visidia, 2008 and 2010. http://www.labri.fr/projet/visidia/. [ bib ] 
[2]  Laboratoire LABRI. B2visidia, 2010. http://www.labri.fr/projet/visidia/. [ bib ] 
[3]  ClearSy. BART. http://www.clearsy.com, 2010. [ bib ] 
[4] 
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.
Springer, 1519 June 2010.
[ bib ]
Abstract. We consider the proofbased 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 proofbased 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 NeedhamSchroeder public key protocol and BlakeWilsonMenezes key transport protocol. The un derlying modelling language is Event B and is supported by the RODIN platform, which is used to validate models.

[5] 
Dominique Cansell and Dominique Méry.
Designing old and new distributed algorithms by replaying an
incremental proofbased development.
In JeanRaymond 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, 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: Keywords: Formal method, B eventbased method, refinement,safety, proofs, distributed systems. 
[6]  A. El Hibaoui, J. M. Robson, N. SahebDjahromi, and A. Zemmari. Uniform election in trees and polyominoids. Discrete Appl. Math., 158(9):981987, 2010. [ bib  DOI ] 
[7]  A. El Hibaoui, Y. Métivier, J.M. Robson, N. SahebDjahromi, and A. Zemmari. Analysis of a randomized dynamic timetable handshake algorithm. Pure Mathematics and Applications (PuMA), 19(23):159169, 2010. [ bib ] 
[8]  Dominique Méry. Refinementbased guidelines for constructing algorithms. In JeanRaymond Abrial, Michael Butler, Rajeev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock, editors, Refinement Based Methods for the Construction of Dependable Systems, number 09381 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2010. Schloss Dagstuhl  LeibnizZentrum fuer Informatik, Germany. [ bib  http ] 
[9]  Nazim Benaissa. La composition des protocoles de sécurité avec la méthode B événementielle. PhD thesis, Université Henri Poincaré Nancy 1, May 2010. [ bib ] 
[10]  Joris Rehm. Proved development of the realtime properties of the ieee 1394 root contention protocol with the eventb method. International Journal on Software Tools for Technology Transfer (STTT), 12, fevrier 2010. [ bib ] 
[11]  Dominique Méry and Neeraj Kumar Singh. Realtime animation for formal specification. In Complex Systems Design & Management (CSDM), Paris, page (to appear), 2010. [ bib ] 
[12]  Dominique Méry and Neeraj Kumar Singh. Functional behavior of a cardiac pacing system (in Press). International Journal of Discrete Event Control Systems, 1, 2010. [ bib ] 
[13]  Dominique Méry and Neeraj Kumar Singh. Technical Report on Formal Development of TwoElectrode Cardiac Pacing System. (http://hal.archivesouvertes.fr/inria00465061/en/), LORIA, 2010. [ bib  http ] 
[14]  Nazim Benaissa and Dominique Méry. Cryptographic protocols analysis in event b. In PSI 2009, Russie Novosibisrk, 20091111. Springer. [ bib  http ] 
[15]  Pierre Castéran and Vincent Filou. Tâches, types et tactiques pour les systèmes de calculs locaux. In Journées Francophones des Langages Applicatifs, pages 83110, La Ciotat, Janvier 2010. Studia Informatica,Hermann Informatique. [ bib ] 
[16]  Nazim Benaissa and Dominique Méry. Proofbased design of security protocols. In Farid Ablayev and Ernst W. Mayr, editors, Computer Science Theory and Applications 5th International Computer Science Symposium in Russia, CSR 2010, number 6072, RUSSIE, KAZAN, 2010. [ bib ] 
[17]  Projet ANRRIMEL. Développement d'algorithmes répartis. Livrable RIMEL, LORIA, Janvier/Février 2008. [ bib ] 
[18]  Projet ANRRIMEL. Intégration de contraintes tempsréel au sein d'un processus de développement incrémental basé sur la preuve. Livrable RIMEL, LORIA, Juillet 2008. [ bib ] 
[19]  Projet ANRRIMEL. Proofbased design patterns. Livrable RIMEL, LORIA, Juillet 2008. [ bib ] 
[20]  Projet ANRRIMEL. Probabilistic incremental proofbased development. Livrable RIMEL, LORIA, Décembre 2009. [ bib ] 
[21]  Projet ANRRIMEL. Formal system engineering. Livrable RIMEL, LORIA, Juillet 2009. [ bib ] 
[22]  Projet ANRRIMEL. Tools. Livrable RIMEL, LORIA, Juin 2010. [ bib ] 
[23]  D. Méry, M. Mosbah, and M. Tounsi. Integrating local computation models by refinement. In Symbolic Computation in Software Science (SCSS 2010), RISC, 2010. [ bib ] 
[24]  J. Chalopin and Y. Métivier. On the power of synchronizations between two adjacent vertices. Distributed computing, 2010. [ bib ] 
[25]  H. Hadj Kacem, M. Mosbah, N. Ouled Abdallah, and A. Zemmari. Broadcast in wireless mobile sensor networks with population protocols and extension with the rendezvous model. In 10th International Conference on New Technologies of Distributed Systems (NOTERE 2010), Tozeur, Tunisie, 31 mai  2 juin 2010. [ bib ] 
[26]  Dominique Méry, Mohammed Mosbah, and Mohammed Tounsi. Proving Distributed Algorithms by Combining Refinement and Local Computations. In AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, 2010. [ bib ] 
This file has been generated by bibtex2html 1.87.