Efficient Parametric Model Checking Using Domain Knowledge
This addresses efficiency issues in software reliability and performance analysis for engineers, though it appears incremental as it builds on existing parametric model checking methods.
The paper tackles the problem of slow parametric model checking for software system quality-of-service properties by introducing ePMC, which uses domain-specific patterns to precompute closed-form expressions, resulting in analysis time reductions of several orders of magnitude compared to existing methods.
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.