Automatic Verification of Bossa Scheduler Properties | Zendy

Jean-Paul Bodeveix | Zendy; Mamoun Filali | Zendy; Julia Lawall | Zendy; Gilles Muller | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Automatic Verification of Bossa Scheduler Properties

Author(s) -

Jean-Paul Bodeveix,

Mamoun Filali,

Julia Lawall,

Gilles Muller

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2007.05.026

Subject(s) - computer science , scheduling (production processes) , invariant (physics) , model checking , proof of concept , process (computing) , distributed computing , programming language , operating system , engineering , physics , mathematical physics , operations management

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research