Software Performability Analysis Using fPMC
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.
About fPMC
fPMC is a tool-supported approach that speeds up parametric model checking (PMC) by automatically decomposing
parametric discrete-time Markov chains (pDTMCs) models into fragments that can be analysed independently by exsiting PMC engines (e.g. PRISM and Storm), enabeling formal analysis of nonfunctional properties (e.g., reliability and performance) of software systems that are too complex to be handled by existing PMC engines.
fPMC builds on recent research that laid the groundwork for the use of pDTMC fragments to improve the applicability of exsiting parametric model checking (ePMC - efficient Parametric Model Checking)
fPMC is a fully automated compositional analysis technique that uses well-defined rules to partition the graph induced by the pDTMC under analysis into sub-graphs called fragments. Each such fragment defines a small pDTCM that is analysed individually to generate a PMC subexpression. Finally, the overall PMC result is obtained by combining these subexpressions with an expression produced by analysing an abstract pDTMC created by replacing each fragment from the original pDTMC with a single state.
Downloading fPMC
fPMC is freely available under the GNU General Public Licence and may be downloaded from the getting started page.Contacting us
If you wish to contact the corresponding authors, then please use the following email addresses:
Xinwei Fang: xinwei.fang@york.ac.uk
Radu Calinescu: radu.calinescu@york.ac.uk
Simos Gerasimou: simos.gerasimou@york.ac.uk
Reference
X. Fang, R. Calinescu, S. Gerasimou and F. Alhwikem, "Fast Parametric Model Checking through Model Fragmentation," 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), 2021, pp. 835-846, DOI: 10.1109/ICSE43902.2021.00081.