HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Friday, August 18, 2006 - 7:27:09 PM
Last modification on : Friday, February 4, 2022 - 3:19:27 AM
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