Automatic Verification of Bossa Scheduler PropertiesReport as inadecuate

Automatic Verification of Bossa Scheduler Properties - Download this document for free, or read online. Document in PDF available to download.

1 IRIT - Institut de recherche en informatique de Toulouse 2 DIKU - Department of computer Science Copenhagen 3 OBASCO - Objects, aspects and components Mines Nantes - Mines Nantes, Inria Rennes – Bretagne Atlantique

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.

keyword : scheduling refinement model-checking WS1S

Author: Jean-Paul Bodeveix - Mamoun Filali - Julia Lawall - Gilles Muller -



Related documents