论文标题
使用快速参数模型检查的软件性能分析
Software Performability Analysis Using Fast Parametric Model Checking
论文作者
论文摘要
我们提出了一种有效的参数模型检查（PMC）技术，用于分析软件性能性能的性能和可靠性属性。新的PMC技术通过自动分解正在验证的软件系统的参数离散时间马尔可夫链（PDTMC）模型中的片段，可以独立分析，从而产生结果，以建立所需的软件可得率属性。我们的快速参数模型检查（FPMC）技术使PDTMC建模的软件系统的正式分析太复杂，无法通过现有PMC方法处理。此外，对于许多最先进的参数模型检查器可以分析的PDTMC，FPMC会产生更简单且更快地评估的解决方案（即代数公式）。我们通过实验表明，将FPMC添加到PMC方法的现有曲目中，可以显着提高参数模型检查的效率，并将其适用性扩展到比当前更复杂的软件系统中。
We present an efficient parametric model checking (PMC) technique for the analysis of software performability, i.e., of the performance and dependability properties of software systems. The new PMC technique works by automatically decomposing a parametric discrete-time Markov chain (pDTMC) model of the software system under verification into fragments that can be analysed independently, yielding results that are then combined to establish the required software performability properties. Our fast parametric model checking (fPMC) technique enables the formal analysis of software systems modelled by pDTMCs that are too complex to be handled by existing PMC methods. Furthermore, for many pDTMCs that state-of-the-art parametric model checkers can analyse, fPMC produces solutions (i.e., algebraic formulae) that are simpler and much faster to evaluate. We show experimentally that adding fPMC to the existing repertoire of PMC methods improves the efficiency of parametric model checking significantly, and extends its applicability to software systems with more complex behaviour than currently possible.
