Efficient Parametric Model Checking Using Domain-Specific Modelling Patterns

被引：2

作者：

Calinescu, Radu ^{[1
]}

Johnson, Kenneth ^{[2
]}

Paterson, Colin ^{[1
]}

机构：

[1] Univ York, Dept Comp Sci, York, N Yorkshire, England

[2] Auckland Univ Technol, Sch Engn Comp & Math Sci, Auckland, New Zealand

来源：

2018 IEEE/ACM 40TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: NEW IDEAS AND EMERGING TECHNOLOGIES RESULTS (ICSE-NIER) | 2018年

关键词：

D O I：

10.1145/3183399.3183404

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We propose a parametric model checking (PMC) method that enables the efficient analysis of quality-of-service (QoS) properties of component-based systems. Our method builds on recent advances in PMC techniques and tools, and can handle large models by exploiting domain-specific modelling patterns for the software components. We precompute closed-form expressions for key QoS properties of such patterns, and handle system-level PMC by combining these expressions into easy-to-evaluate systems of equations.

引用

页码：61 / 64

页数：4

共 16 条

[1] Andova S., 2004, Formal Modeling and Analysis of Timed Systems. First International Workshop, FORMATS 2003. Revised Papers. (Lecture Notes in Comput. Sci. Vol.2791), P88
[2] Calinescu Radu, 2012, Large-Scale Complex IT Systems. Development, Operation and Management. 17th Monterey Workshop 2012. Revised Selected Papers, P303, DOI 10.1007/978-3-642-34059-8_16
[3] Calinescu R, 2013, IEEE INT CONF AUTOM, P734, DOI 10.1109/ASE.2013.6693145
[4] Calinescu Radu, 2017, IEEE T SOFTWARE ENG, V99
[5] Daws C, 2005, LECT NOTES COMPUT SC, V3407, P280
[6] A STORM is Coming: A Modern Probabilistic Model Checker
Dehnert, Christian
Junges, Sebastian
Katoen, Joost-Pieter
Volk, Matthias
[J]. COMPUTER AIDED VERIFICATION (CAV 2017), PT II, 2017, 10427 : 592 - 600
[7] Gallotti S, 2008, LECT NOTES COMPUT SC, V5281, P119, DOI 10.1007/978-3-540-87879-7_8
[8] Search-Based Synthesis of Probabilistic Models for Quality-of-Service Software Engineering
Gerasimou, Simos
Tamburrelli, Giordano
Calinescu, Radu
[J]. 2015 30TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2015, : 319 - 330
[9] Model-based verification of quantitative non-functional properties for software product lines
Ghezzi, Carlo
Sharifloo, Amir Molzam
[J]. INFORMATION AND SOFTWARE TECHNOLOGY, 2013, 55 (03) : 508 - 524
[10] Probabilistic reachability for parametric markov models
Hahn E.M.
Hermanns H.
Zhang L.
[J]. International Journal on Software Tools for Technology Transfer, 2011, 13 (1) : 3 - 19

← 1 2 →