Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

This is an old revision of the document!


Méthodes formelles et langages pour le développement de logiciels fiables dans l'industrie

The primary aim of the session is to give an opportunity to students and academics and non-academic researchers to hear about recent developments of this kind carried out in an industry context. Talks will be in French.

Dates and location

Registration

People interested in participating should register here for logistic reasons. Notice that the inscription for this day is separate from other workshops!

Program

  • 14h00 : Introduction
  • 14h05 : Emmanuel Ledinot ( Dassault Aviation) Analyse de valeur ² : regard sur 25 ans de méthodes formelles dans le secteur aéronautique
  • 14h50 : Jean-Louis Colaço ( Esterel-Technologies) SCADE: un langage formel pour l'embarqué critique
  • 15h15 : Benjamin Monate ( TrustInSoft) TrustInSoft : des méthodes formelles pour donner confiance dans les composants logiciels existants
  • 15h40 : Pause café
  • 16h00 : Dominique Bolignano ( Prove & Run) Méthodes formelles et sécurité mobile
  • 16h25 : Alain Frish ( LexiFi) LexiFi: Approche “langage” pour la description de contrats financiers
  • 16h50 : Olivier Levillain ( ANSSI) Langages de développement et sécurité — Mind your language
  • 17h15 : Pause
  • 17h25 : Philippe Bonnard (IBM)
  • 17h35 : Claire Dross ( Adacore) SPARK 2014: Vérification de Programmes Ada
  • 17h40 : Etienne Prun ( Clearsy)
  • 17h45 : Romain Bardoux ( CryptoSense)
  • 17h50 : Fabrice Le Fessant ( OcamlPro)
  • 17h55 : Conclusion
  • 18h00 : Pot
  • 19h30 : Fin

Talks

Dominique Bolignano ( Prove & Run)
Méthodes formelles et sécurité mobile

Compte tenu du nombre sans cesse croissant de téléphones mobiles et tablettes en circulation et de la multiplication de leurs usages, la sécurité mobile est en train de devenir un enjeu majeur pour la protection des utilisateurs et des fournisseurs de service. De nouvelles architectures ont été identifiées pour y faire face. Mais elles butent toutes sur le problème de réduction du nombre de bogues exploitables par des attaques de sécurité. Ces bogues se trouvent dans l’implémentation, dans la conception ou dans la configuration de la base de confiance qui comprend au minimum le noyau du système mais peut aussi inclure certaines applications.
Les méthodes formelles sont les seules techniques qui pourraient véritablement permettre de répondre à cette problématique. Mais malgré l’énorme effort de recherche et les résultats obtenus ces dernières décennies dans ce domaine, leur utilisation est restée relativement marginale, a fortiori dans le domaine de la sécurité mobile.
Prove & Run développe un outillage et une approche de méthode formelle et se propose de les rendre applicables à des problèmes à fort enjeu comme celui de la sécurité mobile.
Dans cet exposé nous décrirons nos objectifs, en termes d’outils et méthodologies, et la manière dont nous pensons pouvoir les appliquer dans un premier temps au problème de la sécurité mobile.

Jean-Louis Colaço ( Esterel-Technologies)
SCADE: un langage formel pour l'embarqué critique

L'environnement de développement SCADE permet de construire des spécifications exécutables pour des applications temps réel critique. Il s'appuie pour cela un langage synchrone aussi appelé SCADE, historiquement dérivé de Lustre et intégrant depuis sa version 6 des machines à état hiérarchiques ainsi que des structures de contrôle inspirés des Syncharts (notation graphique pour Esterel).
Son générateur de code certifié autorise la production de code (compilation vers du C) sans vérification que celui-ci est bien conforme à la spécification SCADE dont il est issu.
Nous donnerons dans cet exposé quelques éléments de la formalisation de la sémantique statique de SCADE 6 et des propriétés qui en découlent. Enfin, Nous montrerons comment il est possible de vérifier formellement des propriétés de sûreté sur des logiciels développés en SCADE.

Alain Frish ( LexiFi)
LexiFi: Approche “langage” pour la description de contrats financiers

LexiFi est un éditeur de logiciel spécialisé dans le domaine de la finance et des produits structurés. L'originalité de LexiFi est de combiner des méthodes innovantes issues des mathématiques financières et de la théorie des langages de programmation. En particulier, LexiFi a développé un langage de description des contrats financiers, permettant de traiter de manière générique, via des techniques “langages” (analyse, réécriture, compilation), la grande diversité des produits traités. L'exposé présentera ce domaine et la contribution de LexiFi, ainsi que l'utilisation par LexiFi du langage OCaml pour ses développements applicatifs.

Emmanuel Ledinot ( Dassault Aviation) - Keynote
Analyse de valeur ² : regard sur 25 ans de méthodes formelles dans le secteur aéronautique

En dépit de succès indéniables dans quelques secteurs industriels, de la progression de quelques PME en pointe et d'une recherche de qualité tout particulièrement en France, la diffusion des méthodes formelles dans l'industrie ne semble pas en rapport avec la dynamique de croissance des secteurs d'activité auxquels elles sont destinées, et ce en dépit d'un durcissement des cadres réglementaires. En s'appuyant sur le cas du secteur aéronautique et sur un retour d'expérience de 25 ans de “success” et de “failure” stories dans le transfert de méthodes formelles de la recherche vers des équipes opérationnelles de développement de logiciel embarqué, on tentera de dégager quelques facteurs à l'origine de cet échec relatif, ou de ce succès mitigé.
On considèrera l'utilisation des méthodes formelles sous le double point de vue du développement des logiciels embarqués critiques et de la qualification d'outils d'ingénierie, et on s'efforcera de dégager quelques orientations prospectives sur ce que pourrait être un positionnement des méthodes formelles plus favorable à leur diffusion.

Olivier Levillain ( ANSSI)
Langages de développement et sécurité — Mind your language

Il existe de nombreux langages informatiques, et les débats concernant leurs avantages et inconvénients respectifs sont nombreux, mais peu considèrent la question du développement d'applications sécurisées, c'est-à-dire robustes contre les actions d'agents malveillants. C'est l'optique abordée dans cette présentation, qui rebondit sur quelques illustrations dans différents langages afin de pouvoir cerner ce que seraient les bonnes propriétés d'un langage vis-à-vis de la sécurité, mais aussi des recommandations de codage pertinentes ou encore des outils pertinents pour le développement et l'évaluation d'applications de sécurité.

Benjamin Monate ( TrustInSoft)
TrustInSoft : des méthodes formelles pour donner confiance dans les composants logiciels existants

Organizers

industry.1398239037.txt.gz · Last modified: 2014/04/23 09:43 by braibant
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0