 |
 |
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.
Cited literature [21 references]
https://hal.inria.fr/inria-00089493
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
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