David MENTRÉ
2018-11-08 20:17:52 UTC
[ 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)
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)