Waiting for locks: How long does it usually take?
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
Reliability of low-level operating-system (OS) code is an indispensable requirement. This includes functional properties from the safety-liveness spectrum, but also quantitative properties stating, e.g., that the average waiting time on locks is sufficiently small or that the energy requirement of a certain system call is below a given threshold with a high probability. This paper reports on our experiences made in a running project where the goal is to apply probabilistic model checking techniques and to align the results of the model checker with measurements to predict quantitative properties of low-level OS code.
Details
Original language | English |
---|---|
Title of host publication | Formal Methods for Industrial Critical Systems |
Editors | Mariëlle Stoelinga, Ralf Pinger |
Publisher | Springer, Berlin [u. a.] |
Pages | 47-62 |
Number of pages | 16 |
ISBN (print) | 978-3-642-32468-0 |
Publication status | Published - 2012 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 7437 |
---|---|
ISSN | 0302-9743 |
Workshop
Title | 17th International Workshop on Formal Methods for Industrial Critical Systems |
---|---|
Abbreviated title | FMICS 2012 |
Conference number | |
Duration | 27 - 28 August 2012 |
Degree of recognition | International event |
Location | |
City | Paris |
Country | France |
External IDs
Scopus | 84866674397 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236745 |
ORCID | /0000-0003-1724-2586/work/165453608 |
Keywords
Keywords
- Reliability of low-level operating-system (OS) code, prediction of quantitative properties of low-level OS code, probabilistic model checking techniques