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.
翻译:为了分析软件的可性,即软件系统的性能和可靠性,我们提出了一种高效的参数模型检查技术(PMC)分析软件的可性,即软件系统的性能和可靠性。新的PMC技术是自动将所核查的软件系统的参数离散时间链模型(PDMC)分解成碎片,进行独立分析,产生结果,然后合并以建立所需的软件可性能特性。我们的快速参数模型检查技术(fPMC)使得能够正式分析由PDTMC公司模拟的软件系统,这些系统过于复杂,无法由现有的PMC公司方法处理。此外,对于许多能够分析最先进的参数模型检查器,FPMMC公司生产的解决办法(即代数公式)比较简单,而且比评估速度更快。我们实验性地表明,将FPPC公司加入现有的PMC方法重新组合,可以大大提高参数模型检查的效率,并将它的适用范围扩大到行为比目前可能复杂得多的软件系统。