Return to search

Waiting for Locks: How Long Does It Usually Take?

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.

Identiferoai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:27128
Date January 2012
CreatorsBaier, Christel, Daum, Marcus, Engel, Benjamin, Härtig, Hermann, Klein, Joachim, Klüppelholz, Sascha, Märcker, Steffen, Tews, Hendrik, Völp, Marcus
PublisherTechnische Universität Dresden
Source SetsHochschulschriftenserver (HSSS) der SLUB Dresden
LanguageEnglish
Detected LanguageEnglish
Typedoc-type:conferenceObject, info:eu-repo/semantics/conferenceObject, doc-type:Text
SourceFormal Methods for Industrial Critical Systems: 17th International Workshop on Formal methods for industrial critical systems, Paris, France, August 27-28, 2012, Proceedings, S. 47-62, ISBN: 978-3-642-32469-7, ISSN: 0302-9743
Rightsinfo:eu-repo/semantics/openAccess
Relation10.1007/978-3-642-32469-7_4

Page generated in 0.002 seconds