Technologies de pointe pour le développement et le déploiement de logiciels sans défaut

Séminaire d'informatique à Sherbrooke
  • Quand ? 19/04/2018 à partir de 14:00 (America/Montreal / UTC-400)
  • Où ? Local D4-1023, Faculté des sciences, UdeS
  • Nom du contact
  • Participants Conférencier : Thierry Lecomte, Directeur R&D ClearSy Systems Engineering, France www.clearsy.com
  • Ajouter l'événement au calendrier iCal

Audience : Étudiants et industriels (informaticien et ingénieur logiciel)

 

Inscription gratuite (utilisez ce formulaire Google Forms) http://bit.ly/2Imu8Ru

 

Mots-clés : méthodes formelles, logiciels et systèmes sécuritaires (Safety Integrity Level 3 & 4)

 

Résumé : 

 

Ce séminaire vise à présenter des technologies de pointe, à base de méthodes et outils formels, permettant de développer et de déployer des logiciels sans défaut pour des applications où la vie de personnes peut être mise en danger en cas de défaillance. Ces technologies ont été utilisées avec succès sur des dizaines de projets industriels de grande taille, notamment dans le domaine du transport ferré, et pour des systèmes critiques jusqu'au niveau SIL4 (Safety Integrity Level).

 

La première séance (12h à 13h) porte sur les deux sujets suivants.  Elle est dispensée sous forme magistrale avec de nombreuses démonstrations.

  • La construction du modèle formel d'un logiciel, sa preuve mathématique et la génération de son code. Cette approche descendante permet de gérer de manière progressive la complexité du logiciel et démontrer que le modèle d'implémentation satisfait le modèle de spécification. Le code est généré à l'identique du modèle d'implémentation. Ces différents aspects sont présentés et accompagnés d'exemples compréhensibles et démonstratifs.
  • La vérification formelle du paramétrage d'un logiciel. S'il est incorrect (erroné, mal formé, etc.), le paramétrage de configuration d'un logiciel critique peut conduire à une exécution contraire à la sécurité. La construction d'un modèle formel de ces données de configuration permet une vérification mathématique exhaustive et un meilleur niveau de confiance dans le logiciel critique qui les utilise. C'est particulièrement vrai lorsque ce modèle de données n'est pas trivial - il ne s'agit pas uniquement de vérifier le bon typage des données mais de garantir par exemple des propriétés topologiques (graphe) pour un réseau ferroviaire.

La deuxième séance (14h à 17h) prendra la forme d'une séance de travaux dirigés de 3 heures sur le sujet suivant.

  • L'exécution de ce logiciel sur une plateforme matérielle sécuritaire (ClearSy Safety Platform). Un logiciel n'est pas sécuritaire en soi car il est nécessaire de prendre en compte la plateforme matérielle (et ses défaillances) qui va l'exécuter. Nous présentons ici une solution mélangeant astucieusement méthode formelle et architecture redondante (2-parmi-2 matérielle, 4-parmi-4 logicielle) permettant d'implémenter des fonctions de niveau SIL4. Un seul modèle formel est utilisé pour produire deux binaires en utilisant deux chaines de génération de code différentes. Les principes de sécurité de la plateforme (vérifications statiques et dynamiques) sont hors de portée du développeur qui ne peut pas les altérer.

Cette séance permettra aux apprenants de développer leurs propres applications et à les exécuter sur la plateforme de développement sécuritaire. L'utilisation d'un PC windows ou d'une machine virtuelle Windows 10 est nécessaire pour pouvoir mettre en œuvre la plateforme.  Vous pouvez apporter votre propre ordinateur ; 28 postes de travail seront aussi disponibles dans le local.

 

Prérequis : Mis à part une connaissance du développement logiciel et un esprit logique, aucune connaissance particulière n'est nécessaire pour assister à ces présentations, les éléments de compréhension étant fournis au fur et à mesure.

 

Ce séminaire sera aussi donné à Longueuil le 18 Avril 2018, de 13h à 16h.

http://info.usherbrooke.ca/mfrappier/Seminaire-Lecomte-ClearSy-2018-04-18-Longueuil.pdf