By the same authors

From the same journal

Efficient Parametric Model Checking Using Domain Knowledge

Research output: Contribution to journalArticlepeer-review

Full text download(s)

Published copy (DOI)



Publication details

JournalIEEE Transactions on Software Engineering
DateAccepted/In press - 20 Apr 2019
DateE-pub ahead of print (current) - 25 Apr 2019
Number of pages20
Early online date25/04/19
Original languageEnglish


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 (e.g., patterns modelling the invocation of functionally-equivalent services used to jointly implement the same operation within service-based systems, or the deployment of the components of multi-tier software systems across multiple servers). 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 the analysis time by several orders of magnitude compared to current parametric model checking methods.

Bibliographical note

© Copyright 2019 IEEE - All rights reserved. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations