AFSEC

Approches Formelles des Systèmes Embarqués Communicants

Archive pour la catégorie 'Journées'

Workshop AFSEC le 04 avril 2013 à Nancy

Monday 11 February 2013

Workshop AFSEC le 04 avril 2013 à Nancy
lors des journées du GDR GPL du 2 au 5 avril 2013 à Nancy colocalisées avec CIEL et AFADL.

Pdf du programme avec resumés

Programme :

  • Benoît Barbot (LSV, ENS Cachan), Marco Beccuti (Univ. Torino), G. Franceschinis (Univ. Piemonte Orientale) et Serge Haddad (LSV, ENS Cachan)
    “Partially Observed Markov Decision Process, for Energy Management in Wireless Sensor Networks”
  • Frédéric Boniol et Virginie Wiels (ONERA Toulouse)
    “Ingénierie formelle pour logiciels aéronautiques certifiés.”
  • Sylvain Cotard, Sebastion Faucou et Jean-Luc Bechennec, (Renault & IRCCyN Nantes)
    “Runtime Verification for Real-Time Automotive Embedded Software”
  • Iulia Dragomir, Iulian Ober, Christian Percebois (IRIT TOULOUSE)
    “Contrats pour composants réactifs temporisés”

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

Workshop AFSEC 2013 lors des journées GPL - Appel à communication

Friday 1 February 2013

Comme chaque année, l’action AFSEC est invitée à organiser un workshop lors des journées nationales du GDR GPL qui se dérouleront du 2 au 5 avril 2013 à Nancy.
Ces journées seront colocalisées avec CIEL et AFADL.

Le workshop AFSEC se tiendra le jeudi 4 avril

Si vous souhaitez faire un exposé de vos travaux dans le cadre de la session AFSEC de ces journées, merci de faire parvenir par email (à Olivier H Roux) un titre et un résumé de votre présentation.

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

Journée “Robustesse dans les systèmes concurrents” le 19 octobre 2012

Tuesday 16 October 2012

4 exposés “Time constrained MSC Graph”, “la Robustesse dans les timed Petri nets”, “Une sémantique (séquentielle) alternative pour les TPN”, les “Dépendances logiques entre les événements dans les dépliages de réseaux de Petri temporels”
Discussions

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

Compte rendu du Workshop AFSEC du 22 juin 2012

Friday 29 June 2012

Workshop AFSEC (lors des des journées du GDR GPL ) le 22 juin 2012 à Rennes - INRIA Campus Beaulieu

50 participants

Une partie des transparents est disponible :

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

Workshop AFSEC - 22 juin à Rennes

Wednesday 2 May 2012

Workshop AFSEC (lors des des journées du GDR GPL ) le 22 juin 2012 à Rennes - INRIA Campus Beaulieu

Plénier 9h-10h :

  • Claude Jard (ENS Cachan, Antenne de Bretagne - Inria / IRISA)
    QoS-Aware Management of Monotonic Service Orchestrations

Session 10h30-12h30 :

  • Loic Helouet (IRISA)
    “Synthèse de protocoles à partir d’exigences - Garanties de correction par controle asynchrone”
  • Marc Pouzet (Ecole Normale Supérieure, Paris.)
    “Une extension de Lustre avec du temps continu”
  • Thomas Chatain, (LSV - ENS Cachan)
    “Avoiding shared clocks in networks of timed automata”
  • Fabrice Kordon (LIP6 - Paris 6)
    “Exploitation de la Hiérarchie et des Symétries dans les systèmes répartis”

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

Journée “Implementability and Robustness of Timed Systems” le 29 mars 2012

Monday 2 April 2012

Journée “Implementability and Robustness of Timed Systems” de l’ANR Impro

Programme:

  • 10h30 — 11h15 Ocan Sankur, “Shrinking Timed Automata”
  • 11h15 — 12h15 Mathieu Sassolas, “Opacité probabiliste”
  • 13h45 — 14h30 Sandie Balaguer “Transformation de TPN en NTA qui préserve la distribution”
  • 14h30 — 15h00 Arnaud Sangier, “Verification of Probabilistic Timed Automata”
  • 15h00 — 15h30 Loïc Helouët ‘Robustesse dans les Timed-constrained MSCs”
  • 15h30 — 16h15 Rémi Jaubert “Robsutesse dans les TA”

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

Workshop AFSEC lors des journées GPL - Appel à communication

Saturday 17 March 2012

Comme chaque année, l’action AFSEC est invitée à organiser une session lors des journées nationales du GDR GPL qui se dérouleront du 18 au 22 juin 2012 à Rennes.

Si vous souhaitez faire un exposé de vos travaux dans le cadre de la session AFSEC de ces journées, merci de faire parvenir par email (à Olivier H Roux) un titre et un résumé de votre présentation.

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

Compte-rendu de la journée “Méthodes formelles pour la bio-informatique”

Friday 4 November 2011

Journée “Méthodes formelles pour la bio-informatique” du jeudi 20 octobre 2011 au LIP6 à Paris.

25 participants.

Nous remercions particulièrement Béatrice Bérard et Fabrice Kordon pour l’organisation locale.

Les transparents des quatre présentations sont disponibles :

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

Journée “Méthodes formelles pour la bio-informatique”

Friday 1 July 2011

Journée AFSEC “Méthodes formelles pour la bio-informatique” le jeudi 20 octobre 2011 à Paris (Jussieu - la salle Laurière (25-26/101)).

La participation est gratuite mais afin d’envisager une salle plus grande, nous vous demandons de vous inscrire sur le site suivant : INSCRIPTION

Programme :

    9h30-10h45:

  • Gregory Batt (INRIA Paris-Rocquencourt, France) - Joint work with Boyan Yordanov, Calin Belta and Ron Weiss :


    Robustness analysis and tuning of synthetic gene networks

    Motivation: The goal of synthetic biology is to design and construct biological systems that present a desired behavior. The construction of synthetic gene networks implementing simple functions has demonstrated the feasibility of this approach. However, the design of these networks is difficult, notably because existing techniques and tools are not adapted to deal with uncertainties on molecular concentrations and parameter values.

    Results: We propose an approach for the analysis of a class of uncertain piecewise-multiaffine differential equation models. This modeling framework is well adapted to the experimental data currently available. Moreover, these models present interesting mathematical properties that allow the development of efficient algorithms for solving robustness analyses and tuning problems. These algorithms are implemented in the tool RoVerGeNe, and their practical applicability and biological relevance are demonstrated on the analysis of the tuning of a synthetic transcriptional cascade built in Escherichia coli.



  • 11h15-12h30

  • Thao Dang (VERIMAG Lab, Grenoble, France) :


    Applying the Hybridization Approach to Biological Models

    In this presentation, we describe the hybridization approach for the verification of non-linear ODEs and how it can be applied to the analysis of biological models. The main idea of the hybridization approach is to approximate non-linear dynamics with a dynamics which is linear in each approximation domain. A challenging problem is to define approximation domains and associated approximate linear dynamics in order to guarantee accuracy and computational efficiency requirements. Recent results on this approach are then presented, and our experiences in the analysis of some biological models using this approach are also reported.



  • 13h45-15h00

  • Loïc Paulevé (IRCCyN, Nantes, France) :


    Modelling, Simulation and Verification of Large Biological Regulatory Networks.

    Biological regulatory networks (BRNs) describe regulations, positive or negative, between biological components (genes, proteins, etc.). They are commonly used to study protein production dynamics within cells. Because of their highly combinatorial dynamics, the formal analysis of very large BRNs is a challenging task.

    First, we introduce our formalism named the Process Hitting, and its application to the modelling of BRNs with discrete values. With the aim at simulating and analysing quantitative properties, and as a mean to provide a trade-off between stochastic and timed specifications, we show a generic method to tune temporal properties within stochastic semantics of Process Hitting. Besides its clear biological modelling orientation, we claim that the Process Hitting can be applied to less specific dynamical complex systems.

    Finally, we address the large scale analysis of Process Hitting by providing a static analysis by abstract interpretation. Our static analysis brings very efficient over- and under-approximations of reachability properties. The scalability of our approach is illustrated by its application to the decision of reachability of gene expression levels within BRNs of 94 and 104 components. Our implementation responds very fast to the decision, while a well established symbolic model checking techniques regularly fails because of the state space explosion.



  • 15h30-16h45

  • Gilles Bernot (I3S, Nice - Sophia Antipolis, France) :


    Une extension de la logique de Hoare pour l’identification de paramètres dans les réseaux génétiques

    L’obstacle majeur rencontré lorsqu’on veut modéliser des réseaux biologiques est l’identification des nombreux paramètres qui définissent la dynamique du système. La logique temporelle est devenue une des principales méthodes formelles appliquées à cette question depuis les travaux fondateurs autour de BIOCHAM et de SMBioNet. Ici, on propose une nouvelle méthode formelle, plus orientée vers l’exploitation directe des traces observées biologiquement.
    Dans le cadre des réseaux génétiques, une extension de la logique de Hoare et du calcul de la plus petite précondition fournit un ensemble de contraintes sur les paramètres qui sont nécessaires et suffisantes pour que cette trace existe dans le modèle mathématique discret.
    Cette approche pourrait aisément être généralisée à une large classe de modèles discrets de systèmes complexes.



  • 16h45-17h15: discussion et clôture

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

Compte rendu du workshop AFSEC lors des journées GPL

Tuesday 14 June 2011

Workshop AFSEC lors des journées GPL le 9 juin 2011 à Lille Polytech.
25 participants.

Les transparents des présentations du workshop AFSEC sont disponibles :

Les actes des journées GPL sont disponibles : ACTES

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