# Efficient Parametric Model Checking Using Domain Knowledge

## TL;DR

This paper presents ePMC, a novel parametric model checking approach that leverages domain knowledge to significantly accelerate the analysis of software system models, especially for QoS properties.

## Contribution

ePMC introduces a domain-specific precomputation technique for closed-form expressions, enabling faster analysis of complex software models compared to existing methods.

## Key findings

- Reduces analysis time by several orders of magnitude
- Effective for service-based systems and multi-tier architectures
- Demonstrates significant efficiency improvements over current methods

## Abstract

We introduce an efficient parametric model checking (ePMC) method for the analysis of reliability, performance and other quality-of-service (QoS) properties of software systems. ePMC speeds up the analysis of parametric Markov chains modelling the behaviour of software by exploiting domain-specific modelling patterns for the software components. To this end, ePMC precomputes closed-form expressions for key QoS properties of such patterns, and uses these expressions in the analysis of whole-system models. To evaluate ePMC, we show that its application to service-based systems and multi-tier software architectures reduces analysis time by several orders of magnitude compared to current parametric model checking methods.