Fast Parametric Model Checking With Applications to Software Performability Analysis

Xinwei Fang

doi:10.1109/TSE.2023.3313645

Fast Parametric Model Checking With Applications to Software Performability Analysis

2023-10-01

2

OA

AI

DOI：10.1109/TSE.2023.3313645

原文链接

原文求助

摘要

En 中文

We present an efficient parametric model checking technique for the analysis of software performability, i.e., of the performance and dependability properties of software systems. The new parametric model checking (pMC) technique works by using a heuristic to automatically decompose 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.

Keyword:

Markov processes

Parametric statistics

Software systems

Analytical models

Probabilistic logic

Web servers

Software algorithms

Parametric model checking

software performability

nonfunctional software properties

Markov models

Fast Parametric Model Checking With Applications to Software Performability Analysis

摘要

期刊

机构