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 diferent directions are proposed.
In this work we are intersted in Model-Based Testing (MBT) for Real-Time Systems [
Timed Automata (TA) [
Deterministic Timed Automata represent a specific type of timed automata which has stronger properties. This class of timed automata may be used in diferent 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 inputoutput 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.
We adopt almost the same definitions and notations as in [22].
• 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 ;
TW(); • 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.: ⊆ • For = (1, 1) . . . (, ) ∈ TW(ACT) and ⊆ TW(ACT): − 1 := {︀ ′ ∈ TW() ⃒⃒ · ′ ∈ }︀ ;
In this case, we clearly have: − 1 ⊆ TW≥ (ACT).
A clock valuation is a function: CLOCKS = {c1, . . . , c} . ∈ RCLOCKS ≥ 0
assigning a non-negative real number (c) to every clock c ∈ CLOCKS. = 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 = { ∈ RCLOCKS | |= }.
≥ 0
A timed automaton (TA) is a tuple • 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:
TA = (, LOC, CLOCKS, INI, FIN, EDGES)
= (, , , rst, ) • ∈ 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 configuration of a timed automaton TA = (, LOC, CLOCKS, INI, FIN, EDGES) is a tuple: (, , _) • ∈ LOC; • ∈ RCLOCKS; • _ ∈ R; • ∀ c ∈ CLOCKS : (c) ≤ _.
A configuration is said to be initial if and only if: as follows: as follows: such that: • ∈ 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: For ∈ RCLOCKS, rst ⊆ CLOCKS and ∈ R, we define the valuation
CONFIG(TA).
[rst↦→] ∈ RCLOCKS • ∀ c ∈ rst: [rst↦→](c) = ; • ∀ c ∈ CLOCKS ∖ rst: [rst↦→](c) = (c).
Similarly for ∈ RCLOCKS and ∈ R, we define the valuation ∈ RCLOCKS • ∀ c ∈ CLOCKS: (c) = − (c).
For the edge = (, , , rst, ) ∈ EDGES, ∈ RCLOCKS and ∈ R, we define the transition: (, , _→−−)−− − , (, , ) • ∈ RCLOCKS; • ≥ _; • |= ; • = [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: and the set of configurations: we say that the sequence: = (1, 1) . . . (, ) ∈ TW(ACT) ( = (, , ))0≤ ≤ ⊆ CONFIG(TA) is a timed path of the timed automaton TA if for each 0 ≤ ≤ − 1: = →−−−0− − − 1,1 1 . . . →−−− − − 1−− − ,
→−− −−− − 1,1 +1 ∈ TRANS(TA).
The timed path is said to be accepted by the timed automaton TA if:
In case 0 ∈ ICONF(TA), we may also write: ∈ FCONF(TA).
0 ====⇒ .
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) =
⋃︁ ∈ICONF(TA)
TLangTA( ).
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.
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: (,+′) ============⇒ .
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 . Mathematically: (,+′) 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 if ∀ ∈ 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 .
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.
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 corresponding 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: (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:
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.
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 specifications 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. [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, Eficient 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 Computational 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.