Automatic Verification of Bossa Scheduler Properties

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.

Data and Resources

Additional Info

Field Value
Source Electronic Notes in Theoretical Computer Science - Special issue: Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006)
Author Bodeveix, Jean-Paul, Filali, M, Lawall, Julia, L., Muller, Gilles
Maintainer CCSD
Last Updated May 8, 2026, 14:20 (UTC)
Created May 8, 2026, 14:20 (UTC)
Identifier inria-00089493
Language en
Rights https://creativecommons.org/licenses/by/4.0/
contributor Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE) ; Institut de recherche en informatique de Toulouse (IRIT) ; Université Toulouse Capitole (UT Capitole) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse - Jean Jaurès (UT2J) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse III - Paul Sabatier (UT3) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Toulouse Mind & Brain Institut (TMBI) ; Université Toulouse - Jean Jaurès (UT2J) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse III - Paul Sabatier (UT3) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse III - Paul Sabatier (UT3) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse Capitole (UT Capitole) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse - Jean Jaurès (UT2J) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse III - Paul Sabatier (UT3) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Toulouse Mind & Brain Institut (TMBI) ; Université Toulouse - Jean Jaurès (UT2J) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse III - Paul Sabatier (UT3) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)-Université Toulouse III - Paul Sabatier (UT3) ; Communauté d'universités et établissements de Toulouse (Comue de Toulouse)
coverage Nancy, France
creator Bodeveix, Jean-Paul
date 2006-09-08T00:00:00
harvest_object_id 29d4d735-0dc2-4093-9733-d346b8adee5d
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-10-22T00:00:00
relation info:eu-repo/semantics/altIdentifier/doi/10.1016/j.entcs.2007.05.026
set_spec type:COMM