Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code

Christel BaierChristel Baier, Marcus DaumMarcus Daum, Benjamin EngelBenjamin Engel, Hermann HärtigHermann Härtig, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, Steffen MärckerSteffen Märcker, Hendrik TewsHendrik Tews, Marcus VölpMarcus Völp

DOI Link

Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, Marcus Völp
Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code
Proc. of the 7th Conference on Systems Software Verification (SSV'12), volume 102 of Electronic Proceedings in Theoretical Computer Science, 156--166, 2012

Details
Bibtex

KurzfassungAbstract
Reliability in terms of functional properties from the safety-liveness spectrum is an indispensable requirement of low-level operating-system (OS) code. However, with evermore complex and thus less predictable hardware, quantitative and probabilistic guarantees become more and more important. Probabilistic model checking is one technique to automatically obtain these guarantees. First experiences with the automated quantitative analysis of low-level operating-system code confirm the expectation that the naive probabilistic model checking approach rapidly reaches its limits when increasing the numbers of processes. This paper reports on our work-in-progress to tackle the state explosion problem for low-level OS-code caused by the exponential blow-up of the model size when the number of processes grows. We studied the symmetry reduction approach and carried out our experiments with a simple test-and-test-and-set lock case study as a representative example for a wide range of protocols with natural inter-process dependencies and long-run properties. We quickly see a state-space explosion for scenarios where inter-process dependencies are insignificant. However, once inter-process dependencies dominate the picture models with hundred and more processes can be constructed and analysed.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BDEHKKMTV2012,
  author    = {Christel Baier and Marcus Daum and Benjamin Engel and Hermann
               H{\"{a}}rtig and Joachim Klein and Sascha Kl{\"{u}}ppelholz and
               Steffen M{\"{a}}rcker and Hendrik Tews and Marcus V{\"{o}}lp},
  title     = {Chiefly Symmetric: Results on the Scalability of Probabilistic
               Model Checking for Operating-System Code},
  booktitle = {Proc. of the 7th Conference on Systems Software Verification
               (SSV'12)},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {102},
  year      = {2012},
  pages     = {156--166},
  doi       = {10.4204/EPTCS.102.14}
}