Automatic Verification of Bossa Scheduler Properties

Abstract : Bossa is a development environment for operating-system process schedulers that provides numerous safety guarantees. In this paper, we show how to automate the checking of safety properties of a scheduling policy developed in this environment. We find that most of the relevant properties can be considered as invariant or refinement properties. In order to automate the related proof obligations, we use the WS1S logic for which a decision procedure is implemented by Mona. The proof techniques are implemented using the FMona tool.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.19-34, 2006
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00089493
Contributeur : Stephan Merz <>
Soumis le : vendredi 18 août 2006 - 19:27:09
Dernière modification le : mardi 16 janvier 2018 - 14:38:53
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:10:09

Fichier

Identifiants

  • HAL Id : inria-00089493, version 1

Citation

Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller. Automatic Verification of Bossa Scheduler Properties. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.19-34, 2006. 〈inria-00089493〉

Partager

Métriques

Consultations de la notice

362

Téléchargements de fichiers

99