The Coq mailing list

[David MENTRÉ <david.mentre AT bentobako.org>]

[ Sorry, French only announce for an event related to formal methods in 
France. ]

Bonjour à toutes et à tous,


Nous avons le plaisir de vous inviter au séminaire du groupe de travail 
*TransForm : Méthodes Formelles pour les systèmes de Transport*, qui 
aura lieu :
le _*22 novembre 2018*____*de 9h45 à 16h *__à____*l'IFSTTAR Villeneuve 
d'Ascq*_.

Les méthodes formelles sont des techniques basées sur des fondements 
logiques et mathématiques, et permettent la spécification, la conception 
et l'analyse de systèmes complexes, notamment en lien avec des 
problématiques de sécurité. Ces techniques sont fortement recommandées 
pour l'ingénierie des systèmes critiques, et notamment pour les systèmes 
de transport.

L'objectif du groupe TransForm est de créer un espace d'échange entre 
académiques et industriels autour de l'utilisation des méthodes 
formelles dans les systèmes de transport, tout mode confondu.

Vous trouverez le programme détaillé de cet événement et d'autres 
détails sur le groupe *ici* 
<https://filesender.ifsttar.fr/download.php?token=302b9b44-db54-f56b-471a-0d09662ff4e1&files_ids=13586&v=cd728219-1534238828>.

https://filesender.ifsttar.fr/download.php?token=302b9b44-db54-f56b-471a-0d09662ff4e1&files_ids=13586&v=cd728219-1534238828

Et voici le lien pour l'inscription gratuite mais obligatoire. La date 
limite pour l'inscription est le _*14 novembre*_ *(le nombre de places 
est limité)* :

https://docs.google.com/forms/d/e/1FAIpQLSfBxBhUPmfXnJCEvsUYa-i6hDSSlqfSave_fQlMFBPrQw7RBg/viewform


Ci-dessous le programme du séminaire et le résumé des exposés :

*9h45-10h15 : **Accueil des participants – Café*

*10h15 - 10h30 : **Introduction **(Mohamed Ghazel, IFSTTAR & David 
Mentré, MERCE – Mitsubishi Electric)*

*10h30 - 11h15 : **Utilisation des méthodes formelles dans la validation 
de données**(Erwan Mottin**& Romain Lapostolle – ClearSy)*

*11h15 - 12h : **Véhicule autonome et connecté, sûreté et sécurité: un 
cas d'étude avec TIS Analyzer**(Fabien Lheureux**& Stéphane Zimmermann – 
TrustInSoft**et Alexandre Hamez**& David Wagner – EasyMile)*

*12h - 12h10 : **Appel à participation RSSRail’2019 à Lille**(Simon 
Collart-Dutilleul – IFSTTAR)*

*12h10 - 13h40 : **Pause déjeuner autour d'un buffet*

*13h40 - 14h40 : **Tutoriel - Solveurs SAT modernes : Algorithmes et 
Applications**(Saïd Jabbour – CRIL – Univ. Artois)*

*14h40 - 15h : **Pause café*

*15h - 15h45 : **Génération avec CADP de scénarios pertinents pour 
tester les voitures autonomes**(Lina Marsso, Radu Mateescu**et Wendelin 
Serwe**- CONVECS, INRIA Grenoble et laboratoire LIG**)*

*15h45**- 16h : **Notes de fin**(Mohamed Ghazel - IFSTTAR & David 
Mentré*– *MERCE - Mitsubishi Electric)*


_*Résumés :*_

*1- Utilisation des méthodes formelles dans la validation de données 
**(Erwan Mottin**& Romain Lapostolle – ClearSy)*
Dans le ferroviaire, les logiciels critiques pour la sécurité sont 
développés et validés indépendamment des données qui les paramètrent 
telles que la topologie de la voie, les positions des signaux, les 
points kilométriques, etc. La validation des données consiste à 
s'assurer que l'ensemble de ces données est correct. Auparavant, la 
validation était entièrement humaine, menant à des activités à longues 
et fastidieuses, sujettes aux erreurs. La validation formelle des 
données est l'évolution naturelle de ce processus humain en un processus 
automatique et sécurisé. Cette présentation explique les techniques 
utilisées et expose un cas concret d’utilisation.

*2- Véhicule autonome et connecté, sûreté et sécurité : un cas d'étude 
avec TIS Analyzer**(Fabien Lheureux, Stéphane Zimmermann – 
TrustInSoft**& Alexandre Hamez, David Wagner – EasyMile)*
TrustInSoftAnalyzer est un analyseur statique garantissant l'absence de 
comportement non-défini dans du code C. Dans un premier temps, 
TrustInSoftprésentera son extension traitant le languageC++, ainsi que 
les challenges rencontrés dans son développement. La présentation 
montrera comment intégrer TrustInSoftAnalyzer à un cycle de 
développement en partant de tests existants pour arriver à une analyse 
complète de programmes.Dans un deuxième temps, Easymileprésentera le 
retour d'expérience d'utilisation de TrustInSoftAnalyzer dans le cadre 
d'un véhicule autonome. Les problématiques spécifiques à ce domaine, les 
résultats obtenus et le travail nécessaire à la mise en place seront 
abordés.

*3- Tutoriel – Solveurs SAT modernes : Algorithmes et 
Applications**(Saïd Jabbour – CRIL, Univ. Artois)*
Le problème NP-complet classique de la satisfiabilité d'une formule 
Booléenne mise sous forme normale conjonctive a connu un intérêt 
croissant non seulement dans la communauté d'informatique théorique, 
mais aussi dans des domaines d'applications divers ou une solution 
pratique à ce problème permet des avancées significatives. Depuis les 
premiers développements de la procédure de base proposée par Davis, 
Putnam, Logemannet Loveland (DPLL), il y a plus d'une quarantaine 
d'années, ce domaine a connu un effort de recherche croissant ayant 
abouti aux solveurs SAT modernes d'aujourd'hui, capable de résoudre des 
instances de plusieurs centaines de milliers et même de millions de 
variables. Dans cet exposé, nous examinerons les idées principales ayant 
permis ce passage à l'échelle et nous évoquerons quelques applications 
de SAT.

*4- Génération avec CADP de scénarios pertinents pour tester les 
voitures autonomes**(Lina Marsso, Radu Mateescu**et Wendelin Serwe**- 
CONVECS, INRIA Grenoble et Laboratoire LIG)*
De nombreux industriels de l'automobile et de l'informatique travaillent 
activement au développement de voitures autonomes, depuis la simple 
assistance au pilotage jusqu'au pilotage entièrement automatique. Mais 
les véhicules autonomes évoluent dans des environnements complexes et 
doivent offrir des garanties de sûreté et de sécurité. Actuellement, la 
validation repose essentiellement sur la simulation et le test, avec des 
scénarios modélisant les interactions de la voiture autonome avec son 
environnement physique (obstacles, piétons, etc.).
La plupart du temps, ces scénarios sont produits à la main (ce qui est 
long et coûteux) ou générés de manière aléatoire (ce qui ne donne pas 
forcément de bonnes garanties de couverture). Dans cet exposé, nous 
présentons une approche qui permet de générer automatiquement, à partir 
d'un modèle formel en LNT et de la boite à outils de vérification CADP 
(http://cadp.inria.fr <http://cadp.inria.fr/>), des scénarios 
intéressants qui perturbentla trajectoire en cours du véhicule.


Bien cordialement

Mohamed Ghazel (IFSTTAR) & David Mentré (MERCE-CIS, Misubishi Electric)