AFSEC

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

Programme du workshop AFSEC :

• 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”

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.

Thomas Ferrandiz a soutenu sa thèse intitulée “Maîtrise des latences de communication dans les réseaux bord SpaceWire” le 2 mars. Le jury était composé de

• M. Thierry Divoux, rapporteur,
• M. Christian Fraboul, directeur de thèse,
  
• M. Fabrice Frances,
  
• M. David Jameux,
  
• M. Jean-Jacques Lesage, rapporteur,
  
• M. Gilles Moury,
  
• M. Xavier Olive

Vous pouvez retrouvez les transparents.

Journée WEED du mercredi 23 novembre 2011 (10h30-16h30) a eu lieu à l’ICT Lab — 23 avenue d’Italie, 75013 Paris. Elle a réuni 13 participants.
Programme:

• 10h30-11h15: Deterministic performance guarantee: Worst case end-to-end delay analysis. (Sara Medlej, Steven Martin)
• 11h15-12h: An efficient and simple class of function to model arrival curve of
  packetised flows (Marc Boyer)
• 13h45-14h30: Non-preemptive static priority with network calculus (William Mangoua Sofack)
• 14h30-15h15:Modèles et calculs garantis pour les systèmes (min,+)-linéaires (Euriel Le corronc)
• 15h15-16h: Composition of service curves in Network Calculus (Anne Bouillard)
• 16h-16h30: Avenir de groupe, prochaines actions, etc.

Participation gratuite mais réservation obligatoire (Marc.Boyer  —- onera.fr) .

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 :

• Grégory Batt Robustness Analysis and Tuning of Synthetic Gene Networks
• Thao Dang Applying the Hybridization Approach to Biological Models
• Loïc Paulevé Modelling, Simulation and Verification of Large Biological Regulatory Networks
• Gilles Bernot An extension of Hoare logic to identify the parameters of a gene regulatory network

Colloque Francophone sur la Modélisation des Systèmes Réactifs
Soutenu par l’AFSEC.

Ecole Centrale de Lille, du 16 au 18 novembre 2011

Les inscriptions sont ouvertes.
“Early registration” : 30 septembre 2011

Site : MSR’11

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

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 :

• Marc Pouzet Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language
• Sandie Balaguer Building Tight Occurrence Nets from Reveals Relations
• Euriell Le Corronc Flow Control with (Min,+) Algebra

Les actes des journées GPL sont disponibles : ACTES

Workshop AFSEC (lors des journées du GDR GPL ) le 9 juin 2011 à Lille Polytech, Campus universitaire de Lille 1

Programme des journées du GDR GPL : 8-10 juin 2011

Programme du workshop AFSEC :

• Albert Benveniste, Timothy Bourke, Benoît Caillaud, and Marc Pouzet (INRIA, Rennes. & Ecole Normale Supérieure, Paris.)
  “Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language”
• Sandie Balaguer, Thomas Chatain, Stefan Haar (INRIA & LSV (CNRS & ENS Cachan) )
  “Building Tight Occurrence Nets from Reveals Relations”
• Euriell Le Corronc, Bertrand Cottenceau et Laurent Hardouin (LISA, Université d’Angers)
  “Flow Control with (Min,+) Algebra”

Comme chaque année, l’action AFSEC est invitée à organiser une session lors des journées du GDR GPL qui se dérouleront à Lille, du 8-10 juin 2011.

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.