Efficient Parametric Model Checking Using Domain Knowledge

Radu Constantin Calinescu; Colin Paterson; Kenneth Harold Anthony Johnson

doi:10.1109/TSE.2019.2912958

Efficient Parametric Model Checking Using Domain Knowledge

Radu Constantin Calinescu, Colin Paterson, Kenneth Harold Anthony Johnson

Computer Science

Research output: Contribution to journal › Article › peer-review

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 (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.

Original language	English
Article number	8698796
Number of pages	20
Journal	IEEE Transactions on Software Engineering
Volume	0
Early online date	25 Apr 2019
DOIs	https://doi.org/10.1109/TSE.2019.2912958
Publication status	E-pub ahead of print - 25 Apr 2019

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.

Access to Document

10.1109/TSE.2019.2912958

TSE-ePMC-FINAL
© 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.
Accepted author manuscript, 1.16 MB

Radu Calinescu
- radu.calinescuyork.acuk
- Computer Science - Professor
Person: Academic

Cite this

@article{d24f7aaabce44797b1078b941040a88e,

title = "Efficient Parametric Model Checking Using Domain Knowledge",

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 (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.",

author = "Calinescu, {Radu Constantin} and Colin Paterson and Johnson, {Kenneth Harold Anthony}",

note = "{\textcopyright} Copyright 2019 IEEE - All rights reserved. This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details. ",

year = "2019",

month = apr,

day = "25",

doi = "10.1109/TSE.2019.2912958",

language = "English",

volume = "0",

journal = "IEEE Transactions on Software Engineering ",

issn = "0098-5589",

publisher = "IEEE",

}

TY - JOUR

T1 - Efficient Parametric Model Checking Using Domain Knowledge

AU - Calinescu, Radu Constantin

AU - Paterson, Colin

AU - Johnson, Kenneth Harold Anthony

N1 - © 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.

PY - 2019/4/25

Y1 - 2019/4/25

N2 - 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.

AB - 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.

U2 - 10.1109/TSE.2019.2912958

DO - 10.1109/TSE.2019.2912958

M3 - Article

SN - 0098-5589

VL - 0

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

M1 - 8698796

ER -

Efficient Parametric Model Checking Using Domain Knowledge

Abstract

Bibliographical note

Access to Document

Profiles

Radu Calinescu

Cite this