Software Performability Analysis Using Fast Parametric Model Checking

TL;DR

This paper introduces a fast parametric model checking technique that decomposes complex software models into manageable fragments, enabling efficient analysis of software performability properties that were previously infeasible to verify.

Contribution

The paper presents a novel, efficient PMC method that decomposes pDTMC models into fragments for independent analysis, improving speed and applicability over existing PMC techniques.

Findings

fPMC significantly reduces analysis time.

fPMC extends the range of analyzable complex systems.

Experimental results show improved efficiency and applicability.

Abstract

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.