=Paper=
{{Paper
|id=Vol-3067/paper6
|storemode=property
|title=Testing Timed Systems Using Determinization Techniques for One-Clock Timed Automata
|pdfUrl=https://ceur-ws.org/Vol-3067/paper6.pdf
|volume=Vol-3067
|authors=Moez Krichen
|dblpUrl=https://dblp.org/rec/conf/tacc/Krichen21
}}
==Testing Timed Systems Using Determinization Techniques for One-Clock Timed Automata ==
https://ceur-ws.org/Vol-3067/paper6.pdf
Testing Timed Systems Using Determinization
Techniques for One-Clock Timed Automata
Moez Krichen1,2
1
Faculty of Computer Science and Information Technology, Al-Baha University, KSA
2
ReDCAD Research Laboratory, University of Sfax, Tunisia
Abstract
In this work, we are interested in formal Model-Based Testing for Real-Time Systems. The proposed
approach is based on the use of the model of Timed Automata with continuous clocks for which we
adopt the reset-point semantics. We remind the definition of timed conformance relation tioco. We
extend the notion of soundness and completeness of test suites. We also consider specifications in form
of one-clock input-complete timed automata. Moreover, we provide interesting decidability results for
the considered classes of specifications. More specifically, we consider the case when some parameters of
the timed-automaton tester are fixed in advance, namely the number of clocks of the timed-automaton
and its maximal time-constraint constants. Finally, several possible extensions of the present work in
different directions are proposed.
Keywords
Model-Based Testing (MBT) | Formal Methods (FM) | Real-Time Testing (RTT) | Determinization
Techniques (DT) | One-Clock Timed Automata (OC-TA)
1. Introduction
In this work we are intersted in Model-Based Testing (MBT) for Real-Time Systems [1, 2].
This technique consists in describing the behavior of the System Under Test (SUT) using a
specific adequate formalism and then producing automatically test scenarios from the available
descriptions with respect to some selection criteria adopting some coverage methods. The next
phase consists in running the obtained tests suites on the SUT and calculating the corresponding
verdicts in order to check whether the implementation conforms to its model or not. This paper
extends some of our previous contributions [3, 4, 5] about MBT for real-time systems. These
works were mainly built on the classical timed automaton model [6].
Timed Automata (TA) [7] model is one of the most well-known mathematical formalism for
designing real-time systems. This model can be seen as an extension of finite automata with
continuous clocks which may be used to guarantee the correctness of some timed-constraints.
Many tools based on this model were developped during the last few years, namely: UPPAAL
[8], PRISM [9], UPPAAL Tiga [10], etc.
Tunisian Algerian Conference on Applied Computing (TACC 2021), December 18–20, 2021, Tabarka, Tunisia
$ moez.krichen@redcad.org (M. Krichen)
https://www.redcad.org/members/mkrichen/ (M. Krichen)
0000-0001-8873-9755 (M. Krichen)
© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)
Deterministic Timed Automata represent a specific type of timed automata which has stronger
properties. This class of timed automata may be used in different fields like learning [11, 12],
fault diagnosis [13], test generation [14], etc. In general, it is not possible to convert a given
non-deterministic timed automaton to an equivalent deterministic timed automata. However,
there are some specific classes of timed automata which are determinisable such as: timed
automata with integer-resets [15], event-clock timed automata [16], strongly non-zeno timed
automata [17], etc. For the case where determinization [18] is not possible, it may be possible
to use some approximation techniques like the ones proposed in [19, 20, 21] in the context of
model-based testing of real-time systems.
Our new proposed approach is mainly inspired by [22]. We adopt the reset-point semantics for
timed-automata for model-based testing purposes. We adapt the definition of our timed input-
output conformance relation tioco with respect to the new considered semantics. We extend
the notion of soundness and completeness of test suites correspondingly. We also consider the
case of specifications given as one-clock input-complete timed automata for which interesting
decidability properties exist. More precisely, we consider the case when some parameters of the
timed-automaton tester are fixed in advance (e.g., number of clocks and maximal constants).
Next in Section 2 we recall some fundamentals about timed languages and clock-constraints.
In Section 3 we give details about the timed automaton model and the underlying semantics.
Section 4 introduces the adopted testing framework. Section 5 summarizes the most important
results. Finally, Section 6 concludes the article and proposes some directions for future work.
2. Fundamentals
We adopt almost the same definitions and notations as in [22].
2.1. Timed Languages
Consider:
• ACT: a nonempty finite set of discrete actions;
• R𝑒𝑎𝑙𝑠: the set of reals;
• R𝑒𝑎𝑙𝑠≥0 : the set of nonnegative reals.
A timed word 𝑡𝑤 over the set of actions ACT is of the form:
𝑡𝑤 = (𝑎𝑐𝑡1 , 𝑡𝑖𝑚𝑒1 ) . . . (𝑎𝑐𝑡𝑛 , 𝑡𝑖𝑚𝑒𝑛 ) ∈ (ACT × R𝑒𝑎𝑙𝑠)* such that the sequence of instants
𝑡𝑖𝑚𝑒𝑖 satisfy the following:
0 ≤ 𝑡𝑖𝑚𝑒1 ≤ 𝑡𝑖𝑚𝑒2 ≤ · · · ≤ 𝑡𝑖𝑚𝑒𝑛 .
Given two timed words 𝑡𝑤1 and 𝑡𝑤2 such that:
• 𝑡𝑤1 = (𝑎𝑐𝑡1 , 𝑡𝑖𝑚𝑒1 ) . . . (𝑎𝑐𝑡𝑛 , 𝑡𝑖𝑚𝑒𝑛 );
• 𝑡𝑤2 = (𝑎𝑐𝑡𝑛+1 , 𝑡𝑖𝑚𝑒𝑛+1 ) . . . (𝑎𝑐𝑡𝑛+𝑚 , 𝑡𝑖𝑚𝑒𝑛+𝑚 );
• 𝑡𝑖𝑚𝑒𝑛+1 ≥ 𝑡𝑖𝑚𝑒𝑛 .
The concatenation of 𝑡𝑤1 and 𝑡𝑤2 denoted 𝑡𝑤1 · 𝑡𝑤2 is defined as:
𝑡𝑤1 · 𝑡𝑤2 = (𝑎𝑐𝑡1 , 𝑡𝑖𝑚𝑒1 ) . . . (𝑎𝑐𝑡𝑛 , 𝑡𝑖𝑚𝑒𝑛 )(𝑎𝑐𝑡𝑛+1 , 𝑡𝑖𝑚𝑒𝑛+1 ) . . . (𝑎𝑐𝑡𝑛+𝑚 , 𝑡𝑖𝑚𝑒𝑛+𝑚 ).
We also define the following entities:
• TW(ACT): the set of timed words over 𝐴𝑐𝑡;
• For 𝑡𝑖𝑚𝑒 ∈ R, TW≥𝑡𝑖𝑚𝑒 (𝐴𝑐𝑡): the set of timed words such that 𝑡𝑖𝑚𝑒1 ≥ 𝑡𝑖𝑚𝑒;
• A timed language 𝑇 𝐿 over the set of actions 𝐴𝑐𝑡 is a subset of TW(𝐴𝑐𝑡), i.e.: 𝑇 𝐿 ⊆
TW(𝐴𝑐𝑡);
• For 𝑡𝑤 = (𝑎𝑐𝑡1 , 𝑡𝑖𝑚𝑒1 ) . . . (𝑎𝑐𝑡𝑛 , 𝑡𝑖𝑚𝑒𝑛 ) ∈ TW(ACT) and 𝑇 𝐿 ⊆ TW(ACT):
𝑡𝑤−1 𝑇 𝐿 := 𝑡𝑤′ ∈ TW(𝐴𝑐𝑡) ⃒ 𝑡𝑤 · 𝑡𝑤′ ∈ 𝑇 𝐿 ;
{︀ ⃒ }︀
In this case, we clearly have: 𝑡𝑤−1 𝑇 𝐿 ⊆ TW≥𝑡𝑖𝑚𝑒𝑛 (ACT).
2.2. Clock constraints
Consider a finite set of clocks:
CLOCKS = {c𝑙𝑜𝑐𝑘1 , . . . , c𝑙𝑜𝑐𝑘𝑘 } .
A clock valuation is a function:
𝑣𝑎𝑙 ∈ R𝑒𝑎𝑙𝑠CLOCKS
≥0
assigning a non-negative real number 𝑣𝑎𝑙(c𝑙𝑜𝑐𝑘) to every clock c𝑙𝑜𝑐𝑘 ∈ CLOCKS.
A clock constraint is a formula of the form:
𝜙 = true | false | c𝑙𝑜𝑐𝑘𝑖 − c𝑙𝑜𝑐𝑘𝑗 cmp 𝑐𝑜𝑛𝑠𝑡 | c𝑙𝑜𝑐𝑘𝑖 cmp 𝑐𝑜𝑛𝑠𝑡 | 𝜙1 ∧ 𝜙2
such that cmp ∈ {<, ≤, =, >, ≥} is a comparison operator and 𝑐𝑜𝑛𝑠𝑡 ∈ N.1
We say that the valuation 𝑣𝑎𝑙 satisfies the constraint 𝜙 if interpreting every clock c𝑙𝑜𝑐𝑘𝑖 by
𝑣𝑎𝑙(c𝑙𝑜𝑐𝑘𝑖 ) makes the clock constraint 𝜙 a tautology. In this case, we will use the following
notation:
𝑣𝑎𝑙 |= 𝜙.
We also define the set of valuations satisfying 𝜙 as follows:
J𝜙K = {𝑣𝑎𝑙 ∈ R𝑒𝑎𝑙𝑠CLOCKS
≥0 | 𝑣𝑎𝑙 |= 𝜙}.
1
N being the set of non-negative integers.
3. Timed automata
A timed automaton (TA) is a tuple
TA = (𝐴𝑐𝑡, LOC, CLOCKS, INI, FIN, EDGES)
such that:
• ACT: finite set of discrete actions;
• LOC: finite set of locations;
• CLOCKS: finite set of continuous clocks;
• INI ⊆ LOC: set of initial locations;
• FIN ⊆ LOC: set of final locations;
• EDGES: finite set of edges.
The edges in EDGES are of the form:
𝑒𝑑𝑔 = (𝑙𝑜𝑐𝑖 , 𝑎𝑐𝑡, 𝜙, rst, 𝑙𝑜𝑐𝑗 )
such that:
• 𝑙𝑜𝑐𝑖 ∈ LOC: source location of the transition;
• 𝑙𝑜𝑐𝑗 ∈ LOC: destination location of the transition;
• 𝑎𝑐𝑡 ∈ ACT: discrete action labeling the transition;
• 𝜙: clock constraint that must be true for allowing the transition to be executed;
• rst ⊆ CLOCKS: the set of clocks to be reset after the execution of the transition.
Next, we introduce the so-called reset-point semantics [23, 24] for timed automata. A configu-
ration of a timed automaton TA = (𝐴𝑐𝑡, LOC, CLOCKS, INI, FIN, EDGES) is a tuple:
(𝑙𝑜𝑐, 𝑣𝑎𝑙, 𝑐𝑢𝑟𝑟𝑒𝑛𝑡_𝑡𝑖𝑚𝑒)
such that:
• 𝑙𝑜𝑐 ∈ LOC;
• 𝑣𝑎𝑙 ∈ R𝑒𝑎𝑙𝑠CLOCKS ;
• 𝑐𝑢𝑟𝑟𝑒𝑛𝑡_𝑡𝑖𝑚𝑒 ∈ R𝑒𝑎𝑙𝑠;
• ∀ c𝑙𝑜𝑐𝑘 ∈ CLOCKS : 𝑣𝑎𝑙(c𝑙𝑜𝑐𝑘) ≤ 𝑐𝑢𝑟𝑟𝑒𝑛𝑡_𝑡𝑖𝑚𝑒.
A configuration is said to be initial if and only if:
• 𝑙𝑜𝑐 ∈ INI;
• 𝑐𝑢𝑟𝑟𝑒𝑛𝑡_𝑡𝑖𝑚𝑒 = 0;
• ∀ c𝑙𝑜𝑐𝑘 ∈ CLOCKS : 𝑣𝑎𝑙(c𝑙𝑜𝑐𝑘) = 0.
A configuration is said to be final if and only if:
• 𝑙𝑜𝑐 ∈ FIN.
The set of all possible configurations of 𝑇 𝐴 is denoted:
CONFIG(TA).
For 𝑣𝑎𝑙 ∈ R𝑒𝑎𝑙𝑠CLOCKS , rst ⊆ CLOCKS and 𝑡𝑖𝑚𝑒 ∈ R𝑒𝑎𝑙𝑠, we define the valuation
𝑣𝑎𝑙[rst↦→𝑡𝑖𝑚𝑒] ∈ R𝑒𝑎𝑙𝑠CLOCKS
as follows:
• ∀ c𝑙𝑜𝑐𝑘 ∈ rst: 𝑣𝑎𝑙[rst↦→𝑡𝑖𝑚𝑒] (c𝑙𝑜𝑐𝑘) = 𝑡𝑖𝑚𝑒;
• ∀ c𝑙𝑜𝑐𝑘 ∈ CLOCKS ∖ rst: 𝑣𝑎𝑙[rst↦→𝑡𝑖𝑚𝑒] (c𝑙𝑜𝑐𝑘) = 𝑣𝑎𝑙(c𝑙𝑜𝑐𝑘).
Similarly for 𝑣𝑎𝑙 ∈ R𝑒𝑎𝑙𝑠CLOCKS and 𝑡𝑖𝑚𝑒 ∈ R𝑒𝑎𝑙𝑠, we define the valuation
𝑣𝑎𝑙𝑡𝑖𝑚𝑒 ∈ R𝑒𝑎𝑙𝑠CLOCKS
as follows:
• ∀ c𝑙𝑜𝑐𝑘 ∈ CLOCKS: 𝑣𝑎𝑙𝑡𝑖𝑚𝑒 (c𝑙𝑜𝑐𝑘) = 𝑡𝑖𝑚𝑒 − 𝑣𝑎𝑙(c𝑙𝑜𝑐𝑘).
For the edge 𝑒𝑑𝑔 = (𝑙𝑜𝑐𝑖 , 𝑎𝑐𝑡, 𝜙, rst, 𝑙𝑜𝑐𝑗 ) ∈ EDGES, 𝑣𝑎𝑙𝑖 ∈ R𝑒𝑎𝑙𝑠CLOCKS and 𝑡𝑖𝑚𝑒 ∈ R𝑒𝑎𝑙𝑠,
we define the transition:
𝑎𝑐𝑡,𝑡𝑖𝑚𝑒
(𝑙𝑜𝑐𝑖 , 𝑣𝑎𝑙𝑖 , 𝑐𝑢𝑟𝑟𝑒𝑛𝑡_𝑡𝑖𝑚𝑒) −−−−−→ (𝑙𝑜𝑐𝑗 , 𝑣𝑎𝑙𝑗 , 𝑡𝑖𝑚𝑒)
such that:
• 𝑣𝑎𝑙𝑗 ∈ R𝑒𝑎𝑙𝑠CLOCKS ;
• 𝑡𝑖𝑚𝑒 ≥ 𝑐𝑢𝑟𝑟𝑒𝑛𝑡_𝑡𝑖𝑚𝑒;
• 𝑣𝑎𝑙𝑡𝑖𝑚𝑒
𝑖 |= 𝜙;
• 𝑣𝑎𝑙𝑗 = 𝑣𝑎𝑙𝑖 [rst↦→𝑡𝑖𝑚𝑒] .
The set of all possible transitions of TA is denoted:
TRANS(TA).
The timed automaton TA induces a timed labeled transition system TLTS(TA) defined as
follows:
TLTS(TA) = (ICONF(TA); CONFIG(TA), TRANS(TA), FCONF(TA))
such that:
• ICONF(TA) is the set of all possible initial configurations;
• FCONF(TA) is the set of all possible final configurations.
Given the timed word:
𝑡𝑤 = (𝑎𝑐𝑡1 , 𝑡𝑖𝑚𝑒1 ) . . . (𝑎𝑐𝑡𝑛 , 𝑡𝑖𝑚𝑒𝑛 ) ∈ TW(ACT)
and the set of configurations:
(𝑐𝑜𝑛𝑓𝑖 = (𝑙𝑜𝑐𝑖 , 𝑣𝑎𝑙𝑖 , 𝑡𝑖𝑚𝑒𝑖 ))0≤𝑖≤𝑛 ⊆ CONFIG(TA)
we say that the sequence:
𝑎𝑐𝑡1 ,𝑡𝑖𝑚𝑒1 𝑎𝑐𝑡𝑛 ,𝑡𝑖𝑚𝑒𝑛
𝑡𝑝 = 𝑐𝑜𝑛𝑓0 −−−−−−→ 𝑐𝑜𝑛𝑓1 . . . 𝑐𝑜𝑛𝑓𝑛−1 −−−−−−−→ 𝑐𝑜𝑛𝑓𝑛
is a timed path of the timed automaton TA if for each 0 ≤ 𝑖 ≤ 𝑛 − 1:
𝑎𝑐𝑡1 ,𝑡𝑖𝑚𝑒1
𝑐𝑜𝑛𝑓𝑖 −−−−−−→ 𝑐𝑜𝑛𝑓𝑖+1 ∈ TRANS(TA).
The timed path 𝑡𝑝 is said to be accepted by the timed automaton TA if:
𝑐𝑜𝑛𝑓𝑛 ∈ FCONF(TA).
In this case, we will use the following notation:
𝑡𝑤
𝑐𝑜𝑛𝑓0 ====⇒ 𝑐𝑜𝑛𝑓𝑛 .
In case 𝑐𝑜𝑛𝑓0 ∈ ICONF(TA), we may also write:
𝑡𝑤
TA ====⇒ 𝑐𝑜𝑛𝑓𝑛 .
Consider the configuration 𝑐𝑜𝑛𝑓 = (𝑙𝑜𝑐, 𝑣𝑎𝑙, 𝑡𝑖𝑚𝑒) ∈ CONFIG(TA) and the timed word:
𝑡𝑤
𝑡𝑤 ∈ TW(ACT). We will use the notation: 𝑐𝑜𝑛𝑓 ====⇒ in case there exists a configuration
𝑡𝑤
𝑐𝑜𝑛𝑓 ′ ∈ FCONF(TA) such that: 𝑐𝑜𝑛𝑓 ====⇒ 𝑐𝑜𝑛𝑓 ′ . The timed language recognised by the
configuration 𝑐𝑜𝑛𝑓 ∈ CONFIG(TA) with respect to the timed automaton TA is defined as:
{︁ ⃒ }︁
𝑡𝑤
TLangTA (𝑐𝑜𝑛𝑓 ) = 𝑡𝑤 ∈ TW(ACT) ⃒ 𝑐𝑜𝑛𝑓 ====⇒ .
⃒
Similarly, the timed language recognised by the timed automaton TA is defined as:
⋃︁
TLang(TA) = TLangTA (𝑐𝑜𝑛𝑓 ).
𝑐𝑜𝑛𝑓 ∈ICONF(TA)
The timed automaton TA is called empty timed automaton when it recognizes the empty
language. That is:
TLang(TA) = ∅.
Similarly, it is called full timed automaton if it accepts all possible timed words. That is:
TLang(TA) = TW(ACT).
A timed automaton TA is said to be deterministic if it has only one initial location and, for
every two edges (𝑙𝑜𝑐1 , 𝑎𝑐𝑡, 𝜙, rst, 𝑙𝑜𝑐2 ) , (𝑙𝑜𝑐′1 , 𝑎𝑐𝑡′ , 𝜙′ , rst′ , 𝑙𝑜𝑐′2 ) ∈ EDGES, if 𝑙𝑜𝑐1 = 𝑙𝑜𝑐′1 ,
𝑎𝑐𝑡 = 𝑎𝑐𝑡′ and J𝜙 ∧ 𝜙′ K ̸= ∅ then rst = rst′ and 𝑙𝑜𝑐2 = 𝑙𝑜𝑐′2 . A One-Clock Timed Automaton
is a timed automaton which has only one clock.
4. Testing Framework
Starting from this section, we will assume that the set of actions ACT is equal to the union of two
disjoint sets ACTI and ACTO which are respectively the set of input-actions and output-actions.
That is:
ACT = ACTI ∪ ACTO and ACTI ∩ ACTO = ∅.
A given timed automaton TA is said to be input-complete if for every configuration 𝑐𝑜𝑛𝑓 =
(𝑙𝑜𝑐, 𝑣𝑎𝑙, 𝑡𝑖𝑚𝑒) ∈ CONFIG(TA) and each pair (𝑎𝑐𝑡, 𝑡𝑖𝑚𝑒′ ) ∈ ACTI × R𝑒𝑎𝑙𝑠≥0 we have:
(𝑎𝑐𝑡,𝑡𝑖𝑚𝑒+𝑡𝑖𝑚𝑒′ )
𝑐𝑜𝑛𝑓 ============⇒ .
4.1. Conformance Relation
Consider a timed automaton TA and a timed word 𝑡𝑤 ∈ TW(ACT), TA after 𝑡𝑤 is the set of
configurations of 𝒜 which may be reached after the execution of 𝑡𝑤. Mathematically:
𝑡𝑤
TA after 𝑡𝑤 = {𝑐𝑜𝑛𝑓 ∈ CONFIG(TA) | TA ====⇒ 𝑐𝑜𝑛𝑓 }.
Given the configuration 𝑐𝑜𝑛𝑓 = (𝑙𝑜𝑐, 𝑣𝑎𝑙, 𝑡𝑖𝑚𝑒) ∈ CONFIG(TA), outputs(𝑐𝑜𝑛𝑓 ) is the set of all
outputs that may be produced when the system is occupying configuration 𝑐𝑜𝑛𝑓 . Mathemati-
cally:
(𝑎𝑐𝑡,𝑡𝑖𝑚𝑒+𝑡𝑖𝑚𝑒′ )
outputs(𝑐𝑜𝑛𝑓 ) = {(𝑎𝑐𝑡, 𝑡𝑖𝑚𝑒′ ) ∈ ACTO × R𝑒𝑎𝑙𝑠≥0 | 𝑐𝑜𝑛𝑓 ============⇒}
The definition is extended naturally to a set of configurations 𝐶𝑜𝑛𝑓 .
⋃︁
outputs(𝐶𝑜𝑛𝑓 ) = outputs(𝑐𝑜𝑛𝑓 ).
𝑐𝑜𝑛𝑓 ∈𝐶𝑜𝑛𝑓
Given two timed automata 𝒮𝑝𝑒𝑐 (specification) and ℐ𝑚𝑝 (implementation) defined with respect
to the same sets of inputs and outputs The relation tioco [19, 25] is defined as follows:
ℐ𝑚𝑝 tioco 𝒮𝑝𝑒𝑐 iff ∀𝑡𝑤 ∈ TLang(𝒮𝑝𝑒𝑐) : outputs(ℐ𝑚𝑝 after 𝑡𝑤) ⊆ outputs(𝒮𝑝𝑒𝑐 after 𝑡𝑤).
The relation means that the implementation ℐ𝑚𝑝 conforms to the specification 𝒮𝑝𝑒𝑐 if and
only if for every timed word 𝑡𝑤 of 𝒮𝑝𝑒𝑐, the set of outputs of ℐ𝑚𝑝 after the execution of 𝑡𝑤 is
a subset of the set of outputs that can be generated by 𝒮𝑝𝑒𝑐.
4.2. Timed Test Cases
A timed test scenario for the specification 𝒮𝑝𝑒𝑐 over ACT is a total function
𝑇 𝑇 𝑆 : (R≥0 ∪ ACT)* → ACTI ∪ {WAITING, SUCCESS, REJECT}.
𝑇 𝑇 𝑆(𝑡𝑤) indicates the action that must be executed by the tester once it observes 𝑡𝑤. If
𝑇 𝑇 𝑆(𝑡𝑤) = 𝑖𝑛𝑝 ∈ ACTI then the tester produces input 𝑖𝑛𝑝. If 𝑇 𝑇 𝑆(𝑡𝑤) = WAITING then the
tester lets time elapse (waits). If 𝑇 𝑇 𝑆(𝑡𝑤) ∈ {SUCCESS, REJECT} then the tester produces a
verdict and stops.
The execution of 𝑇 𝑇 𝑆 on ℐ𝑚𝑝 may be seen as the parallel composition of the TLTS defined
by 𝑇 𝑇 𝑆 and ℐ𝑚𝑝. This composition is denoted by ℐ𝑚𝑝‖𝑇 𝑇 𝑆. Formally, we will announce
that the implementation ℐ𝑚𝑝 passes 𝑇 𝑇 𝑆, denoted ℐ𝑚𝑝 pass 𝑇 𝑇 𝑆, if state REJECT may not
be reached in ℐ𝑚𝑝‖𝑇 𝑇 𝑆. We conclude that the implementation passes (respectively fails) the
test suite 𝒯 𝒮𝒯 if it passes all tests (respectively fails at least one test) in 𝒯 𝒮𝒯 . 𝒯 𝒮𝒯 is said to
be sound with respect to 𝒮𝑝𝑒𝑐 if
∀ℐ𝑚𝑝 : ℐ𝑚𝑝 tioco 𝒮𝑝𝑒𝑐 ⇒ ℐ𝑚𝑝 pass 𝒯 𝒮𝒯 .
Similalry 𝒯 𝒮𝒯 is said to be complete with respect to 𝒮𝑝𝑒𝑐 if
∀ℐ𝑚𝑝 : ℐ𝑚𝑝 pass 𝒯 𝒮𝒯 ⇒ ℐ𝑚 tioco 𝒮𝑝𝑒𝑐.
The timed test suite 𝒯 𝒮𝒯 is said to be exact with respect to 𝒮𝑝𝑒𝑐 if it is both sound and complete
with respect to 𝒮𝑝𝑒𝑐.
Our goal is then to generate test suites which are both sound and complete. More specifically,
our goal is to produce timed test scenarios which are finitely representable in the form of
deterministic timed automata.
5. Main Results
In this section, we assume that the specification we have in hands is given as a non-deterministic
timed automaton 𝒮𝑝𝑒𝑐 which is input-complete and we aim to generate a timed tester corre-
sponding to this specification and which is represented using a deterministic timed automaton
𝑇 𝑇 𝑆 which is input-complete and which has one or more clocks. Next, we list some interesting
results about this timed automaton tester.
We first start with two intuitive rules related to the cases when the timed automaton tester is
empty and full respectively.
Lemma 1. If 𝑇 𝑇 𝑆 is empty then it is complete with respect to the specification 𝒮𝑝𝑒𝑐.
Lemma 2. If 𝑇 𝑇 𝑆 is full then it is sound with respect to the specification 𝒮𝑝𝑒𝑐.
Now, we consider the situation when the timed automaton tester 𝑇 𝑇 𝑆 is, respectively, an
under-approximation and an over-approximation of the specification 𝒮𝑝𝑒𝑐.
Lemma 3. If TLang(𝑇 𝑇 𝑆) ⊆ TLang(𝒮𝑝𝑒𝑐) (i.e., 𝑇 𝑇 𝑆 under-approximation of 𝒮𝑝𝑒𝑐) then 𝑇 𝑇 𝑆
is complete with respect to the specification 𝒮𝑝𝑒𝑐.
Lemma 4. If TLang(𝒮𝑝𝑒𝑐) ⊆ TLang(𝑇 𝑇 𝑆) (i.e., 𝑇 𝑇 𝑆 over-approximation of 𝒮𝑝𝑒𝑐) then 𝑇 𝑇 𝑆
is sound with respect to the specification 𝒮𝑝𝑒𝑐.
Consequently, we may deduce the following result.
Lemma 5. If TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆) then 𝑇 𝑇 𝑆 is exact with respect to the specification
𝒮𝑝𝑒𝑐.
Clearly, Lemma 1 (respectively, Lemma 2) can be seen as a particular case of Lemma 3
(respectively, Lemma4).
Next we consider the following list of problems and we check their decidability.
(P1) Given a specification presented as a non-deterministic timed automaton 𝒮𝑝𝑒𝑐 which has
two or more clocks, does it exist a deterministic timed automaton tester 𝑇 𝑇 𝑆 such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
(P2) Given a specification presented as a non-deterministic timed automaton 𝒮𝑝𝑒𝑐 which
has two or more clocks and given a non-negative integer 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘, does it exist a
deterministic timed automaton tester 𝑇 𝑇 𝑆 which has less than 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘 clocks and
such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
(P3) Given a specification presented as a non-deterministic timed automaton 𝒮𝑝𝑒𝑐 which has
two or more clocks and given two non-negative integers 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘 and 𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡
does it exist a deterministic timed automaton tester 𝑇 𝑇 𝑆 which has less than 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘
clocks, the numerical constants of which are equal or smaller than 𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡 and
such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
Lemma 6. The three above problems (P1), (P2) and (P3) are undecidable.
Next, we consider three similar problems for the case of one-clock non-deterministic timed
automata with epsilon transitions.
(P4) Given a specification presented as a one-clock non-deterministic timed automaton with
epsilon transitions 𝒮𝑝𝑒𝑐 which has two or more clocks, does it exist a deterministic
timed automaton tester 𝑇 𝑇 𝑆 such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
(P5) Given a specification presented as a one-clock non-deterministic timed automaton
with epsilon transitions 𝒮𝑝𝑒𝑐 and a non-negative integer 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘, does it exist a
deterministic timed automaton tester 𝑇 𝑇 𝑆 which has less than 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘 clocks and
such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
(P6) Given a specification presented as a one-clock non-deterministic timed automaton with
epsilon transitions 𝒮𝑝𝑒𝑐 and two non-negative integers 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘 and 𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡,
does it exist a deterministic timed automaton tester 𝑇 𝑇 𝑆 which has less than 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘
clocks, the numerical constants of which are equal or smaller than 𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡 and
such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
Lemma 7. The three problems (P4), (P5) and (P6) are undecidable too.
Next, we consider the situation where the specification 𝒮𝑝𝑒𝑐 is a one-clock timed automaton
without epsilon transitions.
(P7) Given a specification presented as a one-clock non-deterministic timed automaton
without epsilon transitions 𝒮𝑝𝑒𝑐 which has two or more clocks, does it exist a
deterministic timed automaton tester 𝑇 𝑇 𝑆 such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
(P10) Given a specification presented as a one-clock non-deterministic timed automaton
without epsilon transitions 𝒮𝑝𝑒𝑐 and a positive integer 𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡, does it exist a
deterministic timed automaton tester 𝑇 𝑇 𝑆 the numerical constants of which are equal or
smaller than 𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡 and such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
(P9) Given a specification presented as a one-clock non-deterministic timed automaton
without epsilon transitions 𝒮𝑝𝑒𝑐 and a non-negative integer 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘, does it exist
a deterministic timed automaton tester 𝑇 𝑇 𝑆 which has less than 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘 clocks and
such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
(P10) Given a specification presented as a one-clock non-deterministic timed automaton
without epsilon transitions 𝒮𝑝𝑒𝑐 and two non-negative integers 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘 and
𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡, does it exist a deterministic timed automaton tester 𝑇 𝑇 𝑆 which has
less than 𝑚𝑎𝑥_𝑐𝑙𝑜𝑐𝑘 clocks, the numerical constants of which are equal or smaller than
𝑚𝑎𝑥_𝑐𝑜𝑛𝑠𝑡𝑎𝑛𝑡 and such that:
TLang(𝒮𝑝𝑒𝑐) = TLang(𝑇 𝑇 𝑆).
Lemma 8. The problems (P7) and (P8) are undecidable while the problems (P9) and (P10) are
decidable.
The positive result mentioned in the second part of Lemma 8 may be useful for building exact
timed automata testers for the considered class of specifications (one-clock timed automata
without epsilon transitions). For the other situations where the considered problems are
undecidable, we may use approximation techniques to construct either sound or complete timed
automata testers which are as precise as possible.
6. Conclusion and Future Work
In this work, we presented a formal testing framework for real-time systems based on the model
of timed automata and the use of the reset-point semantics. Some interesting results were
identified. These results may represent a starting point for many future extensions:
• First, making some experimental work for developing timed testers for the case of specifi-
cations presented as one-clock timed automata without epsilon transitions.
• Second, identifying some optimal approximation techniques for generating timed testers
which are either sound or complete.
• Third, considering the case where the specification of the system under test is given as a
product of a set of timed automata.
• Fourth, considering other types of restrictions on the structure and the size of the timed
testers we aim to produce such as the number of locations, the number of edges, etc.
• Fifth, considering some adequate selection criteria for generating timed testers with
reasonable size and which guarantee optimal coverage of the considered specification.
References
[1] J. Tretmans, Testing concurrent systems: A formal approach, in: Proceedings of the 10th
International Conference on Concurrency Theory, CONCUR ’99, Springer-Verlag, London,
UK, UK, 1999, pp. 46–65. URL: http://dl.acm.org/citation.cfm?id=646734.701460.
[2] M. Krichen, Contributions to model-based testing of dynamic and distributed real-time
systems, Ph.D. thesis, École Nationale d’Ingénieurs de Sfax (Tunisie), 2018.
[3] M. Krichen, Testing real-time systems using determinization techniques for automata
over timed domains, in: International Colloquium on Theoretical Aspects of Computing,
Springer, Cham, 2019, pp. 124–133.
[4] M. Krichen, A formal framework for black-box conformance testing of distributed real-
time systems, International Journal Critical Computer Based Systems 3 (2012) 26–43. URL:
http://dx.doi.org/10.1504/IJCCBS.2012.045075. doi:10.1504/IJCCBS.2012.045075.
[5] M. Krichen, A formal framework for conformance testing of distributed real-time systems,
in: OPODIS, volume 6490 of Lecture Notes in Computer Science, Springer, 2010, pp. 139–142.
[6] R. Alur, D. Dill, The theory of timed automata, in: J. W. de Bakker, C. Huizing, W. P.
de Roever, G. Rozenberg (Eds.), Real-Time: Theory in Practice, Springer Berlin Heidelberg,
Berlin, Heidelberg, 1992, pp. 45–73.
[7] R. Alur, D. L. Dill, A theory of timed automata, Theor. Comput. Sci. 126 (1994) 183–235.
[8] G. Behrmann, A. David, K. G. Larsen, J. Hakansson, P. Petterson, W. Yi, M. Hendriks,
Uppaal 4.0, in: Proceedings of the 3rd International Conference on the Quantitative
Evaluation of Systems, QEST ’06, IEEE Computer Society, Washington, DC, USA, 2006, pp.
125–126. URL: https://doi.org/10.1109/QEST.2006.59. doi:10.1109/QEST.2006.59.
[9] M. Kwiatkowska, G. Norman, D. Parker, PRISM 4.0: Verification of probabilistic real-time
systems, in: G. Gopalakrishnan, S. Qadeer (Eds.), Proc. of CAV’11, volume 6806 of LNCS,
Springer, 2011, pp. 585–591.
[10] F. Cassez, A. David, E. Fleury, K. G. Larsen, D. Lime, Efficient on-the-fly algorithms for the
analysis of timed games, in: M. Abadi, L. de Alfaro (Eds.), Proc. of CONCUR’05, Springer
Berlin Heidelberg, Berlin, Heidelberg, 2005, pp. 66–80.
[11] S. Verwer, M. de Weerdt, C. Witteveen, An algorithm for learning real-time automata, in:
Proc of. the Annual Belgian-Dutch Machine Learning Conference (Benelearn’078), 2007.
[12] M. Tappler, B. K. Aichernig, K. G. Larsen, F. Lorber, Time to learn - learning timed automata
from tests, in: É. André, M. Stoelinga (Eds.), Proc. of FORMATS’19, Springer International
Publishing, Cham, 2019, pp. 216–235.
[13] P. Bouyer, F. Chevalier, D. D’Souza, Fault diagnosis using timed automata, in: Proc.
of FOSSACS’05, Springer-Verlag, Berlin, Heidelberg, 2005, pp. 219–233. doi:10.1007/
978-3-540-31982-5_14.
[14] B. Nielsen, A. Skou, Automated test generation from timed automata, International Journal
on Software Tools for Technology Transfer 5 (2003) 59–77. URL: https://doi.org/10.1007/
s10009-002-0094-1. doi:10.1007/s10009-002-0094-1.
[15] P. V. Suman, P. K. Pandya, S. N. Krishna, L. Manasa, Timed automata with integer
resets: Language inclusion and expressiveness, in: Proc. of FORMATS’08, Springer-Verlag,
Berlin, Heidelberg, 2008, pp. 78—92. URL: https://doi.org/10.1007/978-3-540-85778-5_7.
doi:10.1007/978-3-540-85778-5_7.
[16] R. Alur, L. Fix, T. A. Henzinger, Event-clock automata: a determinizable class of timed
automata, Theor. Comput. Sci. 211 (1999) 253–273.
[17] E. Asarin, O. Maler, A. Pnueli, J. Sifakis, Controller synthesis for timed automata, in: Proc.
of the 5th IFAC Conference on System Structure and Control (SSSC’98), volume 31, 1998,
pp. 447–452. doi:https://doi.org/10.1016/S1474-6670(17)42032-5.
[18] P. Bouyer, S. Jaziri, N. Markey, On the determinization of timed systems, in: FORMATS,
volume 10419 of Lecture Notes in Computer Science, Springer, 2017, pp. 25–41.
[19] M. Krichen, S. Tripakis, Conformance testing for real-time systems, Formal Methods in
System Design 34 (2009) 238–304. doi:10.1007/s10703-009-0065-1.
[20] N. Bertrand, A. Stainer, T. Jéron, M. Krichen, A game approach to determinize timed
automata, Formal Methods in System Design 46 (2015) 42–80.
[21] N. Bertrand, A. Stainer, T. Jéron, M. Krichen, A game approach to determinize timed
automata, in: International Conference on Foundations of Software Science and Computa-
tional Structures, Springer, Berlin, Heidelberg, 2011, pp. 245–259.
[22] L. Clemente, S. Lasota, R. Piórkowski, Determinisability of one-clock timed automata, 2020.
arXiv:2007.09340.
[23] L. Fribourg, A Closed-Form Evaluation for Extended Timed Automata, Technical Report,
CNRS & ECOLE NORMALE SUPERIEURE DE CACHAN, 1998.
[24] M. Bojańczyk, S. Lasota, A machine-independent characterization of timed languages, in:
Proc. ICALP 2012, 2012, pp. 92–103.
[25] M. Krichen, S. Tripakis, Interesting properties of the real-time conformance relation tioco,
in: K. Barkaoui, A. Cavalcanti, A. Cerone (Eds.), Theoretical Aspects of Computing - ICTAC
2006, Springer Berlin Heidelberg, Berlin, Heidelberg, 2006, pp. 317–331.