Skip to Main content Skip to Navigation
Conference papers

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

Cited literature [21 references]  Display  Hide  Download
Contributor : Stephan Merz <>
Submitted on : Friday, August 18, 2006 - 7:27:09 PM
Last modification on : Thursday, March 18, 2021 - 2:34:41 PM
Long-term archiving on: : Monday, April 5, 2010 - 11:10:09 PM


  • HAL Id : inria-00089493, version 1


Jean-Paul Bodeveix, M Filali, Julia Lawall, Gilles Muller. Automatic Verification of Bossa Scheduler Properties. Automatic Verification of Critical Systems, Sep 2006, Nancy, France. pp.19-34. ⟨inria-00089493⟩



Record views


Files downloads