Testing timed automata

被引:147
|
作者
Springintveld, J
Vaandrager, F
D'Argenio, PR
机构
[1] Univ Twente, Dept Comp Sci, NL-7500 AE Enschede, Netherlands
[2] Univ Nijmegen, Inst Comp Sci, NL-6500 GL Nijmegen, Netherlands
关键词
(black-box) conformance testing; real-time systems; timed automata; I/O automata; bisimulation;
D O I
10.1016/S0304-3975(99)00134-6
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We present a generalization of the classical theory of testing for Mealy machines to a setting of dense real-time systems. A model of timed I/O automata is introduced, inspired by the timed automaton model of Alur and Dill, together with a notion of test sequence for this model. Our main contributions is a test suite derivation algorithm for black-box conformance testing of timed I/O automata. Black-box testing amounts to checking whether an implementation conforms to a specification of its external behavior, by means of a set of tests derived solely from specification. The main problem is to derive a finite set of tests from a possibly infinite, dense time transition system representing the specification. The solution is to reduce the dense time transition system to an appropriate finite discrete subautomaton, the grid automaton, which contains enough information to completely represent the specification from a test perspective. Although the method results in a test suite of high exponential size and cannot be claimed to be of practical value, it gives the first algorithm that yields a finite and complete set of tests for dense real-time systems. (C) 2001 Elsevier Science B.V. All rights reserved.
引用
收藏
页码:225 / 257
页数:33
相关论文
共 50 条
  • [1] Timed automata and recognizability
    Hermann, P
    INFORMATION PROCESSING LETTERS, 1998, 65 (06) : 313 - 318
  • [2] Specification Mutation Analysis for Validating Timed Testing Approaches Based on Timed Automata
    AbouTrab, M. Saeed
    Counsell, Steve
    Hierons, Robert M.
    2012 IEEE 36TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2012, : 660 - 669
  • [3] Time for Networks: Mutation Testing for Timed Automata Networks
    Cortes, David
    Ortiz, James
    Basile, Davide
    Aranda, Jesus
    Perrouin, Gilles
    Schobbens, Pierre-Yves
    PROCEEDINGS OF THE 2024 IEEE/ACM 12TH INTERNATIONAL CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING, FORMALISE 2024, 2024, : 44 - 54
  • [4] A guided method for testing timed input output automata
    En-Nouaary, A
    Dssouli, R
    TESTING OF COMMUNICATING SYSTEMS, PROCEEDINGS, 2003, 2644 : 211 - 225
  • [5] From timed automata to testable untimed automata
    Petitjean, E
    Fouchal, H
    REAL TIME PROGRAMMING 1999 (WRTP'99), 1999, : 189 - 194
  • [6] Event-clock automata: a determinizable class of timed automata
    Alur, R
    Fix, L
    Henzinger, TA
    THEORETICAL COMPUTER SCIENCE, 1999, 211 (1-2) : 253 - 273
  • [7] A Flattening Algorithm for Hierarchical Timed Automata
    Podymov V.V.
    Computational Mathematics and Modeling, 2019, 30 (2) : 99 - 106
  • [8] Timed automata and additive clock constraints
    Bérard, B
    Dufourd, C
    INFORMATION PROCESSING LETTERS, 2000, 75 (1-2) : 1 - 7
  • [9] THE THEORY OF TIMED AUTOMATA
    ALUR, R
    DILL, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 600 : 45 - 73
  • [10] The Timestamp of Timed Automata
    Rosenmann, Amnon
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2019), 2019, 11750 : 181 - 198