Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code
Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code
复制标题
主要对称：操作系统代码概率模型检查的可扩展性结果
DOI：
10.4204/eptcs.102.14
复制
发表时间：
2012
影响因子：
1
通讯作者：
M. Völp
中科院分区：
文献类型：
--
作者：
C. Baier;Marcus Daum;Benjamin Engel;Hermann Härtig;Joachim Klein;Sascha Klüppelholz;Steffen Märcker;H. Tews;M. Völp
从安全活性谱的功能属性方面的可靠性是低级操作系统（OS）代码的一个不可或缺的要求。然而，随着硬件越来越复杂，可预测性越来越差，定量和概率保证变得越来越重要。概率模型检查是自动获得这些保证的一种技术。低级操作系统代码的自动化定量分析的第一次经验证实了这样的期望，即当进程数量增加时，朴素概率模型检查方法迅速达到其极限。本文报告了我们正在进行的工作，以解决状态爆炸问题的低级别OS代码所造成的指数爆炸的模型大小时，进程的数量增长。我们研究了对称性约简方法，并进行了我们的实验与一个简单的测试和测试和设置锁的情况下，研究作为一个代表性的例子，广泛的协议与自然的进程间的依赖关系和长期运行的属性。在进程间依赖性不重要的场景中，我们很快就看到了状态空间爆炸。然而，一旦进程间的依赖关系占主导地位的图片模型与数百个和更多的进程可以构建和分析。
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.
DOI：
10.1109/qest.2009.21
发表时间：
2009-09
期刊：
2009 Sixth International Conference on the Quantitative Evaluation of Systems
影响因子：
--
作者：
Alastair F. Donaldson;Alice Miller;D. Parker
通讯作者：
Alastair F. Donaldson;Alice Miller;D. Parker
DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Basler G
通讯作者：
Basler G