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.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:27128 |
| Date | January 2012 |
| Creators | Baier, Christel, Daum, Marcus, Engel, Benjamin, Härtig, Hermann, Klein, Joachim, Klüppelholz, Sascha, Märcker, Steffen, Tews, Hendrik, Völp, Marcus |
| Publisher | Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | doc-type:conferenceObject, info:eu-repo/semantics/conferenceObject, doc-type:Text |
| Source | Formal 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 |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | 10.1007/978-3-642-32469-7_4 |
Page generated in 0.0457 seconds