Modélisation des systèmes réactifs (Actes du colloque de MSR 2007)

La synergie des disciplines de l'automatique et de l'informatique se révèle dans notre actualité d'autant plus prépondérante et justifiée qu'émergent des systèmes pour lesquels les couches physiques et logicielles sont de plus en plus imbriquées, entraînant une complexité de mise en oeuvre et de validation croissante. Les contraintes de performance, de dimensionnement et de criticité liées aux usages, aux normes et au développement durable posent de nouvelles problématiques qui ne peuvent plus être résolues localement. Pour relever ces nouveaux défis, les méthodes et les outils de la conception et de l'analyse de tels systèmes sont à définir selon des approches croisées de l'automatique et de l'informatique. La 6e édition du colloque francophone Modélisation des Systèmes Réactifs, « MSR », se place résolument dans ce contexte.

Avant-propos. Conférence invitée 1. Construction de systèmes à base de composants en BIP. Session 1. Vérification formelle 1. Test de vacuité pour automates de Büchi ensemblistes avec tests d'inclusion. Une approche efficace pour le traitement des données dans RT-LOTOS. Session 2. Synthèse de contrôleurs. Conditions structurelles dans le contrôle modulaire de SED concurrents. Synthèse optimale de contrôleurs discrets et systèmes répartis tolérants aux fautes. Validation de commande des systèmes à événements discrets. Session 3. Diagnostic. Construction de moniteurs pour la surveillance de propriétés de sécurité. Démarche globale de diagnostic décentralisé des SED. Application à un système de transfert de pièces. Conférence invitée 2. Systèmes embarqués et compilation. Session 4. Applicatifs. Modèle multi-agent pour le pilotage temps réel d'un voilier. Systèmes réactifs pour modéliser la décision en production agricole. Exemples à propos des traitements phytosanitaires. Application de la commande par platitude pour le contrôle de trafic Internet. Session 5. Vérification formelle 2. Vérification paramétrée de la cohérence des processus workflow. Spécification et vérification des propriétés de vivacité en B événementiel. Session 6. Multiparadigme. Sur certains liens entre comparaison stochastique et traitement du signal. Stabilité des systèmes à commutation caractérisés par un réseau de Petri temporel. Conférence invitée 3. Diagnostic des systèmes à événements discrets. Session 7. Approche temporelle des RdP. Réseaux de Petri à chronomètres post et pré-initialisés. Réseaux de Petri à arcs temporels généralisés aux sémantiques faible et forte. Synthèse de contraintes de conception à partir de réseaux de Petri temporels paramétrés. Index des auteurs.