Timed Transition Tour for Race Detection in Distributed Systems

被引:1
作者
Vinarskii, Evgenii [1 ,3 ]
Kushik, Natalia [1 ]
Yevtushenko, Nina [2 ,3 ]
Lopez, Jorge [4 ]
Zeghlache, Djamal d [1 ]
机构
[1] Inst Polytech Paris, SAMOVAR, Telecom SudParis, Palaiseau, France
[2] Russian Acad Sci, Ivanikov Inst Syst Programming, Moscow, Russia
[3] Higher Sch Econ, Moscow, Russia
[4] Airbus, Issy Les Moulineaux, France
来源
PROCEEDINGS OF THE 18TH INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING, ENASE 2023 | 2023年
关键词
Races; Model Based Testing; Timed Finite State Machines; Timed Transition Tour;
D O I
10.5220/0011986700003464
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
The paper is devoted to detecting output races in distributed systems. We perform such detection through testing their implementations. As an underlying model for our test generation strategy we consider a Timed Finite State Machine or a TFSM (for short), where each input/output transition is augmented with a timed guard and an output delay. A potential output race can thus be simulated as an output delay mutant; this formalism is introduced in the paper. In order to build a test suite, we adapt a well-known test generation strategy, a transition tour method. The novelty of the proposed method relies on choosing appropriate timestamps for inputs, yielding a timed transition tour. We discuss its fault coverage for output race detection. As an application case study, we consider a Software Defined Networking (SDN) framework where the system under test is represented by the composition of a controller and a switch. Experimental results show that the timed transition tour can detect races in the behavior of the widely used ONOS controller.
引用
收藏
页码:613 / 620
页数:8
相关论文
共 22 条
  • [1] Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
  • [2] Constraint-Based Oracles for Timed Distributed Systems
    Benharrat, Nassim
    Gaston, Christophe
    Hierons, Robert M.
    Lapitre, Arnault
    Le Gall, Pascale
    [J]. TESTING SOFTWARE AND SYSTEMS (ICTSS 2017), 2017, 10533 : 276 - 292
  • [3] Equivalence checking and intersection of deterministic timed finite state machines
    Bresolin, Davide
    El-Fakih, Khaled
    Villa, Tiziano
    Yevtushenko, Nina
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2021, 59 (1-3) : 77 - 102
  • [4] Z3: An efficient SMT solver
    de Moura, Leonardo
    Bjorner, Nikolaj
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
  • [5] El-Hassany A, 2016, ACM SIGPLAN NOTICES, V51, P402, DOI [10.1145/2980983.2908124, 10.1145/2908080.2908124]
  • [6] Li A, 2022, Arxiv, DOI arXiv:2209.04026
  • [7] DCatch: Automatically detecting distributed concurrency bugs in cloud systems
    Liu H.
    Li G.
    Lukman J.F.
    Li J.
    Lu S.
    Gunawi H.S.
    Tian C.
    [J]. 1600, Association for Computing Machinery, 2 Penn Plaza, Suite 701, New York, NY 10121-0701, United States (52): : 677 - 691
  • [8] Predictive analysis for race detection in software-defined networks
    Lu, Gongzheng
    Xu, Lei
    Yang, Yibiao
    Xu, Baowen
    [J]. SCIENCE CHINA-INFORMATION SCIENCES, 2019, 62 (06)
  • [9] Lynch Nancy A, 1989, CWI Quaterly, V2, P219
  • [10] McClurg Jedidiah, 2021, SOSR '21: Proceedings of the ACM SIGCOMM Symposium on SDN Research (SOSR), P66, DOI 10.1145/3482898.3483362