Abstract FR:

On présente un formalisme de représentation graphique pour les systèmes parallèles et communicants, par signaux de synchronisation. Ces descriptions sont ensuite reliées au formalisme algébrique des calculs de processus, qui procure un cadre formel pour en étudier la sémantique et en vérifier les propriétés. On décrit l'outil de visualisation AUTOGRAPH, basé sur ces concepts. AUTOGRAPH contient un éditeur graphique multifenêtres, un interprète/traducteur des dessins vers leurs formes algébriques textuelles, ainsi que des fonctionnalités de retour vers les descriptions graphiques. La phase d'interprétation contient trois types d'analyse sur les dessins : étude de leur cohérence ; expansion de conventions graphiques ; complétion de leurs éléments facultatifs. Ces phases ultérieures permettent de garantir à l'utilisateur des conditions d’édition souples et économiques au niveau graphique, en conservant la précision des significations. AUTOGRAPH est interfacé avec plusieurs systèmes de vérification, et principalement avec AUTO, qui s'adapte aux principes de visualisation d'AUTOGRAPH. Des exemples typiques d'utilisation d'AUTOGRAPH dans des sessions de développement et de vérification sont présentés et commentes. Ces exemples incluent des expériences de traitement de programmes ESTEREL, pour lesquels AUTOGRAPH permet une analyse des automates après compilation