Model-Based Testing IoT Communication via Active Automata Learning

被引:66
作者
Tappler, Martin [1 ]
Aichernig, Bernhard K. [1 ]
Bloem, Roderick [2 ]
机构
[1] Graz Univ Technol, Inst Software Technol, Graz, Austria
[2] Graz Univ Technol, Inst Appl Informat Proc & Commun, Graz, Austria
来源
2017 10TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST) | 2017年
关键词
GENERATION; CHECKING;
D O I
10.1109/ICST.2017.32
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper presents a learning-based approach to detecting failures in reactive systems. The technique is based on inferring models of multiple implementations of a common specification which are pair-wise cross-checked for equivalence. Any counterexample to equivalence is flagged as suspicious and has to be analysed manually. Hence, it is possible to find possible failures in a semi-automatic way without prior modelling. We show that the approach is effective by means of a case study. For this case study, we carried out experiments in which we learned models of five implementations of MQTT brokers/servers, a protocol used in the Internet of Things. Examining these models, we found several violations of the MQTT specification. All but one of the considered implementations showed faulty behaviour. In the analysis, we discuss effectiveness and also issues we faced.
引用
收藏
页码:276 / 287
页数:12
相关论文
共 49 条
  • [1] Aarts Fides, 2012, FM 2012: Formal Methods. Proceedings of the 18th International Symposium, P10, DOI 10.1007/978-3-642-32759-9_4
  • [2] Learning Register Automata with Fresh Value Generation
    Aarts, Fides
    Fiterau-Brostean, Paul
    Kuppens, Harco
    Vaandrager, Frits
    [J]. THEORETICAL ASPECTS OF COMPUTING - ICTAC 2015, 2015, 9399 : 165 - 183
  • [3] Aarts F, 2010, LECT NOTES COMPUT SC, V6435, P188, DOI 10.1007/978-3-642-16573-3_14
  • [4] Symbolic Input-Output Conformance Checking for Model-Based Mutation Testing
    Aichernig, Bernhard K.
    Tappler, Martin
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2016, 320 : 3 - 19
  • [5] Model-based mutation testing via symbolic refinement checking
    Aichernig, Bernhard K.
    Joebstl, Elisabeth
    Tiran, Stefan
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2015, 97 : 383 - 404
  • [6] Aichernig BK, 2006, LECT NOTES COMPUT SC, V3922, P324
  • [7] A THEORY OF TIMED AUTOMATA
    ALUR, R
    DILL, DL
    [J]. THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) : 183 - 235
  • [8] LEARNING REGULAR SETS FROM QUERIES AND COUNTEREXAMPLES
    ANGLUIN, D
    [J]. INFORMATION AND COMPUTATION, 1987, 75 (02) : 87 - 106
  • [9] [Anonymous], 2016, ISO/IEC 20922:2016
  • [10] [Anonymous], MQTT VERSION 3 1 1