Les projets de recherche sur B / Research Projects on B

 https://velo.wiki.ls2n.fr/lib/exe/fetch.php?media=velo:7-habrias-projets_de_recherche_b.pdf

En doutant, nous nous mettons en recherche, et en cherchant, nous
trouvons la vérité.
Pierre Abélard, le philosophe du Pallet

 

Sommaire  

Pojet MIST, Measurable Improvement with Specification Techniques 

"Measurable Improvement in Specification Techniques (MIST) is ESSI ap-
plication experiment 10228. MIST is a 16 month project involving three com-
panies :GEC-Marconi Avionics, who are the prime user ; Praxis, who are the
main subcontractor, acting as an independent reviewer ; and B-Core (UK),who
provide the tools used and consultancy. The main aims of MIST are to develop
procedures for using formal methods with current methods on safety critical
avionics software and to collect metrics to enable reasonable estimates for the
use of these procedures"
Jonathan Draper, Mission Avionics Division, GEC-Marconi Avionics 

 Projet de la Commission Européenne 

SPECTRUM, Improved competitiveness through
integration and automation of complementary
formal approaches in the development process 

 Programme FP4-ESPRIT 4 - Specific research and technological development pro-
gramme in the field of information technologies, 1994-1998 1-01-
textbf1997, 30-091997

 Projet BOM (B Optimisant la Mémoire)

Le but était d'obtenir un traducteur du langage B vers le
langage C, facilement adaptable à des contraintes mémoire (logiciels embarqués
sur cartes à puce)" 

Projet RNTL 

Projet Rodin, Rigorous Open Development En-
vironment for Complex Systems
(2004 à 2007)

Projet DEPLOY, (Industrial deployment of sys-
tem engineering methods providing high de-
pendability and productivity)
2008 à 2012 ICT 214158 DEPLOY

 Une plate-forme mécanisée et basée sur la preuve
pour la vérication d'obligations de preuve B
 BWare
INS - Ingénierie Numérique & Sécurité 

 Augmenter les outils de raisonnement sur le
langage B par des techniques SAT et SMT 
BLaSST 

February 2022 - 48 Mois 

 

Méthode outillée de modélisation formelle des
exigences pour des systèmes complexes critiques
 FORMOSE 

Le projet Formose est un projet de recherche industrielle dont l'objectif est
de produire une méthode formelle d'ingénierie des exigences (IE) orientée mo-
dèles pour des systèmes complexes critiques, supportée par un outil libre. C'est
un projet de 48 mois auquel participent 2 partenaires académiques (LACL 
porteur du projet , Institut Mines-Telecom) et deux partenaires industriels
(THALES, ClearSy). L'IE est un processus critique dans la conception de logi-
ciels et de systèmes. 

September 2014 - 48 Mois 

 CE25 - Sciences et génie du logiciel - Réseaux
de communication multi-usages, infrastructures
de hautes performances, Assistants de preuve
basés sur la théorie des ensembles interopé-
rables et sûrs  ICSPA 

December 2021 - 48 Mois 

 

Déduction Certiée  DECERT 

L'objectif du projet DECERT est de concevoir une architecture pour
des procédures de décision coopérant entre elles, avec une attention particulière
portée à des fragments de l'arithmétique (arithmétiques bornée et non-bornée,
sur les entiers et les réels, ...) et à leur combinaison avec d'autres théories concer-
nant les structures de données (listes, tableaux, ensembles, ...).  

Enrichissement de EventB et de RODIN : EventB-
Rodin-Plus  EBRP-EventB-Rodin-Plus 

14/01/2020  48 mois 

Projet CASES/Clearsy, calculateur Souverain
sûr et sécurisé 

2022, durée du projet 24 mois dans le cadre de la Stratégie nationale cyber 

Comments

Post a Comment

Popular posts from this blog

Ce que je dois à Jean-Raymond Abrial

Image
 Quand ai-je découvert Jean-Raymond Abrial ?  Peut-être bien que c'est quand j'ai fait acheter les actes de la conférence de Cargèse et que j'ai lu son article Data Semantics . Ou est-ce lors de la lecture des publications de la DER-IMA d'EDF (située à Clamart) ? Ce qui est sûr c'est que j'ai découvert Z dans le Meyer Baudoin, Méthodes de Programmation chez Eyrolles, puis dans le Delobel Adiba, Bases de données chez Dunod. Quand j'ai débuté en "informatique de gestion" (en I.U.T "Informatique") je trouvais que ce que je lisais était bien peu "scientifique". "Information" "donnée" "rubrique" etc.  Pour "donnée" j'ai appris les théorèmes de Jean-Louis Rigal qui était prof à l'Université Dauphine. Facile : Th1, "Une donnée n'est pas donnée" car c'est le résultat d'une abstraction, Th 2. "Une donnée n'est pas donnée" car une fois donnée, ce n'est...
Read more

Jean-Raymond Abrial (1938, 2025)

Image
  Jean-Raymond Abrial (1938, 2025) Jean-Raymond Abrial est décédé les 26 mai 2025 la vieille de la conférence qui a eu lieu dans le cadre des Journées Scientifiques de l'université de Nantes et qui traitait de ses travaux et de leur mise en oeuvre dans différentes domaines.J.-R Abrial est né en 1938 à Versailles. Après des études au Prytanée militaire de la Flèche, il fera l'Ecole Polytechnique. En 1960 il sera ingénieur du génie maritime. Il sera boursier du gouvernement français à Stanford University puis au Centre de Programmation de la Marine où il travaillera sur une version du langage LTR (Langage Temps Réel). C'est là que Gérard Le Lann, qui a fait partie de l'équipe ayant conçu Internet, l'a connu. J.-R Abrial est pour lui "l'un des plus grands informaticiens français ! Peu enclin à épouser les « modes » qui agitent plus ou moins régulièrement les communautés scientifiques. Liberté de penser, de créer, et liberté d'essaimer !".A Grenoble, d...
Read more

On B, Jean-Raymond Abrial

 Cet article date du temps où Jean-Raymond Abrial habitait rue des plantes à Paris. Digilog était deveni Steria, mais pas encore Clearsy. Donc d'avant 2001. On B Jean-Raymond Abrial Consultant, 26, rue des Plantes, 75014, Paris. abrial@steria.fr In  the B-Book [Abr96], an introduction entitled “What is B ?” presents it in a few pages. There is no point in reproducing this introduction here. There is, however, clearly a need to have in this book a sort of informal presentation of B complementing that of the B-Book for those readers who are not familiar with this approach. This is the purpose of this short text, where the emphasis will be put on the question of the development process with B. At the end of the text, I will also cover some more general problems concerning B (tool, education, research, future). B is o “Debugger”. The aim of B is very practical. Its ambition is to provide to industr...
Read more