Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-00457181
Contributor : LS2N Hal Connect in order to contact the contributor
Submitted on : Friday, June 24, 2022 - 2:10:54 PM
Last modification on : Friday, August 5, 2022 - 12:31:19 PM

File

Vérification automatique de p...
Publisher files allowed on an open archive

Identifiers

  • HAL Id : hal-00457181, version 1

Citation

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⟩

Share

Metrics

Record views

174

Files downloads

3