AFSEC

Approches Formelles des Systèmes Embarqués Communicants

Archive pour October, 2008

Informations sur les appels ANR 2009

Thursday 30 October 2008

L’ANR vient de mettre à disposition sur son site un document qui décrit, en quelques pages par type d’appel, les objectifs 2009 des appels à projets qui seront diffusés sur la programmation 2009.

Télécharger le document

Publié dans Appels à projets | Pas de commentaire »

Compte rendu de la réunion du 23 octobre 2008

Sunday 26 October 2008

Réunion du 23 octobre 2008 sur les “Structures de données pour l’analyse des Réseaux de Petri?

Exposé le matin et table ronde l’après midi pour des travaux communs LIP6/IRCCyN/IRISA.

Transparents des présentations :

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

PETRI NETS 2009 (24 au 26 juin 2009)

Saturday 25 October 2008

International Conference on Application and Theory of Petri Nets and other Models of Concurrency
Collocated with RAPID SYSTEM PROTOTYPING 2009 (RSP’09)

PETRI NETS 2009

June 22-26, 2009
Paris, France

. Submission of Papers : January 5, 2009
. Notification : March 1, 2009
. Final Version Due : April 1, 2009
. Workshops & Tutorials : June 22-23, 2009
. Conference : June 24-26, 2009

Email : petrinet2009@lip6.fr

Publié dans Manifestations, Conférences | Pas de commentaire »

Journée “Structures de données pour l’analyse des RdP”

Tuesday 14 October 2008

Séminaire sur les “Structures de données pour l’analyse des Réseaux de Petri”
le 23 octobre 2008 à l’ IRCCyN (Nantes) en salle 018 : plan

Programme:
• 9h:00-10:30 — Yann Thierry Mieg (LIP6) : Hierarchical Set Decision Diagrams & Applications
• 10:30-10:45 — pause
• 10:45-12:15 — Morgan Magnin (IRCCyN - MOVES) : A la recherche de méthodes efficaces pour la vérification de réseaux de Petri à chronomètres en temps discret

Une discussion aura lieu l’après midi pour établir les connexions possibles entre les 2 méthodes exposées.

Résumés des exposés :

Exposé de Yann Thierry Mieg : Hierarchical Set Decision Diagrams & Applications

Les SDD sont une structure de données qui partage les grandes caractéristiques des diagrammes de décision binaires (BDD) : unicité de représentation des noeuds, utilisation de cache(s), forme canonique, représentation symbolique très compacte d’un ensemble.
Leur originalité vient de
1. Les arcs sont étiquetés par un ensemble, plutot que par une seule valeur (un booléen en BDD). Comme un ensemble est représenté de façon compacte par un SDD, la structure peut être hiérarchique.
2. Les opérations sont spécifiées à l’aide d’homomorphismes inductifs, une façon élégante
et flexible de coder des opérations spécifiques à une application.
3. La gestion de structures de taille variable (piles, files, listes…) est possible

Enfin, l’implantation transparente d’algorithmes dit de “saturation” permet d’obtenir d’excellentes performances dans le cadre du calcul de point fixe sur un ensemble d’évenements.
Cet exposé présentera la structure de données et comment l’utiliser pour le model-checking à travers des exemples.

———————————————————————————————————
Exposé de Morgan Magnin : À la recherche de méthodes efficaces pour la vérification de réseaux de Petri à chronomètres en temps discret

Les réseaux de Petri temporels (RdPT) permettent de modéliser la durée de différentes actions sous la forme d’un intervalle de temps. Ils peuvent par ailleurs être enrichis afin de représenter des tâches susceptibles d’être suspendues puis relancées (réseaux de Petri à chronomètres notés SwPN).
Nous nous proposons de comparer les deux approches que sont le temps dense et le temps discret pour ces modèles. Notre étude commence par un approfondissement des liens entre réseaux de Petri, RdPT et SwPN en fonction de leur sémantique en temps dense et en temps discret. Nous introduisons ensuite une méthode efficace de calcul énumératif de l’espace d’états de modèles en temps discret : nous proposons notamment de traduire un réseau de Petri temporel borné en réseau de Petri non-temporisé (en préservant la bisimulation). Il devient dès lors possible de vérifier des propriétés temporelles sur un réseau de Petri temporel en raisonnant sur le réseau non-temporisé sous-jacent. L’outil que nous avons choisi d’utiliser pour obtenir l’espace d’états des réseaux non temporisés est Markg. Celui-ci repose sur des structures de données inspirées par les Diagrammes de Décision Binaires dont l’efficacité n’est plus à prouver. Les structures de données développées par Pierre Molinaro spécialement pour l’analyse des réseaux de Petri sont les suivantes :
- les Vector Decision Diagrams (VDD) sont dédiés au stockage des états ;
- les Arithmetic Expression Decision Diagrams (AEDD) modélisent les fonctions d’incidence amont et aval.
Nous avons également effectué des recherches dans une autre voie : plutôt que de traduire le réseau à chronomètres en réseau de Petri non temporisé, nous avons cherché à le transformer en automate à compteurs bisimilaire. Cette procédure nous permet alors de recourir à des outils qui ont fait leurs preuves sur ces modèles à l’instar de FAST et de Lever. Toutefois, quels que soient le modèle de sortie et l’outil utilisés, nous avons été confrontés à l’explosion combinatoire du nombre des états dès que l’intervalle de tir associé à une transition est important (supérieur à une centaine d’unités de temps). Cela rend difficile la vérification de certains modèles en temps discret, nous incitant ainsi à élaborer une méthode non plus énumérative mais symbolique de calcul de l’espace d’états des réseaux en temps discret.

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