AFSEC

Approches Formelles des Systèmes Embarqués Communicants

Workshop AFSEC lors des journées 2018 du GDR GPL

Wednesday 13 June 2018

Un Workshop AFSEC se tiendra le mecredi 13 juin (session 14h-15h30) lors des journées nationales du GDR GPL qui se dérouleront à Grenoble du 12 au 15 juin 2018.

Programme du Workshop AFSEC :

  • Julien Brunel (ONERA)
    Modelling the structure and the behaviour of systems.
  • Loïg Jezequel (Université de Nantes)
    Analyse paresseuse d’atteignabilité dans des réseaux d’automates temporisés..
  • Marc Pouzet (Ecole Normale Supérieure)
    Un peu d’ordre supérieur dans Zélus.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Session Outils AFSEC et SED (GDR MACS) lors de MSR 2017

Friday 1 December 2017

Jeudi 17 novembre 2017
Session “Outils” Lors du 11e Colloque sur la Modélisation des Systèmes Réactifs MSR 2017.
Le programme est disponible : ici

Organisée par le GT SED et le GT AFSEC

Publié dans Actions Afsec, Journées | Pas de commentaire »

Session “Outils” Lors de MSR 2017

Tuesday 29 August 2017

Session “Outils” Lors du 11e Colloque sur la Modélisation des Systèmes Réactifs (MSR 2017)

Lors du 11e Colloque sur la Modélisation des Systèmes Réactifs (MSR 2017), qui aura lieu à Marseille du 15 au 17 novembre 2017, les groupes AFSEC et SED organisent une session de démonstration de logiciels relatifs à la modélisation, l’analyse et la commande des systèmes réactifs et temps réel. Le but est de présenter à la communauté les outils logiciels que vous avez développés ou que vous utilisez dans le cadre de vos travaux de recherche.

Cette présentation se fera en deux temps :
- Une présentation rapide (5 minutes) en session plénière : genèse de l’outil, fonctionnalités, licences, copies d’écran…
- Un temps plus long de discussion autour des démonstrateurs, ou chacun pourra de manière informelle échanger avec les présentateurs et tester les outils qui les intéressent particulièrement.

Nous lançons donc un appel à propositions à tous ceux qui souhaitent présenter un outil qu’ils jugent intéressant. Le but n’est pas de vendre ou de gagner un prix mais de partager votre expérience ou votre travail. N’hésitez donc pas à proposer de présenter votre propre création, même si elle n’est qu’en version alpha, ou au contraire un outil mature que vous maitrisez.

Les personnes intéressées sont invitées à soumettre avant le 17 septembre 2017 un résumé d’une ou deux pages en suivant la procédure du site de MSR: http://www.lsis.org/msr2017/index.php?menu=sou

MSR: 15-17 novembre 2017
Lieu: Campus de St-Charles à Marseille.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Journée: “méthodes formelles pour la sécurité”. 21 juin 2017

Wednesday 5 April 2017

Journée AFSEC organisée par Pierre Bieber, Julien Brunel et Claire Pagetti.
Organisée avec le soutien du GDR GPL.
Organisation locale: Xiaoting Li, Sebti Mouelhi ECE

Quand: Le 21 juin 2017
Lieu: ECE Paris — Ecole d’ingénieurs
Campus Eiffel 1   10 rue Sextius Michel – 75015 Paris
Métro ligne 6 (stations Bir-hakeim ou Duplex), RER C (station Champ de Mars)

Du fait des restrictions budgétaires, l’action prendra en charge les pauses café et le repas de midi sera à la charge de chacun. L’inscription (gratuite) est nécessaire en envoyant un email à claire.pagetti@onera.fr ; objet : “Inscription AFSEC 21 juin” (cliquer sur le lien) - préciser : Nom et Affiliation.

Programme :

  • 9h15-9h30: accueil
  • 9h30-9h45: Mot d’accueil ECE
  • 9h45-11h0  La sécurite des systèmes embarqués : quelques cas d’études (Vincent Nicomette, LAAS)
    • Résumé: Les systèmes informatiques d’aujourd’hui ne sont plus des simples PC de bureau classiques. L’informatique est partout et elle est notamment de plus en plus embarquée, dans les moyens de transport par exemple mais aussi dans les objets connectés qui envahissent chaque jour d’avantage notre quotidien. Par ailleurs, l’utilisation massive du réseau Internet a facilité la propagation de logiciels malveillants, qui peuvent aujourd’hui cibler tous ces types d’équipements informatiques. Alors qu’il existe déjà des normes permettant d’évaluer la sécurité d’équipements informatiques “classiques”, leur application aux équipements embarqués est encore limitée. La présence et la criticité des vulnérabilités qui peuvent affecter ces équipements sont encore mal connues car pas suffisamment étudiées.
      Cet exposé présente des travaux de recherche qui ont été menés au LAAS depuis plusieurs années sur le thème de la sécurité des systèmes embarqués. Deux exemples seront présentés sur différents types d’équipements. La première étude
      présente une analyse de vulnérabilités d’un système embarqué critique avionique, réalisé dans la cadre d’une collaboration avec Airbus. La seconde étude concerne une analyse de vulnérabilités de systèmes embarqués dans deux types d’équipements connectés : les box ADSL et les téléviseurs connectés. Cette étude a été réalisée dans le cadre d’une collaboration avec Thalès. La présentation de ces cas d’études sera précédée d’une introduction générale à la sécurité informatique et aux propriétés associées.
    • Bio: Vincent Nicomette est professeur à l’INSA de Toulouse et chercheur dans l’équipe Tolérance aux Fautes et Sûreté de Fonctionnement Informatique du LAAS-CNRS. Il est diplômé de l’ENSEEIHT option Informatique
      en 1992, a obtenu son doctorat de l’TNP de Toulouse en 1996 et son HDR de l’INP de Toulouse en 2009. Ses principaux thèmes de recherche concernent la sécurité dans les systèmes répartis, la sécurité des systèmes d’exploitation et des systèmes embarqués.
  • 11h-12h Sécurité des applications : quels outils ? quelles techniques ? (Marie-Laure Potet, Verimag)
    • Résumé: L’analyse de code pour chercher des vulnérabilités ou évaluer leur robustesse vis-à-vis d’attaques pose des problèmes différents de la vérification ou la recherche de bugs pour la sûreté. Dans un premier temps nous illustrerons ceci à travers des exemples et montrerons les outils adaptés pour ces analyses. Un premier type d’analyse de vulnérabilités sera ensuite illustré par l’approche Gueb, développée dans le cadre du projet ANR BinSec, qui combine analyses statique et concolique pour la détection de use-after-free. Nous nous intéresserons ensuite à l’analyse de la robustesse de code contre l’injection de fautes. Nous présenterons FISCC, la première collection publique de code durci contre l’injection de fautes ainsi que des métriques d’évaluation de la robustesse à l’injection de fautes. Ces derniers travaux sont développés dans le cadre du projet DGA-ANR Sertif.
    • Bio: Marie-Laure Potet est Professeur à l’Ensimag, école de Grenoble INP, et chercheur au laboratoire Verimag. Elle a travaillé dans le domaine des méthodes formelles (approche correction par construction) pour la validation de systèmes sûrs et la certification Critères Communs. Depuis 8 ans elle anime une équipe à Vérimag sur l’analyse de code pour la sécurité et l’analyse de vulnérabilités à partir de modèles. Elle est impliquée dans de nombreux projets collaboratifs en sécurité.
  • 13h-14h Vérification automatique de propriétés d’équivalence (Vincent Cheval, LORIA)
    • Résumé: La conception et l’analyse des protocoles de sécurité sont connues pour être difficiles puisqu’elles demandent de considérer toutes les actions malicieuses d’un attaquant sur le protocole. Les modèles symboliques ont été utilisées avec succès pour prouver la sécurité de protocoles et pour découvrir de nouvelles failles de sécurité. Pourtant, prouver à la main la sécurité des protocoles cryptographiques est difficile et souvent source d’erreurs. C’est pourquoi une grande variété d’outils de vérification automatiques a été développée afin de prouver ou découvrir des attaques sur les protocoles. Je présenterai dans un premier temps un aperçu des outils existants puis je parlerai plus précisément des techniques de vérification automatique développées au sein de l’équipe PESTO pour vérifier différentes notions d’équivalence de processus. Ces notions étant particulièrement importantes pour exprimer de nombreuses propriétés de sécurité (ex: l’anonymat, la confidentialité du vote, la non-traçabilité).
    • Bio: Vincent Cheval est  chargé de recherche à Inria Nancy au sein du LORIA. Ses thèmes de recherche concernent l’analyse et la vérification de protocoles cryptographiques au sein de modèles formels, développement d’outils et la vérification de programmes.
  • 14h-15h Formal Methods and the Dark Side of the Force (Jean-Louis Lanet, Université de Rennes)
    • Résumé: Formal methods have been used in the industry for a long time with some noticeable successes. Unfortunately any technology can have a dual use, and in particular, attackers can use rigorous technologies for discovering weaknesses in a product or hidding a code inside another one.
    • Bio: Jean-Louis Lanet joined INRIA- Rennes Bretagne Atlantique in September 2014 to be involved into the High Security Labs (LHS) for a four years period. He has been Professor at the University of Limoges (2007-2014) at the Computer Science department, where he lead the team SSD (Smart Secure Device). He was also associate professor of the University of Sherbrooke and was in charge of the Security and Cryptology course of the USTH Master (Hanoi). His research interests included the security of small systems like smart cards, but also software engineering. Prior to that, he was senior researcher at Gemplus Research Labs (1996-2007) the smart card manufacturer. During this period he spent two years at INRIA (2003-2004) as an engineer at DirDRI (Direction des Relations Industrielles) and senior research associate in the Everest team at INRIA Sophia-Antipolis. He got my Habilitation à Diriger des Recherches (HdR) during the first INRIA period. He was researcher at the Advanced Studies Labs of Elecma, Electronic division of the Snecma, now part of the Safran group where he worked on hard real time techniques for jet engine control (1984-1995).
  • 15h15-16h15 Model Based Safety and Security Analyses of Avionics Systems (Pierre Bieber et Julien Brunel, ONERA)
    • Résumé: We aim at developing common models and tools to assess safety and security. In this talk we propose adaptations of models devised for safety assessment of avionics platforms in order to analyse their security. We describe  a security modelling and analysis approach based on the AltaRica and Alloy languages and their associated tools. The approach is illustrated by avionics case-studies. We report lessons learnt about the convergence and divergence points between security and safety with respect to modelling and analysis techniques.
    • Bio: Pierre Bieber et Julien Brunel sont ingénieurs de recherche à l’ONERA Toulouse, ils travaillent sur les méthodes d’analyse de la sécurité des systèmes aéronautiques.
  • 16h15-17h15 Opacité probabiliste (Béatrice Bérard, LIP6)
    • Résumé: L’opacité est un cadre générique qui permet de décrire formellement certaines propriétés de sécurité liées aux fuites d’information. Elle prend comme paramètres les exécutions d’un système, dont
      certaines sont considérées comme secrètes, et une fonction d’observation fournissant une vue partielle des exécutions à un agent extérieur qui connaît la structure du système. Le secret est opaque si pour toute exécution secrète, il en existe une non secrète avec la même observation. Après un bref panorama des résultats obtenus, je présenterai des extensions probabilistes de la notion d’opacité, avec pour but de mesurer la résistance d’un système aux fuites d’information et d’en comparer plusieurs réalisations. (travaux communs avec Serge Haddad, Olga Kouchnarenko, Engel Lefaucheux, John Mullins et Mathieu Sassolas).
    • Bio: Béatrice Bérard est professeur à l’Université P. et M. Curie et chercheur au LIP6, en délégation Inria au LSV pour 2016/2017. Ses thèmes de recherche concernent les questions d’expressivité et de vérification pour des modèles quantitatifs (temporisés ou probabilistes), avec des applications à la sécurité et aux systèmes de transport automatisés.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Journée “Parametric Analyses of Concurrent Systems” le 26 mai 2016

Tuesday 19 April 2016

Journée commune AFSEC/PACS (ANR PACS : Parametric Analyses of Concurrent Systems)

Pour définir la taille de la salle et prévoir les autorisations d’accès au bâtiment , une inscription (gratuite) au plus tard le 10 mai 2016 est nécessaire en envoyant un email à olivier-h.roux@irccyn.ec-nantes.fr ; objet : “Inscription AFSEC 26 mai” (cliquer sur le lien) - préciser : Nom et Affiliation.

Quand: Le 26 mai 2016
Lieu: Salle 1009, Bâtiment Sophie Germain, IRIF, Université Paris Diderot
M° 14 / RER C Bibliothèque François Mitterrand / Tramway T3a Porte de France.

Programme (en cours d’élaboration) :

  • 10h-11h Polynomial Interrupt Timed Automata (Serge Haddad, LSV - ENS Cachan)
    • Résumé: Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA). We prove that reachability is decidable in 2EXPTIME on PolITA, using an adaptation of the cylindrical decomposition method for the first-order theory of reals. Compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA.
      Joint work with B. Bérard (LIP6), C. Picaronny (LSV) , M. Safey El Din (LIP6) and M. Sassolas (LACL).
  • 11h-12h Symbolic Robustness Analysis of Timed Automata. (Ocan Sankur, IRISA - Rennes)
    • Résumé:
      We study the robust safety problem for timed automata under guard imprecisions which consists in computing a bound on the perturbations on delays under which a safety specification holds. We give a symbolic semi-algorithm for the problem based on a parametric data structure, and evaluate its performance in comparison with a recently published one, and with a binary search on enlargement values.
  • 14h-15h Reachability in Networks of Register Protocols under a Fair Stochastic Scheduler (Arnaud Sangnier, LIAFA - Paris 7)
    • Résumé: We study the almost-sure reachability problem in a distributed system
      obtained as the asyn- chronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property: the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.
      This is a joint work with Patricia Bouyer, Nicolas Markey, Mickael Randour and Daniel Stan.
  • 15h-16h Controlling Actions and Time in Parametric Timed Automata (Laure Petrucci, LIPN - Paris 13)
    • Résumé:
      Cyber-physical systems involve both discrete actions and real-time that elapses depending on timing constants.
      In this paper, we introduce a formalism for such systems containing both real-time parameters in linear timing constraints and switchable (Boolean) actions.
      We define a new approach for synthesizing combinations of parameter valuations and allowed actions, under which the system correctness is ensured when expressed in the form of a safety property.
      We apply our approach to a railway crossing system example with a malicious intruder potentially threatening the system safety.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Journée “solveurs SMT dans le contexte des systèmes embarqués critiques”. 29 Mars 2016

Tuesday 12 January 2016

Journée AFSEC organisée Par Claire Pagetti et Rémi Delmas
Organisée avec le soutien du GDR GPL.

Quand: Le 29 mars 2016
Lieu: Université Paris Diderot amphi Turing du bâtiment Sophie Germain map

Du fait des restrictions budgétaires, l’action prendra en charge les pauses café et le repas de midi sera à la charge de chacun. L’inscription (gratuite) au plus tard le 20 mars 2016 est nécessaire
en envoyant un email à claire.pagetti@onera.fr ; objet : “Inscription AFSEC 29 mars” (cliquer sur le lien) - préciser : Nom et Affiliation.

Programme :

  • 9h30-10h00: accueil
  • 10h00-11h15 Présentation de l’approche SMT (fondements mathématiques et logiques) et le standard SMT-lib (Pascal Fontaine, LORIA)
    • Résumé: Avant d’aborder les solveurs Satisfaisabilité Modulo Théories (SMT), nous considérerons brièvement le problème SAT de la satisfaisabilité en logique propositionnelle, et les techniques actuelles pour le résoudre, ces techniques étant elles aussi utilisées au coeur des les solveurs SMT.  Nous verrons ensuite l’architecture SMT, et comment elle s’articule autour d’un solveur SAT.  En particulier, nous verrons par l’exemple comment on peut élever l’expressivité d’un solveur SAT vers des langages plus riches, et comment, à partir de procédures de décision pour différents langages, on peut construire une procédure de décision sur la combinaison des langages.
      Enfin, nous présenterons quelques solveurs SMT disponibles, la communauté SMT et les différentes initiatives, notamment le standard SMT-lib qui définit un langage d’entrée accepté par la majorité des solveurs SMT.
  • 11h15-12h30 Implémentation d’un solveur SMT: le cas Alt-Ergo (Theory-comb, AC-comp, Quantificateurs, etc) (Mohamed Iguernlala, OCamlPro/LRI)
    • Résumé: Alt-Ergo est un démonstrateur SMT conçu pour le domaine de la vérification de programmes. Il est intégré dans plusieurs outils, en particulier via la plateforme Why3. Il est utilisé par Frama-C et Caveat pour démontrer la validité d’obligations de preuves (OPs) issues de code C, par SPARK pour prouver les OPs générées à partir de programmes Ada, ainsi que sur des OPs générées par Atelier-B. Il est aussi utilisé par EasyCrypt pour la vérification de protocoles de cryptographie et par Cubicle pour faire du model-checking.
      Le langage d’entrée d’Alt-Ergo est une logique du premier ordre avec types polymorphes et théories prédéfinies. Son coeur combine un SAT-solver inspiré de la méthode des tableaux, un moteur d’instantiation de formules quantifiées, et un ensemble de procédures de décision pour des théories telles que la théorie de l’égalité non-interprétée, l’arithmétique linéaire sur les entiers et les rationnels, les tableaux fonctionnels polymorphes, les types énumérés ainsi que la théorie AC des symboles associatifs et commutatifs. Cet exposé sera l’occasion de revenir sur quelques détails d’implémentation d’Alt-Ergo, et sur les particularités qui font sa force dans le domaine de la vérification de programmes.
  • 13h45-14h45 Vérification déductive de programmes (Claude Marché, LRI)
    • Résumé: Le principe de l’approche déductive de la vérification consiste, à partir d’un programme et d’une spécification formelle, à générer des “obligations de preuve”: des formules logiques dont la validité implique que le programme respecte sa spécification. Nous illustrons cette approche telle qu’elle est implantée dans l’environnement Why3, ainsi que dans les plateformes Frama-C et SPARK pour la vérification de codes critiques C et Ada. Les solveurs SMT sont utilisés de manière prépondérante pour la preuve automatique des obligations de preuve. Nous examinons les avantages et les inconvénients de ces solveurs dans ce contexte.
  • 14h45-15h45 Solveurs SAT application au model-checking (Loïg Jezequel, Université de Nantes)
    • Résumé: La planification est un domaine de l’intelligence artificielle ayant pour objectif de trouver des séquences d’actions (des plans) permettant d’atteindre, depuis l’état initial d’un système, un état objectif. Au début des années 90 une méthode de planification reposant sur l’utilisation de solveurs SAT a été proposée. Il s’agit de re-coder un problème de planification comme un ensemble (généralement infini) de problèmes SAT, puis de chercher à les résoudre l’un après l’autre dans un ordre bien choisi. Dès qu’une solution à l’un de ces problèmes SAT est trouvée, le problème de planification correspondant est résolu. Cette technique de planification s’est révélée surprenamment efficace, notamment en raison des efforts importants ayant été menés pour optimiser l’implantation des solveurs SAT.
      Dans cet exposé, nous présenterons une manière d’encoder les problèmes de planification comme des ensembles de problèmes SAT. Nous montrerons ensuite comment cette approche peut se généraliser pour calculer non plus un seul plan, mais des ensembles exhaustifs de plans, sous forme d’arbres d’exécution. Enfin, nous discuterons la possibilité d’étendre l’approche pour calculer des préfixes finis complets de dépliages de réseaux de Petri, comparables aux arbres d’exécution, mais plus compacts car prenant en compte la concurrence des réseaux de Petri.
  • 16h00-17h00 Synthèse d’un diagnostiqueur déterministe pour la prise de décision embarquée (Stéphanie Roussel, ONERA)
    • Résumé: Nous nous intéressons au problème de la synthèse d’un diagnostiqueur à base de modèle devant être intégré avec un algorithme de planification en vue d’une prise de décision embarquée. Les planificateurs que nous visons étant déterministes (pas de gestion de l’incertitude), le diagnostiqueur doit renvoyer à chaque étape un unique diagnostic. Nous utilisons alors une combinaison de systèmes de transition, logique temporelle et réseau de préférences conditionnelles booléennes (CP-Nets) pour spécifier le diagnostiqueur. Nous décrivons différentes réductions du  calcul d’un diagnostic vers le cadre de satisfaction booléenne et comparons des implémentations basées SAT et BDD sur un benchmark de type mission multi-robots soumis à différentes pannes.
  • 17h00-18h00 Synthèse d’architecture embarquées et vérification fonctionnelle de programmes synchrones basées SAT/SMT (Rémi Delmas, ONERA)
    • Résumé: Dans cet exposé nous présenterons un panorama des applications de SAT et SMT conduites au DTIM pour l’assistance à la conception et à la vérification de systèmes embarqués, allant de la vérification de propriétés de safety pour des programmes synchrones écrits en lustre avec l’outil STUFF, à la synthèse de plans de câblage de poids minimal pour la connexion de capteurs au réseau avionique avec le langage eLogical et sa traduction en logique pseudo-booléenne, en passant par l’allocation de niveaux de DAL et de budgets de taux de défaillance aux composants d’un système avionique à partir d’informations issues d’analyses de safety (coupes minimales) et du profil d’utilisation de l’avion, à l’aide de solveurs SAT, pseudo-booléens et de programmation MILP.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Session “logiciels pour la recherche” MSR 2015

Thursday 22 October 2015

Lors du 10e Colloque sur la Modélisation des Systèmes Réactifs (MSR 2015), qui aura lieu à Nancy du 18 au 20 novembre, les groupes SED (GDR MACS) et AFSEC organisent une session sur le thème des logiciels pour la recherche relatif à modélisation, l’analyse et la commande des systèmes réactifs et temps réel. Le but est de présenter à la communauté les logiciels que vous avez développés ou que vous utilisez dans le cadre de vos travaux de recherche.

Cette présentation se fera en deux temps :

  • Une présentation rapide (5 minutes) en session plénière : genèse de l’outil, fonctionnalités, licences, copies d’écran…
  • Un temps plus long de discussion autour des démonstrateurs, ou chacun pourra de manière informelle échanger avec les présentateurs et tester les outils qui les intéressent particulièrement

Nous lançons donc un appel à propositions à tous ceux qui souhaitent présenter un outil qu’ils jugent intéressant. Le but n’est pas de vendre ou de gagner un prix mais de partager votre expérience ou votre travail.
N’hésitez donc pas à proposer de présenter votre propre création, même si elle n’est qu’en version alpha, ou au contraire un outil mature que vous maîtrisez.

Nous espérons présenter entre 5 et 10 outils. Nous attendons vos propositions et dans un deuxième temps nous reviendrons vers celles
retenues pour préciser les moyens matériels et logiciels à mettre en oeuvre.

Les personnes intéressées sont invitées à se faire connaître (sans trop tarder) auprès de
- Laurent Piétrac, laurent.pietrac@insa-lyon.fr
- Sébastien Lahaye, sebastien.lahaye@univ-angers.fr
- ou Olivier H. Roux, olivier-h.roux@irccyn.ec-nantes.fr
en transmettant une brève description de leur outil logiciel.

Publié dans Actions Afsec, Conférences | Pas de commentaire »

Modélisation des Systèmes Réactifs (MSR 2015)

Wednesday 22 July 2015

10ème Colloque sur la Modélisation des Systèmes Réactifs (MSR 2015)

Inria Nancy ‐ Grand Est, France, du 18 au 20 novembre 2015

Site : MSR’15

Publié dans Actions Afsec, Conférences | Pas de commentaire »

Workshop AFSEC le 12 juin 2015 à Bordeaux

Monday 6 April 2015

Le Workshop AFSEC se tiendra le vendredi 12 juin (session 11h-12h30) lors des journées nationales du GDR GPL qui se dérouleront à Bordeaux du 10 au 12 juin 2015.

Programme du Workshop AFSEC :

  • Claire Pagetti (ONERA)
    Calcul d’ordonnancement hors­ligne sur plateformes multi/pluri­coeurs à base de méthodes formelles.
  • Maurice Comlan (Université d’Abomey Calavi (Bénin), Université de Nantes)
    Processus de branchement des réseaux de Petri avec reset arcs.
  • Marc Pouzet (Ecole Normale Supérieure, Paris.)
    SCADE Hybrid: une extension de SCADE avec des ODEs.

Publié dans Actions Afsec, Journées | Pas de commentaire »

journée “méthodes formelles et processus métier” le 16 octobre 2014 à Paris

Tuesday 1 July 2014

Une journée sur le thème “méthodes formelles et processus métier” (workflow, services Web, contrats QoS, …) se tiendra le 16 octobre 2014 à Paris (10h-17h15).
Organisée avec le soutien des GDR ASR et GPL.

Lieu : LIP6, Paris 6 (Jussieu) - salle 203-205 bâtiment 41 .

Le repas du midi sera offert mais une inscription (gratuite) au plus tard le 2 octobre 2014 est nécessaire
en envoyant un email à olivier-h.roux@irccyn.ec-nantes.fr ; objet : “Inscription AFSEC 16 octobre” (cliquer sur le lien) - préciser : Nom et Affiliation.

Programme :

  • 9h30-10h : Accueil (Café, viennoiseries)
  • 10h-12h30
    • Yoann LAURENT (LIP6) Alloy4SPV: a Formal Framework for Software Process Verification.
      In this work we present a framework for software process verification called Alloy4SPV which uses a subset of UML2 Activity Diagrams as a process modeling language. In order to achieve software process verification, we i) define a formal model of our process modeling language using first-order logic, ii) we give it a formal semantics based on the fUML standard, and iii) we implement this formalization using the Alloy language. In order to ease its adoption by process modelers, our framework comes with a graphical tool and a ready to use and customizable set of software process properties. We categorize these properties into two categories, syntactical and behavioral. We extend the set of behavioral properties we identified from the literature with two new categories that we defined, namely, organizational properties which relate to resource management and planning during process execution and business properties which are project/process specific properties.
    • Laurence DUCHIEN (LIFL) Une approche formelle pour la préservation de contrats de qualité de service lors de reconfiguration dynamique.
      L’omniprésence de services informatiques dans la vie quotidienne, combinée à la nature dynamique de leurs contextes d’exécution, constitue un défi majeur pour garantir la qualité attendue de ces services à l’exécution. Des contrats de Qualité de service (QoS) ont été proposés pour spécifier les niveaux de QoS attendus sur les différentes conditions de contexte, à l’aide de différents mécanismes. Dans cet exposé, nous présentons une définition des contrats de qualité de service en tant que politique de haut niveau pour régir le comportement des logiciels qui s’adaptent automatiquement à l’exécution, en réponse aux changements de contexte. Pour réaliser ce contrat, nous spécifions sa sémantique formelle et nous la mettons en œuvre dans un cadre logiciel capable d’exécuter et de reconfigurer des services, en vue de maintenir les contrats de qualité de service associés. Dans un premier temps, nous étendons les systèmes de transformation des graphes typés attribués et des machines à états finis, et nous les utilisons comme dénotations pour spécifier la sémantique des contrats de qualité de service. Deuxièmement, cette sémantique permet d’exploiter systématiquement des patrons de conception à l’exécution pour leur déploiement dynamique dans le logiciel. Troisièmement, notre sémantique garantit des propriétés d’auto-adaptation telles que la fiabilité et la robustesse dans la satisfaction de contrat. Enfin, nous évaluons l’applicabilité de notre mise en œuvre en l’intégrant et en l’exécutant dans Frascati, un middleware à base de composants multi-échelle, dans une étude de cas.
    • Nikolaos GEORGANTAS (INRIA) Service Choreographies: The Case for Interaction Paradigm Interoperability.
      With an increasing number of services and devices interacting in a decentralized manner, choreographies are an active area of investigation. The heterogeneous nature of interacting systems leads to choreographies that may not only include conventional services but also sensor-actuator networks, shared data spaces and event-based systems. Their middleware behavior within choreographies can be captured through abstract interaction paradigms, such as client-service, publish-subscribe and tuple space. This raises the essential issue of distributed system interoperability within heterogeneous choreographies. Open system integration paradigms, such as service oriented architecture (SOA) and enterprise service bus (ESB), have provided answers to the interoperability requirement. However, when it comes to integrating systems featuring heterogeneous interaction paradigms, existing solutions are typically ad hoc and partial, applying to specific interaction protocol technologies. In this talk, we introduce an interoperability solution based on abstraction and merging of the common high-level semantics of interaction paradigms, which is sufficiently general and extensible to accommodate many different protocol technologies. We apply this solution to revisit the SOA- and ESB-based integration of heterogeneous distributed systems.

  • 12h30-13h45 - Repas
  • 13h45-15h45
    • Kais KLAI (LIPN) Abstraction and Modular Verification of Inter-Enterprise Business Processes.
      Business process composition and cooperation are two important research fields in the business process domain. The questions, what properties of a process have to be public so that potential partners can collaborate with the process without risking to have an ill-designed composed process, and what is the minimal information necessary to be published, is a hot topic in the literature since many years. Also, one has to make sure that the composition of processes has the desired behaviour. The importance of dealing with such inter-enterprise business processes (IEBP for short) on one hand and business process composition on the other hand is reflected in the literature by numerous publications. In general, an IEBP can be considered as the cooperation of several local processes designed separately. The activities of each process are formally of two kinds: internal activities and cooperative activities (interface activities). IEBP are often too large for formal analysis, and the details of the components are hidden to the public so that no party knows the entire process definition. Therefore, we defend the idea that the analysis should be on the local business process and, if necessary, on an abstraction of the pertness models or of the IEBP.
      In this talk, we will present our contributions on abstraction and verification of IEBP. These contribution are mainly based on the Event-based Symbolic Observation Graph approach. Tow kinds of properties will be considered: generic properties (deadlock freeness, different variants of the soundness property) and specific properties (expressed by LTL logic).
    • Tarek MELLITI (IBISC) Formal Modelling and Evaluation of Service-based Business Process Elasticity in the Cloud.
      One of the expected features of Cloud environments is elasticity at different levels in order to guarantee provisioning of necessary resources that ensure a smooth functioning of cloud services despite changes in solicitations. Nevertheless, the provisioning of elastic infrastructures and/or platforms is not sufficient to provide users with elasticity at the level of Service-based Business Processes (SBPs). Therefore, there is a need to provide SBPs with mechanisms to scale their resource requirements up and down to ensure their adaptation to the workload changes. This can be achieved using mechanisms for duplicating and consolidating business services that compose the SBP. In this talk, we present a formal unified model (Timed Petri-nets) for SBPs elasticity. We show that our model preserves the semantics of SBPs when services are duplicated or consolidated. Based on this model, we propose a framework that defines and evaluates (by Simulation and Verification) elasticity strategies (defined as colored Petri nets). Our elasticity strategies could be a formal start to Services Level Agreement languages. The complete approach is experimented in a real Cloud environment.

  • 15h45-16h15 - Café, discussions
  • 16h15-17h
    • Pascal POIZAT (LIP6) Développement Formel de Processus Métier Chorégraphiques
      Les processus métier collaboratifs peuvent être vus selon deux perspectives complémentaires.
      Dans la première il s’agit d’inter-connecter les modèles des pairs participant à la collaboration.
      C’est une approche qui convient bien à un développement « bottom-up », par réutilisation et assemblage de pairs.
      Dans la seconde, les interactions entre pairs sont des entités de premier ordre, et il est possible de décrire les processus métiers collaboratifs d’un point de vue global, aussi appelé chorégraphique.
      Cela convient bien à un développement « top-down », par spécification et génération d’obligations locales (ou squelettes de pairs).
      Deux problèmes importants lors de la conception de processus métiers chorégraphiques (BPC) sont d’un côté la conformité entre une spécification et un ensemble de modèles de pairs
      et d’un autre côté la réalisabilité d’une spécification, c’est-à-dire la possibilité d’obtenir des modèles conformes de pairs à partir de la spécification.
      Ces problèmes ont été étudiés principalement pour des modèles interconnectés et plus récemment des modèles d’interactions.
      Par ailleurs, la prise en compte des données échangées entre les partenaires d’un processus métier collaboratif nécessite habituellement une sur-approximation ou un bornage du domaine des données.
      Dans cet exposé je présenterai des résultats récents quant à la vérification de BPC décrits dans le standard BPMN 2.0 ainsi qu’une approche symbolique basée sur l’utilisation d’un solveur SMT pour la prise en compte des données dans cette vérification.

Publié dans Actions Afsec, Journées | Pas de commentaire »