Vérification automatique de propriétés d'ordonnanceurs Bossa

Résumé : Bossa est un environnement dédié au développement d’ordonnanceurs. Dans cet article, nous étudions l’automatisation de la vérification des propriétés énoncées par le langage dédié de Bossa. Nous montrons que la plupart de ces propriétés peuvent être vues commes des propriétés d’invariance ou de raffinement. Pour automatiser les obligations de preuve associées à ces notions, nous utilisons la logique WS1S et l’outil Mona qui implante une procédure de décision de cette logique. Les techniques de preuve utilisées sont exprimées à l’aide de l’outil FMona.