Learning and statistical model checking of system response times

被引:9
作者
Aichernig, Bernhard K. [1 ]
Bauerstaetter, Priska [2 ]
Joebstl, Elisabeth [3 ]
Kann, Severin [3 ]
Korosec, Robert [3 ]
Krenn, Willibald [2 ]
Mateis, Cristinel [2 ]
Schlick, Rupert [2 ]
Schumi, Richard [1 ]
机构
[1] Graz Univ Technol, Inst Software Technol, Graz, Austria
[2] Austrian Inst Technol, Vienna, Austria
[3] AVL List GmbH, Graz, Austria
关键词
Statistical model checking; Property-based testing; Model-based testing; FsCheck; User profiles; Response time; Cost learning; Performance testing;
D O I
10.1007/s11219-018-9432-8
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Since computers have become increasingly more powerful, users are less willing to accept slow responses of systems. Hence, performance testing is important for interactive systems. However, it is still challenging to test if a system provides acceptable performance or can satisfy certain response-time limits, especially for different usage scenarios. On the one hand, there are performance-testing techniques that require numerous costly tests of the system. On the other hand, model-based performance analysis methods have a doubtful model quality. Hence, we propose a combined method to mitigate these issues. We learn response-time distributions from test data in order to augment existing behavioral models with timing aspects. Then, we perform statistical model checking with the resulting model for a performance prediction. Finally, we test the accuracy of our prediction with hypotheses testing of the real system. Our method is implemented with a property-based testing tool with integrated statistical model checking algorithms. We demonstrate the feasibility of our techniques in an industrial case study with a web-service application.
引用
收藏
页码:757 / 795
页数:39
相关论文
共 50 条
[41]   Schedulability of Herschel revisited using statistical model checking [J].
David, Alexandre ;
Larsen, Kim G. ;
Legay, Axel ;
Mikucionis, Marius .
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2015, 17 (02) :187-199
[42]   Statistical Model Checking of Cooperative Autonomous Driving Systems [J].
Bernardeschi, Cinzia ;
Lettieri, Giuseppe ;
Rossi, Federico .
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: RIGOROUS ENGINEERING OF COLLECTIVE ADAPTIVE SYSTEMS, PT II, ISOLA 2024, 2025, 15220 :316-332
[43]   TraceVis: Towards Visualization for Deep Statistical Model Checking [J].
Gros, Timo P. ;
Gross, David ;
Gumhold, Stefan ;
Hoffmann, Jorg ;
Klauck, Michaela ;
Steinmetz, Marcel .
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: TOOLS AND TRENDS, ISOLA 2020, PT IV, 2021, 12479 :27-46
[44]   DyNeMoC: Statistical Model Checking for Agent Based Systems on Graphs [J].
Ramesh, Yenda ;
Anand, Nikhil ;
Rao, M. V. Panduranga .
PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS (PRIMA 2019), 2019, 11873 :627-634
[45]   Statistical Model Checking for Dynamical Processes on Networks: A Healthcare Application [J].
Ramesh, Yenda ;
Anand, Nikhil ;
Rao, M. V. Panduranga .
2019 11TH INTERNATIONAL CONFERENCE ON COMMUNICATION SYSTEMS & NETWORKS (COMSNETS), 2019, :720-725
[46]   Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification [J].
Zuliani, Paolo ;
Platzer, Andre ;
Clarke, Edmund M. .
HSSC 10: PROCEEDINGS OF THE 13TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2010, :243-252
[47]   A statistical model checking approach to analyse the random access protocol [J].
Roumane A. ;
Kechar B. .
International Journal of Wireless and Mobile Computing, 2022, 23 (3-4) :338-349
[48]   Statistical abstraction and model-checking of large heterogeneous systems [J].
Basu A. ;
Bensalem S. ;
Bozga M. ;
Delahaye B. ;
Legay A. .
International Journal on Software Tools for Technology Transfer, 2012, 14 (01) :53-72
[49]   Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking [J].
Jegourel, Cyrille ;
Sun, Jun ;
Dong, Jin Song .
ACM TRANSACTIONS ON MODELING AND COMPUTER SIMULATION, 2019, 29 (04)
[50]   Research on verification of properties for cps based on statistical model checking [J].
Chen, Mingcai ;
Zhang, Guangquan ;
Wei, Hui ;
Shao, Yuzhen ;
Xu, Chengkai ;
Zheng, Linfeng .
Journal of Computational Information Systems, 2014, 10 (02) :747-754