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

Jean-Paul Bodeveix (1, 2) , M Filali (1, 3) , Julia L. Lawall (4) , Gilles Muller (5, 6)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 UT3 - Université Toulouse III - Paul Sabatier
3 CNRS - Centre National de la Recherche Scientifique
4 DIKU - Department of Computer Science [Copenhagen]
5 LINA - Laboratoire d'Informatique de Nantes Atlantique
6 OBASCO - Objects, aspects and components

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.

Domaines: Langage de programmation [cs.PL]

Jean-Paul Bodeveix, M Filali, Julia L. Lawall, Gilles Muller. Vérification automatique de propriétés d'ordonnanceurs Bossa. AFADL 2006 - Conférence Francophone sur les Approches formelles pour le développement de logiciels, Groupe sur les Approches Formelles dans l'Assistance au Développement de Logiciels, Jan 2006, Paris, France. pp.95-109. ⟨hal-00457181⟩