Sites Inria

Séminaire In'Tech

Validation formelle de systèmes industriels critiques

airbus - MiqsPixImaging

Le club de veille technologique In’ Tech, en partenariat avec CAP’TRONIC, organise une demi-journée de rencontres entre chercheurs et industriels sur le thème " Validation formelle de systèmes industriels critiques ", le jeudi 18 avril de 13h30 à 18h, à Inria Montbonnot.

  • Date : 18/04/2013
  • Lieu : Inria Grenoble - Rhône-Alpes, Montbonnot
  • Organisateur(s) : Inria Grenoble - Rhône-Alpes et le Cluster Isère du logiciel et des services informatiques (GRILOG)

Séminaire animé par Radu Mateescu  directeur de recherche, responsable de l’équipe CONVECS Inria

Pré-Programme

13h30 - 13h40

  • Introduction

Radu Mateescu  directeur de recherche, responsable de l’équipe CONVECS Inria 

Les composants informatiques, matériels et logiciels, sont devenus omniprésents dans tous les secteurs de la vie et de la société. Le parallélisme, la communication et la synchronisation se manifestent à tous les niveaux, depuis l'échelle microscopique des réseaux sur puce jusqu'à l'échelle macroscopique des grilles et des nuages de calcul, en passant par les ordinateurs et dispositifs embarqués multi-coeurs.

Les applications informatiques qui exploitent ces équipements sont complexes et souvent critiques, leurs défaillances pouvant avoir des conséquences lourdes en termes humains et économiques. C'est pourquoi, une conception rigoureuse des systèmes critiques, basée sur l'utilisation des méthodes formelles et assistée par des outils de validation adéquats, est devenue plus nécessaire que jamais.

Cette édition du séminaire In'Tech propose un panorama des progrès récents des méthodes formelles et des techniques de validation mises en oeuvre pour améliorer la fiabilité des systèmes critiques. Plusieurs approches de validation (preuve formelle, analyse statique, vérification, génération de tests) sont illustrées, ainsi que leurs applications en contexte industriel.

13h40 - 14h10

  • Arithmétique virgule flottante et validation

Jean-Michel Muller,  directeur de recherches au CNRS, équipe ARIC Inria

Dans la plupart des applications nécessitant du calcul numérique, les nombres sont représentés en "virgule flottante". Dans ce système, les opérations arithmétiques ne sont qu'une approximation des opérations réelles. Pour valider les applications, il est pourtant souvent préférable de les regarder comme des opérations exactes, qui ne sont pas les opérations usuelles, mais sur lesquelles on peut faire des preuves et construire des algorithmes. On donnera des exemples d'outils construits en faisant appel à ce paradigme.

14h10 - 14h40

  • An overview of the Astrée analyzer

Jérôme Feret , chercheur équipe ABSTRACTION 

Astrée is a static program analyzer aiming at proving the absence of Run Time Errors (RTE) in programs written in the C programming language. ASTREE was able to prove completely automatically the abscence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system and of the Airbus A380, and the automatic software of the Jules Vernes Automated Transfer Vehicle.
In this talk, after a short reminder of the Astree story, we give an overview of the structure of the analyzer and describe some of the abstractions that are used within the analyzer.

14h40 - 15h10

  • Des processus métier et exigences aux tests pour les grands systèmes complexes

Bruno LEGEARD , Scientific advisor, Smartesting

Les techniques de génération automatique de tests ont muri ces dix dernières années pour se déployer aujourd’hui au niveau industriel. Nous présenterons un état de l’art actualisé des technologies mises en œuvre, de leur déploiement dans le contexte de grands systèmes industriels à la fois pour le test de bout en bout, pour le test inter-composants et de composants. Les enjeux concernent l’automatisation et l’optimisation du processus de test pour augmenter le niveau de couverture des exigences et du code en diminuant l’effort global de test. Un retour d’expérience avec la technologie Smartesting CertifyIt est présenté dans le contexte d’un grand système de suivi (transport).

15h10 - 15h40

  • Formal Modeling and Verification of Concurrent Systems using CADP

Radu Mateescu  directeur de recherche, responsable de l’équipe CONVECS Inria

Asynchronous concurrency is becoming increasingly present in a large spectrum of systems (communication protocols, embedded systems, multiprocessor architectures, etc.). Due to the intrinsic complexity of asynchronous concurrency, the correct design of such systems is notoriously difficult, requiring the support of formal methods and verification tools. CADP (Construction and Analysis of Distributed Processes) is a toolbox for the design, functional verification, and performance evaluation of asynchronous concurrent systems. The toolbox, which consists currently of over 50 interconnected tools and libraries, is already used by more than 440 research institutions and companies worldwide in many application domains. CADP is also used in education, in particular for teaching the concepts of concurrency theory. This talk gives an overview of the principles, architecture and main functionalities of CADP, with a focus on the various input languages, analysis features, and software libraries that enable users to develop their own analysis tools.

15h40 - 16h30
Pause et découverte des stands

16h30 - 17h00

  • Sûreté de Fonctionnement des Logiciels Critiques : État des lieux et évolutions récentes

Julien CANCELIER,  Serma Ingénierie  

Le développement de Logiciel industriel critique est un domaine à forte contrainte sécuritaire et normative. L’utilisation de ces logiciels s’est multipliée lors de la dernière décennie.
Cette intervention présentera un historique et un état des lieux de la Sûreté de Fonctionnement des Logiciels Critiques  avec l’introduction des normes de développement associées pour les différents secteurs (aéronautique, ferroviaire, médicale, nucléaire, automobile, ...), en abordant les récentes évolutions.
Les pratiques de développement Logiciel seront introduites avec la présentation du cycle en V, des techniques formelles, de l’analyse statique et des activités de vérification & validation.
Ces pratiques de développement Logiciel s’intègrent dans la définition d’un processus de développement critique, d’une organisation adéquate (avec notamment des notions d’indépendance) afin de répondre aux contraintes normatives et de sécurité des systèmes.

17h00 - 17h30

Mathieu Clabaut , Systerel

  • Systèmes, logiciels et données : application industrielle des méthodes formelles

Que ce soit pour réaliser des logiciels, valider des données ou concevoir des systèmes, les équipes de SYSTEREL mettent en œuvre des méthodes formelles depuis plus de 15 ans. Nous présenterons un panorama de notre retour d'expérience sur la mise en œuvre industrielle de différentes méthodes formelles.

17h30 - 18h00

  • Ingénierie d'exigences fonctionnelles à l'aide de langages synchrones

Erwan Jahier , ingénieur de recherche CNRS équipe synchrone laboratoire Verimag

Dans cet exposé, nous montrons comment des outils et des langages synchrones peuvent être utilisés pour automatiser les tests fonctionnels de systèmes réactifs hétérogènes (pas nécessairement synchrones) développés incrémentalement. Ces technologies synchrones se sont avérées être particulièrement utiles pour ingénierer des exigences fonctionnelles précises, complètes et cohérentes. Nous illustrerons notre propos sur quelques cas d’études issus de systèmes de contrôle-commande de centrale de production d’énergie. 

Localisation

Mots-clés : Validation Systèmes critiques Outils de validation Vérification Preuve Méthodes formelles

Haut de page