COrSS: Composition et raffinement de systèmes sûrs

ACI Sécurité Informatique

2003-2006

Mots clés:

Participants

 
Obasco/LOAC EMN (Nantes) SVF FéRIA (Toulouse) COMPOSE INRIA (Bordeaux) ARLES INRIA (Roquencourt) MODEL LORIA (Nancy)
Jean-Marc Menaud Jean-Paul Bodeveix Claus Brabrand Valérie Issarny Dominique Cansell
Gilles Muller Mamoun Filali Charles Consel Nicole Levy Stephan Merz
  Philippe Mauran Laurent Réveillère Ferda Tartanoglu Dominique Méry
  Gérard Padiou     Leonor Prensa
  Philippe Quéinnec      
  Jean-François Rolland      
  Martin Strecker      
  François Vernadat      

Résumé

Le projet s'inscrit dans le cadre d'une collaboration entre des équipes issues de la communauté système et des équipes issues de la communauté méthodes formelles. Il a pour but d'étudier des méthodes et outils de développement de services systèmes satisfaisant par construction les propriétés de sûreté et de vivacité énoncées dans leur spécification. Les fondements de ces méthodes sont le raffinement et la composition. L'expertise des équipes systèmes permettra de définir des formalismes spécifiques adaptés au développement de systèmes ainsi que les besoins en terme de raffinement et de composition. On citera par exemple, l'interaction de services dans le domaine de la téléphonie, la dérivation par raffinement de services et la composition de systèmes ouverts. Des techniques de raffinement et de composition et les règles de preuves associées seront proposées, formalisées, validées et expérimentées sur les études de cas envisagées.

Rapport à mi parcours

Réunions

2003

2004

2005

Publications dans le cadre du projet

Références

[BCL+is]
Laurent Burgy, Charles Consel, Julia Lawall, Nicolas Palix, and Laurent Reveillère. Telephony software engineering: A domain specific language approach. Technical report, LABRI, 2005 (soumis).

[BFLMSI]
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, and Gilles Muller. Vérification automatique de propriétés d'ordonnanceurs Bossa. In AFADL, ENST Paris, pages 95—109. ENST, 15-17 mars 2006 (soumis à TSI).

[BFLM05a]
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, and Gilles Muller. Applying the B formal method to the Bossa domain-specific language. In The 17th Nordic Workshop on Programming Theory, Copenhagen, Denmark, page (à paraitre). DIKU Copenhagen, Denmark, 19-21 octobre 2005.

[BFLM05b]
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, and Gilles Muller. Formal methods meet domain specific languages. In Fifth International Conference on Integrated Formal Methods (IFM), Eindhoven Netherlands, volume 3771 of Lecture Notes in Computer Science, pages 187–206, 29 November-2 December 2005.

[BFLM05c]
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, and Gilles Muller. Vérification automatique de propriétés d'ordonnanceurs Bossa. Rapport de recherche 2005-21-r, IRIT, Université Paul Sabatier, Toulouse, octobre 2005.

[BFLM06]
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, and Gilles Muller. Automatic Verification of Bossa Scheduler Properties. In Sixth International Workshop on Automated Verification of Critical Systems, page (à paraire dans ENTCS). LORIA, 18-19 september 2006.

[FIM+05]
Mamoun Filali, Valérie Issarny, Philippe Mauran, Gérard Padiou, and Philippe Quéinnec. Maximal group membership in ad hoc networks . In Sixth International Conference on Parallel Processing and Applied Mathematics , Poznan (Pologne), number 3911 in Lecture Notes in Computer Science, pages 51–58. Springer-Verlag, 11-14 septembre 2005.

[LLMM04]
Julia Lawall, A.-F. Le Meur, and Gilles Muller. On designing a target-independent DSL for safe OS process-scheduling components. In Third International Conference on Generative Programming and Component Engineering (GPCE'04), volume 3286 of Lecture Notes in Computer Science, pages 436–455, Vancouver, October 2004. Springer-Verlag.

[Lon05]
Seang Meng Long. Modélisation et preuve d'un algorithme de groupes dans les réseaux ad hoc. Rapport de recherche MASTER SLCP, IRIT, Institut National Polytechnique, Toulouse, juin 2005.

[Per04]
Florent Peres. Modélisation et vérification d'algorithmes répartis. Rapport de DEA programmation et systèmes (EDIT). Technical report, IRIT, Université Paul Sabatier, 118 Route de Narbonne, F-31062 Toulouse cedex, juillet 2004.
Ce document a été traduit de LATEX par HEVEA