Alexandre David
email: adavid@cs.aau.dk

Kim G Larsen

Marius Mikučionis
email: marius@cs.aau.dk

Omer L Nguena Timo

Antoine Rollet
email: rollet@labri.fr

Remote Testing of Timed Specifications ⋆

We present a study and a testing framework on black box remote testing of real-time systems using Uppaal-TIGA. One of the essential challenges of remote testing is the communication latency between the tester and the system under test (SUT) that may lead to interleaving of inputs and outputs. This affects the generation of inputs for the SUT and the observation of outputs that may trigger a wrong test verdict. We model the overall test setup using Timed Input-Output Automata (TIOA) and present an adapted asynchronous semantics with explicit communication delays. We propose the ∆-testability criterion for the requirement model where ∆ describes the communication latency. The test case generation problem is then reduced into a controller synthesis problem. We use Uppaal-TIGA for this purpose to solve a timed game with partial observability between the tester and the communication media together with the SUT. The objective of the game corresponds to a test purpose.

Introduction

This paper deals with black box conformance testing of remote real-time systems. Usually, conformance black-box testing is an activity where a tester executes selected test cases on a system (implementation) under test (SUT) and emits a test verdict (pass, fail, etc.). This verdict indicates the conformance between SUTs and the specification. It is computed according to the specification and a conformance relation between SUTs and the specification. Usually, the assumption of zero delay and synchronous communication between the tester and the SUT is done, but this is not realistic in many situations, such as network applications, or systems when time matters. In some cases, it may provide an erroneous verdict, potentially implying catastrophic situations. Our goal is to study the impact of explicit propagation delays between the implementation and the tester on test case generation and execution, and to provide a general testing framework for remote testing of real-time systems modeled with timed automata. ioco based theory. In the case of untimed systems, the most common approaches are based on the Labeled Transition Systems (LTS) model, which is used as a semantics for many standardized languages such as SDL [START_REF] Mammeri | Introduction au langage de description et de spécification (sdl)[END_REF] or LOTOS [START_REF]ISO: Information processing systems -open systems interconnection -LOTOS[END_REF]. The ioco relation theory [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF] proposes a complete testing approach for LTS with inputs and outputs, using the idea that any output of the implementation should be authorized by the specification.

They also introduce the notion of quiescence permitting to consider blocking states as a special output which should be explicitly specified. A complete framework based on this theory has been proposed in [START_REF] Jard | TGV: theory[END_REF], especially providing the possibility to use Test Purposes in order to lead the testing process.

Testing with time. The ioco theory has inspired many testing approaches. [START_REF] Núñez | Conformance testing relations for timed systems[END_REF] proposes an extension of the Finite States Machines with Time (TEFSM) and defines adapted conformance relations. [START_REF] Krichen | Black-box conformance testing for real-time systems[END_REF], [START_REF] Mikučionis | T-uppaal: Online model-based testing of realtime systems[END_REF] and [START_REF] Hessel | Testing real-time systems using uppaal[END_REF] propose extensions of ioco relation with time (tioco) including delays in the set of observable actions, leading to infinite systems. They propose non deterministic test generation algorithms based on Timed Input/Output Automata (TIOA). [START_REF] Hessel | Testing real-time systems using uppaal[END_REF] also shows how to use the Uppaal tool suite in order to generate offline test cases using coverage criteria for timed models. More recently, [START_REF] Bertrand | Off-line test selection with test purposes for non-deterministic timed automata[END_REF] proposes a formal framework permitting to use Test Purpose and non-deterministic Timed Automata thanks to a determinization algorithm.

Remote testing. These works introduce conformance relations and test selection algorithms based on synchronous test execution algorithms. However, in the untimed setting, [START_REF] Jard | Remote testing can be as powerful as local testing. Formal Desciption Techniques and Protocol Specification[END_REF] and [START_REF] Simao | Generating asynchronous test cases from test purposes[END_REF] point out the fact that synchronous execution of tests cases is not realistic when there is a significant distance between testers and SUTs. Under this remoteness assumption, the adequate communication mode should be asynchronous. [START_REF] Jard | Remote testing can be as powerful as local testing. Formal Desciption Techniques and Protocol Specification[END_REF] considers that SUTs and testers communicate via input and output queues, and asynchronous points of control of observation (PCOs). [START_REF] Jard | Remote testing can be as powerful as local testing. Formal Desciption Techniques and Protocol Specification[END_REF] also shows that simply using logical stamps permits to obtain the "same power" of testing than in a synchronous environment. In a more general way, [START_REF] Noroozi | Synchronizing asynchronous conformance testing[END_REF] proposes a study revisiting asynchronous testing and showing possibilities (or not) to synchronize asynchronous testing.

Usually, the works done on this topic consider this as a "distributed" testing, implying several entities in a "system" of components. In this case, most effort is done for solving the problem of relative order between events induced by the communication process without state space explosion. [START_REF] Henniger | On test case generation from asynchronously communicating state machines[END_REF] proposes a test generation framework using several Input Output State Machines (IOSM) and perfect FIFO queues between them. Then the author uses the Prime Event Structure in order to fix the problems of interleaving in the test generation process. Still using queues, but with Input Output Transition Systems (IOTS), [START_REF] Simao | Generating asynchronous test cases from test purposes[END_REF] proposes a method to generate sound test cases with test purposes. They apply a transformation of the test purpose allowing to consider all possible distortions induced by the queues. The problem of interleaving is also addressed in [START_REF] De León | Conformance relations for labeled event structures[END_REF] where authors focus on testing of concurrent systems. They propose to use Labeled Event Structures and partial order semantics in order to handle lightly concurrency aspects in the conformance relation. [START_REF] Hierons | Using time to add order to distributed testing[END_REF] proposes to add local clocks in each component and timestamps directly included in the exchanged messages. They propose different strategies depending on assumptions regarding how the clocks relate and give adapted conformance relations.

Contributions. The related works described above provide testing techniques for untimed systems. To the best of our knowledge, there is no explicit work that considers remote testing of timed specifications. Our contribution is two-fold. Firstly and based on a real example, we show how remote testing can be performed by modelling the communication channels with processes that delay the actions and synchronize with the SUT and its environment. We discuss the drawback of this general approach. Then, after considering timed asynchronous behaviours, we provide a ∆-testability criterion ensuring remote testing with the same detecting properties as local one.

The paper is organised as follows. Section 2 recalls well-known concepts of the model-based testing theory with TIOA. In Section 3, we address the challenges for the remote testing. We present the disadvantages of using asynchronous timed traces in general. Asynchronous semantics described the observations of a remote tester. Section 4 relates observed traces with the traces of the implementation. We define the ∆-testable criterion and present some interesting properties. The remote testing framework with Uppaal-TIGA is described in Section 5 and it is followed by a case study in Section 6.

The tioco-based Testing Theory

The tioco-testing theory is based on the representation of the specifications and the implementations with deterministic TIOA. Let us now present formal notations and concepts for the tioco-testing theory that we extend later for remote testing.

Timed word, timed sequence, and timed trace. In the sequel, R ≥0 denotes the set of non negative real-numbers that we will often call delays. A timed word over an alphabet of actions Γ is an element

w = w 1 • w 2 • . . . • w n of (R ≥0 ∪ Γ ) * . We define w[i] = w i and w[i..j] = w i • w i+1 • . . . • w j-1 • w j ,
and |w| = n denotes the length of w. We consider the causal/dependency relation between the actions in w and we say that w j depends on w i when i < j and we write w i ≺ ρ w j . The timed word w is a timed sequence if the projection of w over R ≥0 is empty or an increasing sequence of real-numbers i.e ∀0 ≤ i ≤ j ≤ |n| such that w i , w j ∈ R ≥0 , it holds that w i ≤ w j . A timed sequence is called a timed trace if it is a sequence of timestamped actions followed with a delay i.e it belongs to (R ≥0 × Γ ) * × R ≥0 . We will consider that the behaviours of real-time systems can be described with timed traces. Each delay in a timed sequence refers to the time that has elapsed since the system started.

Input/Output Timed Transition Systems (IOTTS)

Definition 1 (IOTTS). An input/output timed transition system (IOTTS) is a tuple S = S, s 0 , I, O, Λ, M where S is the set of states, s 0 is the initial state, I is a finite set of input actions, O is a finite set of output actions, Λ is a finite set of silent actions,

M ⊆ S × (I ∪ O ∪ Λ ∪ R ≥0 ) × S is the set of moves. We will write s α -→ s ′ with α ∈ (I ∪ O ∪ Λ ∪ R ≥0 ) to represent a move (s, α, s ′ ) ∈ M .
Moreover, we require the following standard properties for IOTTS : time-Determinism

( if s d -→ s ′ and s d -→ s ′′ with d ∈ R ≥0 , then s ′ = s ′′ ) , 0-Delay (s 0 -→ s), additivity (if s d -→ s ′ and s ′ d ′ -→ s ′′ with d, d ′ ∈ R ≥0 , then s d+d ′ ---→ s ′′ ), continuity (if s d -→ s ′ , then for every d ′ and d ′′ in R ≥0 such that d = d ′ + d ′′ , there exists s ′′ such that s d ′ -→ s ′′ d ′′ -→ s ′
). We denote by IOTTS(I, O, Λ), the class of IOTTS of which the input actions, the output actions and the silent actions belong to I, O and Λ, respectively. For S ∈ IOTTS(I, O, Λ), we define Act(S) = I ∪ O ∪ Λ.

3

Notations. In the sequel we write s α -→ with α ∈ Act(S) ∪ R ≥0 when there exists s ′ ∈ Q such that s α -→ s ′ . We write s α1.α2....αn -------→ s ′ with α i ∈ Act(S) ∪ R ≥0 when there exists s 1 , s 2 , . . . s n-1 ∈ S such that s

α1 -→ s 1 α2 -→ s 2 → • • • → s n-1 αn --→ s ′ .
Executions and timed traces. A run of S starting at s ∈ S, is a finite sequence π = s.(α i .s i ) i=1..n ∈ S × ((Act(S) ∪ R ≥0 ) × S) * such that s α1 -→ s 1 and s i αi -→ s i+1 . We denote Runs(s) the set of runs of S starting from s and Runs(S) = Runs(s 0 ). The execution sequence of π is the sequence Seq(π) = α 1 .α 2 . . . . .α n ∈ ((Act(S)∪ R ≥0 ) * , and we naturally extend the notation with Seq(s) = {Seq(π) | π ∈ Runs(s)} and Seq(S) = Seq(s 0 ). As usual, a move s α -→ s ′ with a ∈ Act(S) means that s ′ is reached when the action a is executed on s (discrete move). A move s d -→ s ′ with d ∈ R ≥0 means that the state s ′ is reached after d time units has elapsed from s; so d is interpreted as the time distance between s and s ′ (time elapse).

The environment cannot observe the executions of silent actions in Λ. Moreover delays in executions are time distances between states. A timed trace corresponding to an execution is a timed sequence consisting of time-stamps and visible actions and such that the time-stamps indicate the dates of occurrences of the actions. Given an execution sequence ρ = (α i ) i=1..n ∈ (Act(S) ∪ R ≥0 ) * , the timed trace associated with ρ is denoted ttrace(ρ) and it is defined by ttrace(ρ) = obs(0, ρ) where Complete and deterministic IOTTS. We say that S is deterministic if it has no silent transition and s ′ = s ′′ whenever there exists s, α ∈ Act(S), s α -→ s ′ and s α -→ s ′′ . IOTTS S is input-complete if all the inputs can be executed (observed) in each state.

obs : R ≥0 × (I ∪ O ∪ Λ ∪ R ≥0 ) * → (R ≥0 × (I ∪ O)) * × R ≥0

Timed Input/Output Automata (TIOA)

A clock is a real-valued variable. Let X denote a set of clocks. A (clock) valuation over X is a function v : X → R ≥0 that assigns a non negative real value to each clock. x = 1, ?a2, {x}

x = 6, !b1, {x} x = 7, !b2, {x} x = 1, !b3, {x} x = 2, !b4 x = 2, ?a3, {x} x = 2, !b1 x = 0, ?a1, {x} x ≥ 0, !b1 (a) Spec n0 n1 n2 n3 n4 n5 n6 n7 n8 n9 x = 3, ?a1 x = 2, ?a1 x = 4, ?a2, {x} x = 6, !b1, {x} x = 7, !b2, {x} x = 1, !b3, {x} x = 2, ?a3, {x} x = 1, !b2 x = 2, !b1 (b) Imp 1 n0 n1 n2 n3 n4 n5 n6 n9 x = 3, ?a1 x = 4, ?a2, {x} x = 6, !b1, {x} x = 7, !b2, {x} x = 1, !b3, {x} x = 2, ?a3, {x} x = 2, !b1 (c) Imp 2 ℓ0 ℓ1 ℓ2 ℓ3 ℓ4 ℓ6 ℓ5 ℓ7 ℓ8 ℓ9 ℓ10 x = 5, ?a1, {x} x = 0, !b5, {x} x = 1, ?a2, {x} x = 6, !b1, {x} x = 7, !b2, {x} x = 1, !b3, {x} x = 0, !b4 x > 4, ?a3, {x} x = 2, !b1 x > 4, ?a1, {x} x ≥ 0, !b1 (d) 2-testable TIOA n0 n1 n2 n3 n4 n5 n6 n7 n9 n10 x = 3, ?a1 x = 4, ?a2, {x} x = 3, !b5, {x} x = 6, !b1, {x} x = 7, !b2, {x} x = 1, !b3, {x} x = 2, ?a3, {x} x = 2, !b1 x ≥ 0, !b1 (e) Imp 3 n0 n1 n2 n3 n4 n5 n6 n9 x = 3, ?a1 x = 4, ?a2, {x} x = 6 !b1, {x} 5 ≤ x ≤ 7 !b2, {x} x = 1 !b3, {x} x = 2, ?a3, {x} x = 2, !b1 (f) Imp 4

Fig. 1: Models of one specification and four implementations

The set of valuations over X is denoted by R X ≥0 . As usual, we consider two operations on valuations: the reset of the clocks and the elapse of the time. Given a valuation v, a real number t ∈ R ≥0 and a subset of clocks Y ⊆ X, the valuation v[Y := 0] is obtained from v by resetting every clock in Y and the valuation v + t increases by

t the value v(x) of each clock x ∈ X. Formally, v[Y := 0](x) = 0 when x ∈ Y , otherwise v[Y := 0](x) = v(x); and (v + t)(x) = v(x) + t.
The valuation 0 assigns the zero value to every clock. A clock constraint over X is a boolean combination of equations of the form n x where n ∈ Q is a rational number, ∈ {<, >, =, ≤, ≥} and x ∈ X. We will denote by C(X) the set of clock constraints over X. The truth value of a clock constraint is computed w.r.t a valuation and this notion is standard. We say that v ∈ R X ≥0 satisfies g ∈ C(X) and we write v |= g if g evaluates to true w.r.t to v.

Definition 2 (TIOA). A timed input/output automaton (TIOA) is a tuple

A = L, ℓ 0 , I, O, Λ, X, E where L is a finite set of locations, ℓ 0 is the initial location, X is a finite set of clocks, I is a finite set of input actions, O is a finite set of output actions, Λ is a finite set of silent actions, E ⊆ L × (C(X) × (I ∪ O) × 2 X ) × L is the set of edges. Definition 3 (Semantics of TIOA). Let A = L, ℓ 0 , I, O, Λ, X, E be a TIOA. The semantics of A is the IOTTS(I, O, ∅) A = S A , s 0 A , I, O, ∅, M A where: S A = L × R X ≥0 is the set of states of A, s 0 A = (ℓ 0 , 0) is the initial state of A, I is the set of inputs of A, O is the set of outputs of A, M A ⊆ S A × (I ∪ O ∪ R ≥0 ) × S A is the set of moves of A defined such that: ((ℓ, v), d, (ℓ, v + d)) for every d ∈ R ≥0 , (ℓ, v) ∈ S A ; and ((ℓ, v), a, (ℓ ′ , v[Y := 0])) whenever (ℓ, g, a, Y, ℓ ′ ) ∈ E and v |= g.
We define TTraces(A) = TTraces( A ) and A after σ = A after σ with σ ∈ TTraces(A). --------→ ℓ 1 is passed provided that x equals 3, the input ?a 1 is received and x set to 0 just after the passing of the edge. An execution of Spec is π 1 = (ℓ 0 , 0)

Deterministic TIOA. We say that A is deterministic if A is deterministic. Similarly, A is input-complete if A is input-complete.
0.5 --→ (ℓ 0 , 0.5) 2.5 --→ (ℓ 0 , 3) ?a1 --→ (ℓ 1 , 0) 0.7 --→ (ℓ 1 , 0.7) 0.3 --→ (ℓ 1 , 1) ?a2 --→ (ℓ 2 , 0) 2 -→ (ℓ 2 , 2) 1 -→ (ℓ 2 , 3) 4 -→ (ℓ 2 , 7) !b2 --→ (ℓ 4 , 0) 1 -→ (ℓ 4 , 1) !b3 --→ (ℓ 5 , 0) 1 -→ (ℓ 5 , 1) 1 -→ (ℓ 5 , 2) ?a3
--→ (ℓ 6 , 0), and the execution sequence associated with

π 1 is Seq(π 1 ) = 0.5 • 2.5 • ?a 1 • 0.7 • 0.3 • ?a 2 • 2 • 1 • 4 • !b 2 • 1 • !b 3 • 1 • 1 • ?a 3 and the associated timed trace is TTraces(Seq(π 1 )) = (3 • ?a 1 ) • (4 • ?a 2 ) • (11 • !b 2 ) • (12 • !b 3 ) • (14 • ?a 3 ) • 0. We have that Spec after (3 • ?a 1 ) • (4•?a 2 )•(11•!b 2 )•0 = {(ℓ 4 , 0)}, Spec after (3•?a 1 )•(4•?a 2 )•(10•!b 1 )•0 = {(ℓ 3 , 0)}, out(Spec after (3 • ?a 1 ) • (4 • ?a 2 ) • 9) = R ≥0 , out(Spec after (3 • ?a 1 ) • (4 • ?a 2 ) • 10) = {!b 1 } ∪ R ≥0 and out(Spec after (3 • ?a 1 ) • (4 • ?a 2 ) • 11) = {!b 2 } ∪ R ≥0 .

The Relation tioco and Synchronous Testing

As usual, the SUT is represented with an input-complete TIOA. We recall the tioco conformance relation definition, a common extension of ioco. In the following, we use this relation for conformance between the SUT and the specification. Definition 4 (tioco). Let S and I be in TIOA(I, O) where I is input-complete.

I tioco S iff ∀σ ∈ TTraces(S), out(I after σ) ⊆ out(S after σ) Example 2. Consider Spec and the four implementations depicted in Figure 1. We can verify that Imp 1 conforms with Spec even though Imp 1 can receive ?a 1 when x = 2. The same, Imp 2 tioco Spec. But Imp 3 does not because out(Imp

3 after (3•?a 1 )) = {!b 5 } ∪ R ≥0 and out(Spec 1 after (3•?a 1 )) = R ≥0 and Imp 4 does not conform with Spec because out(Imp 4 after (3•?a 1 ) • (4•?a 2 ) • 9) = {!b 2 } ∪ R ≥0 whereas out(Spec after (3•?a 1 ) • (4•?a 2 ) • 9) = R ≥0 .
An on-line tester for an SUT simulates the specification either by sending an input to the SUT or by letting the time elapses, while checking that the outputs emitted by the SUT are expected. Upon the reception of an unexpected output (outputs that are not specified or that arrive at bad instants), the tester emits the verdict fail indicating that the SUT does not conform to the specification. The communications between the tester and the SUT are synchronous meaning that the tester blocks upon transmitting an input to (receiving an output from) the implementation. There is no latency. Consequently, the time instant at which the tester sends available inputs or receives expected outputs should be exactly those described by the specification. Local and synchronous testers control the tests i.e each time a tester observes an output, that output depends on all the inputs it has sent before. The controllability of the test is an important property giving the possibility to lead the SUT into a particular situation.

Introduction to Remote Testing and Challenges

The main idea is that the SUT and the tester are not located at the same site and communications may be delayed. Fig. 2 illustrates our framework for remote testing. The model is centered around a 2F IF O(⊲⊳, ∆) architecture that consists of:

1. One FIFO for each direction of the communication between the SUT and the tester. 2. A communication latency bounded by ∆. The symbol ⊲⊳ stands for either ≤ or =.

Remote Testing Challenges

Remote test cases are different from the test cases designed for local testers. When the transmission of an input depends on the reception of an output, a remote tester should not wait to receive the output before sending the input since there is a latency. The experimentation with Uppaal-TIGA highlights this point. Let us now consider simple specification models to provide a theoretical point of view of remote testing. Remote testing introduces two news challenges: managing the signal propagation delay between the tester and the SUT; and managing the input/output interleaving caused by the asynchronous communication: the actions are not always received in the order they are transmitted and received.

In the next subsection we study the asynchronous traces and we will study the impact of the propagation delay and the interleaving on the tests cases.

Testing with Asynchronous Traces

We introduce the asynchronous semantics for TIOA and we present results on using asynchronous traces for testing. The asynchronous semantics for TIOA takes into account the queues and the latency; it describes the influence of the latency on the transmissions and the receptions of the actions.

Definition 5 (Asynchronous semantics for TIOA). Let A = L, ℓ 0 , I, O, ∅, X, E be a TIOA(I, O) with no silent action. Let ⊲⊳∈ {≤, =} and ∆ ∈ N. The asynchronous semantics for A is an

IOTTS(I, O, Λ I∪O ), [A] ⊲⊳∆ = (L×R X ≥0 )×(R ≥0 ×(I∪O)) * ×(R ≥0 ×(I∪O)) * , (ℓ 0 , 0), I, O, Λ I∪O }, M ⊲⊳∆ where Λ I∪O = {τ a | a ∈ I ∪ O}
is the set of silent actions. An asynchronous state is of the form ((ℓ, v), p, q) where p and q are input and output queues respectively. The set of asynchronous moves, M ⊲⊳∆ is defined by the following five rules: ((ℓ, v), p, q) ?a -→ ((ℓ, v), p.(0•?a), q) (r1) ((ℓ, v), (δ•?a).p, q)

τa -→ ((ℓ ′ , v[Y := 0]), p, q) ℓ g,?a,Y ----→ ℓ ′ ∧ v |= g ∧ δ ⊲⊳ ∆ (r2) ((ℓ, v), p, q) t -→ ((ℓ, v + t), p + t, q + t) (r3) ((ℓ, v), p, (δ•!b).q) !b -→ ((ℓ, v), p, q) δ ⊲⊳ ∆ (r4) ((ℓ, v), p, q) τ b -→ ((ℓ ′ , v[Y := 0]), p, q.(0•!b)) ℓ g,!b,Y ----→ ℓ ′ ∧ v |= g (r5)
The rules r1 and r2 (resp r5 and r4) are dual and they correspond to the transmission and the reception of an input (resp. output). The rule r3 corresponds to the time elapsing. The time elapsing operation on a queue is defined by ((δ • a).p) + t = (δ + t, a).(p + t).

Notice that [A] ⊲⊳∆ is input-complete because the transmissions of the inputs do not require to check the clock constraints. The receptions of the pending inputs require to check for the validity of clock constraints. The length of each queue is unbounded.

Based on [A] ⊲⊳∆ , we can define asynchronous runs, asynchronous execution sequences and asynchronous timed traces in ATTraces ⊲⊳∆ (A) = TTraces( [A] ⊲⊳∆ ).

On asynchronous tioco. Given an implementation I and a specification S modelled with a TIOA(I, O), one could try to adapt the relation tioco based on the asynchronous semantics. Such an adaptation has been studied in [START_REF] Jard | Remote testing can be as powerful as local testing. Formal Desciption Techniques and Protocol Specification[END_REF] for untimed systems. A quick adaptation of tioco that we call atioco ⊲⊳∆ can be defined as follows:

I atioco ⊲⊳∆ S iff ∀σ ∈ ATTraces ⊲⊳∆ (S), out(( [I] ⊲⊳∆ ) after σ) ⊆ out(( [S] ⊲⊳∆ ) after σ).
Designing a remote testing algorithm as a simple adaptation of the local and synchronous testing algorithm with asynchronous traces can be the source of differences between local testing verdicts and remote testing verdicts. The following example highlights three relevant problems: the non preservation of conformance, the permissiveness and the lack of control during the test. Permissiveness. The relation atioco ⊲⊳∆ is permissive in the way that there exists an implementation I of a specification S, a delay ∆ and ⊲⊳∈ {<=, =} such that ¬(I tioco S) but I atioco ⊲⊳∆ S. For example, consider Fig. 1 and 2F IF O(=, 2). We check that Imp 3 atioco ⊲⊳∆ Spec because out(

[Imp 3 ] ⊲⊳∆ after (1•?a 1 )•2) = {!b 5 }∪R ≥0 and out( [Spec] ⊲⊳∆ after (1•?a 1 )• 2) = {!b 5 } ∪ R ≥0 .
But, as we discussed earlier, ¬(Imp 3 tioco Spec).

Non preservation of conformance. The relation atioco ⊲⊳∆ does not preserve the conformance in the way that there exists an implementation I of a specification S, a delay ∆ and ⊲⊳∈ {<=, =} such that ¬(I atioco ⊲⊳∆ S) but I tioco S. For example, consider Fig. 1 and

2F IF O(=, 2). Because out( [Imp 1 ] ⊲⊳∆ after (0•?a 1 )• 1) = {!b 2 } ∪ R ≥0 and out( [Spec] ⊲⊳∆ after (0•?a 1 ) • 1) = R ≥0 it comes that ¬(Imp 1 atioco ⊲⊳∆ Spec). But we can check that Imp 1 tioco Spec.
Controllability of the test. We say that a specification is controllable if in the case a tester observes an input, this means that any output it has sent before has already been received by the implementation. When performing remote testing, signal propagating delay needs to be managed, especially when the tester sends the inputs early and receives the outputs lately. An output received after the transmission of an input it does not depend on forces the tester to change the test case it was executing. For example, consider the specification in Figure 1, and assume that the implementation is the same as the specification. Also assume that we want to test the path up to ℓ 7 through ℓ 6 . For that purpose a tester may observe the asynchronous timed trace

σ ′ 1 = (1•?a 1 ) • (2•?a 2 ) • (12•?a 3 ) • (13•!b 2 ) • (14•!b 3 ) • 0.
This trace means that the tester sends ?a 3 before it receives !b 3 . But, the implementation can change the test purpose by sending !b 4 at the time 13. So a tester should remind that it already has sent ?a 3 and it should pursue the test by following a new trajectory where ?a 3 follows !b 4 .

It is not reasonable that testing verdicts vary depending on the distance and the communication mode between tester and implementation. In order to return correct verdict whatever the distance and the communication mode, we can equip the implementations with an additional mechanisms, like logical stamping mechanism [START_REF] Jard | Remote testing can be as powerful as local testing. Formal Desciption Techniques and Protocol Specification[END_REF], that will help the testers to recover the causal order of the interleaved actions. But, that mechanism cannot allow the remote testers to control the test. order: this happens when inputs and outputs interleave in the communication channels. We intend to characterize remote observations that may lead to action interleaving. Thanks to the timing information, we introduce ∆-testable specifications of which asynchronous traces can be used for remote testing without using costly mechanisms. 14•?a 3 ).0. We remark that ?a 3 occurs before !b 2 in ttrace(ρ) but !b 2 occurs before ?a 3 in ttrace(apply(ρ)) which is a timed traces of Spec.

4. Let ρ = 1•?a 1 • 1•?a 2 • 1 • τ a1 • 1 • τ a2 • 5 • 2 • τ b2 • 1 • τ b3 • 0•?a 3 • 1•!b 2 • 0.6 • 0.4•!b 3 • 0 • τ a3 be in ATTraces ⊲⊳∆ (Spec).
(ρ) = 1•1•1?a 1 1•?a 2 •5•2•!b 2 •1•!b 3 •0•1•0.6•0.4•0•?a 3 . We can also compute ttrace(ρ) = (1•?a 1 ) • (2•?a 2 ) • (12•?a 3 ) • (13•!b 2 ) • (14•!b 3 ) • 0 and ttrace(apply(ρ)) = (3•?a 1 ) • (4•?a 2 ) • (11•!b 2 ) • (12•!b 3 ) • (
The causal order of the action in an asynchronous timed trace may not be respected by a remote implementation. The order of execution of two actions may be inverted by the remote SUT. For example this situation happens in asynchronous sequence ρ that contains a pattern1 of the form

• • • ρ[i] • • • ζ ρ[j] • • • ζ ρ[i] • • • ρ[j] • • • where ρ[i]
and ρ[j] are visible actions and i < j. When such a situation happens, we say that ρ is action-interleaving. For example, ρ presented in Example 4 is action-interleaving.

Definition 6. A regular sequence ρ ∈ Seq( [S] ⊲⊳∆ ) is action interleaving if there exists i, j s.t ρ[i] ≺ ρ ρ[j] and ζ ρ[j] ≺ ρ ζ ρ[i] .
Proposition 1 states that the causal order of the actions in a non interleaving asynchronous trace is preserved at the implementation site. Let us denote by Proj vis (ρ) the projection of ρ over I ∪ O ∪ R ≥0 . Given a state s = ((l, v), p, q) of [A] ⊲⊳∆ , let us denote by p(s) = p and q(s) = q the content of the input and output queues at s. Proposition 1. Let ρ = (α i ) i=1..n in Seq( [S] ⊲⊳∆ ) be a regular execution sequence. ρ is not action-interleaving iff Proj vis (apply(ρ)) = Proj vis (ρ). Proposition 2. Let ρ = (α i ) i=1..n ∈ Seq( [S] ⊲⊳∆ ) be a regular asynchronous execution sequence. ρ is action-interleaving iff p(s) and q(s) are non empty for some state s,

some k ≤ n such that s 0 ρ[1..k]
----→ s.

∆-Testable TIOA

We provide a ∆-testability criterion permitting to test remotely while preserving properties of local testing. Action-interleaving does not occur in ∆-testable specifications.

Definition 7 (∆-testability). Let A ∈ TIOA(I, O) and σ ∈ TTraces(A) such that σ = (t i • a i ) i=1..n .t n+1 . The timed trace σ is ∆-testable if, -either n = 0, -or (t i • a i ) i=1..n-1 is ∆-testable and a n ∈ O, -or (t i • a i ) i=1..n-1 is ∆-testable and if a n ∈ I, then for every t b ∈ R ≥0 , every b ∈ O, and every k ∈ [1..n -1] such that !b ∈ out( A after σ[1..k] • t b ), it holds that t n -t b > 2∆. A is ∆-testable if every σ ∈ TTraces(A) is ∆-testable.
Example 5. Spec is 1-testable. Spec is not 2-testable. Indeed, one can consider the subspecification rooted at ℓ 4 . The delay between !b 4 and ?a 3 equals 1 and it is not greater than 2 × ∆ = 4. The specification obtained in Fig. 1d that is obtained from Spec by changing some constants is 2-testable.

The causal order of the observed actions is the same as the causal order of the actions executed by the remote implementation when the specification is ∆-testable.

Proposition 3. Let A be a TIOA(I, O). If A is ∆-testable then Seq( [A] ⊲⊳∆ ) contains no action-interleaving sequence.
Putting Proposition 2 and Proposition 3 together, we get Proposition 4.

Proposition 4. Let A be a TIOA(I, O). Let s, ρ ∈ Seq( [A] ⊲⊳∆ ) such that s 0 ρ -→ s. A is ∆-testable iff p(s) is non empty implies q(s) is empty.
According to Proposition 4, ∆-testability implies that at most one queue is non empty at every reachable state. However, ∆-testability does not guarantee that the sizes of the queues are bounded. A fast environment can increase the size of the input queue by sending repetitively the inputs faster than the latency.

We can show that ∆-testable specifications are controllable. Indeed, ∆-testable specifications have no action-interleaving sequences. Consequently a regular asynchronous timed trace ρ is such that ρ

[i] ≺ ρ ρ[j] iff ζ ρ[i] ≺ ρ ζ ρ [j] for every 1 ≤ i, j ≤ |ρ|. W.l.o.g, assume that ρ[i] ∈ O and ρ[j] ∈ I. Then, ζ ρ[i] ≺ ρ ρ[i], ρ[j] ≺ ρ ζ ρ[j]
. Since the specification is ∆-testable, the delay between ζ ρ[i] and ζ ρ[j] is strictly greater than 2∆. But since the delay between ρ[k] and ζ ρ[k] with k ∈ {i, j} is bounded with ∆, we get the delay between ρ[i] and ρ[j] is strictly positive. This implies that the output ρ[i] is observed before the input ρ[j]. This means that the outputs transmitted earlier are received before the transmission of new inputs. Thus, each observed output depends on input transmitted earlier and the specification is controllable.

In brief, ∆-testability criterion takes advantage of the timing information that are not available in untimed models. We claim that if the specification is ∆-testable then, the asynchronous execution of the synthesized test cases is as simple as the synchronous execution, the tioco conformance is preserved and the tester can control the test.

Remote testing Framework with Uppaal-TIGA

In this section we present our general framework using Uppaal-TIGA with partial observability [START_REF] Cassez | Timed control with observation based and stuttering invariant strategies[END_REF]. We model the SUT, the communication channels, and the actual tester as a timed game with the twist that only some states or clocks are visible. The tester changes its states according to the output from the SUT (via the delayed FIFOs) and the goal is that given a test objective expressed as a formula (using an extra observer automaton or not), find a strategy using the actions of the tester and a fixed set of observations to reach that objective. This matches the situation that the tester can only observe the delayed output from the SUT and cannot see its state. The framework is an extension of [START_REF] David | Timed testing under partial observability[END_REF].

Modelling Pattern. Fig. 2 presents our modelling pattern. The originality of the model is how the FIFOs are encoded. We want to transmit a message with optional data with a delay that may be non-deterministic. In general, this may change the order of the outputs of the "FIFO" if the delays overlap. Each cell of the FIFO buffer is modeled as an automaton with its own identifier (id) as shown in Fig. 2. Only the automaton with the right identifier that matches the head of the FIFO (a global variable) reacts to the communication. The head and tail of the FIFOs are simple counters managed by the automata. Each automaton has its own clock to delay the output of the incoming message. We rename the channels to do the delayed transmission. For our light controller example of Section 6, grasp becomes setGrasp, and release setRelease.

Then we compose the SUT in parallel with the FIFOs and the tester. The tester automaton is free to generate outputs with possibly some constraints. The next step is to solve the game to decide which outputs should be generated, and when.

Solving the Game. To generate the test, Uppaal-TIGA solves a two-player game between the tester and the implementation. The implementation (together with the FIFO) plays uncontrollable transitions and the tester plays controllable transitions. In addition, observations together with the test purpose are specified. To play the game an action label is associated with the transitions and the tester plays one given controllable action until its observation changes. In the meantime, the implementation can play its uncontrollable transitions. It is only when an observation changes that the tester can change its action. We refer to [START_REF] Cassez | Timed control with observation based and stuttering invariant strategies[END_REF] and [START_REF] David | Timed testing under partial observability[END_REF] for more details. The result is that Uppaal-TIGA will find a strategy for the tester to fulfil the test purpose under the specified observations iff there exists such a strategy. POCO Conformance. Uppaal Tiga with partial observability [START_REF] David | Timed testing under partial observability[END_REF] assumes poco P conformance relation constructed similarly to tioco, except that in addition to outputs the observations also contain a partial information about the system state defined by a set of predicates P . In theory the discrete changes in the partial state observation can be identified as special outputs and therefore emulated by tioco. In general, poco P is most useful to relate to the SUT as a continuous observation of its partial state which might be difficult to achieve in practice. In this paper we assume that only the state of environment (the model of test assumptions or a tester) is observable and thus only observable I/O is communicated with the black-box SUT and media and therefore tioco is sufficient for our purposes.

Light Controller Example

To apply our remote testing framework we consider the example of a light controller [START_REF] Kim | Uppaal TRON User Manual[END_REF]. A user can grasp or release a trigger rod. Grasping and holding makes the intensity of the light vary. Grasping and releasing have the effect of switching off or on to the previous light level.

Encoding Delayed Communications. We specialize the FIFOs presented in Section 3 to send grasp and release to the SUT, and level together with a value to the tester. Fig. 3a shows the automaton used to delay grasp and release, and Fig. 3b the one to delay level with the value of the light level. The pattern for both automata is that upon synchronization on a given channel, a transition is taken to a state where the delay occurs and then a renamed output is produced. Data (Fig. 3b) may be stored and forwarded thanks to a local buffer. SUT, Tester, and Test Purpose. The light controller has an interface that receives the grasp and release commands. It controls two components to respectively dimmer or switch on or off the light. The actual details of the SUT are not important here since we are doing black-box testing. The internal communication is not visible to the tester or the FIFOs. The tester is an automaton that can generate grasp or release at any time. We can constrain the outputs and to illustrate this, we use two types of testers to generate test strategies. Our testers are shown in Fig. 4a and4b. They restrict the tests to one or two grasp and release. The test purpose is a monitor automaton put in parallel together with the tester automaton to specify interesting sequences of outputs that we want to observe. Fig. 4c specifies that the light level should increase to its maximum level and then decrease monotonically. Fig. 4d specifies that the light level should increase monotonically to its maximum level and then be switched off. Playing the Game to Generate Tests. To generate the tests, Uppaal-TIGA solves a twoplayer game between the tester and the implementation. In the automata shown for the tester, purpose, and the FIFO, the uncontrollable transitions played by the implementation are dashed. The controllable transitions played by the tester are not dashed. In addition, we need to specify what is observable, which is done together with the formula giving the test purpose.

We specify the following test purposes: Purpose 1 specifies to turn the light on to its maximum intensity level without having a buffer overflow in the FIFO 2 . In addition, the user must have released the trigger. We do not need an extra automaton for this purpose. To achieve this, the user has a clock x that can be reset (Fig. 4a or 4b) and can observe if x ∈ [0, 1[ or not. In addition, overflow and the released state together with the maximum light intensity are observable 3 .

Purpose 2 specifies that the goal state of our monitor automaton should be reached while avoiding overflow or the error state in the monitor. To do so the user can observe if his clock x ∈ [0, 2[ or not, if the light is at its maximum level (or not), or if it is switched off (or not). This can be checked for both our purpose automata, though we need the user of Fig. 4b to fulfil the goal of the purpose of Fig. 4d.

It is important to notice that the observations that are given are only from the tester's side and we do not see the internal state of the SUT, thus respecting the black-box testing principle. We show one strategy generated in a few second 4 for purpose 2 with a deterministic communication delay of 4 time units. We sanitized and minimized it (the raw output has 16 states).

∆-Testability

The model is general and does not enforce minimal delays between inputs and outputs. We can constrain the environment model or add another purpose automaton to constrain the strategy. For example, if the delay between grasp and release exceeds the longest duration for registering a touch, then there is no strategy to satisfy purpose 2. This delay is the ∆ of our example.

Conclusion

We addressed conformance testing of remote SUTs specified with timed input/output automata. Our testing architecture is composed of two queues with a communication latency threshold. Testers and SUTs communicate in an asynchronous way. We introduced the ∆-testability criterion allowing remote testing to be as powerful as local testing without any additional mechanism. The ∆-testability criterion ensures that input/output interleaving never occurs, controllability of the test and a remote verdict similar to local one. Then we presented a test selection approach with the partial observability timed game solver Uppaal-TIGA. The method has consisted in modelling the queues with new TIOA that receive and delay the actions. Then the test generation was reduced to synthesis of winning strategies in the game provided that the sizes of the queues are bounded. However the limitation of the size of the queue restricts the number of consecutive inputs/outputs the tester/SUT may send within the period of the latency threshold. Moreover, using one clock per cell leads to exponential blow up during the generation of the test cases whether the latency is deterministic or not.

We believe that testing ∆-testable criterion can be performed in a more efficient way and with less constraints on the size of the queues. Promising results hold in case of deterministic latencies. Further works include the design of dedicated testing algorithms for ∆-testable specifications and the automatic verification of the ∆-testability criterion.

  is a function that removes silent action from execution actions and that computes the date of the occurrence of the input and output actions. We propose the following recursive definition of obs: obs(d, ε) = d with d ∈ R ≥0 ; then obs(d, α.w) equals obs(d + α, w) if α ∈ R ≥0 , otherwise it equals obs(d, w) if α ∈ Λ, otherwise it equals d.α.obs(d, w) if α ∈ (I ∪ O). In the sequel, TTraces(S) = {ttrace(ρ) | ρ ∈ Seq(S)} denotes the set of timed traces of S. Note that since σ = (δ i • a i ) i=1..m .δ m+1 ∈ TTraces(S) is a timed sequence, it implies that δ i ≤ δ i+1 for every i ∈ [1..m]. Given a timed trace σ ∈ (R ≥0 × (I ∪ O)) * × R ≥0 , we consider as usual the after operator: s after σ = {s ′ ∈ S | ∃ρ ∈ Seq(s ′ ) s.t s ρ -→ s ′ ∧ σ = ttrace(ρ)} represents the set of states that can be reached from s and after observing the behaviour σ. Then we define elapse(s) = {δ ∈ R ≥0 | s δ -→} (Notice that elapse(s) = R ≥0 when there is no restriction on the elapse of the time in s), S after σ = s 0 after σ; and out(s) = {a ∈ O | ∃ρ ∈ Seq(s) s.t ttrace(ρ) = (0 • a) • 0} ∪ elapse(s) denotes the set of delays augmented with the set of outputs that can be observed from s without any delay, possibly preceded by the execution of silent actions. Illustrations of all these notations can be found in Example 1.

Example 1 .

 1 The TIOA Spec in Fig.1ais composed of a single clock x, the inputs are ?a 1 , ?a 2 , ?a 3 and the outputs are !b 1 , !b 2 , !b 3 , !b 4 , !b 5 . The edge ℓ 0 x=3,?a1,{x}

Fig. 2 :

 2 Fig.2:The modeling pattern and how our example of the light controller is modeled.

Example 3 .

 3 Consider the specification Spec in Fig. 1a and assume that the latency is exactly 2 time units. If the tester wants that SUT receives a 1 at global time 3, it should send a 1 at time 1. When SUT sends b 2 at time 11, the tester receives it at time 13. etc. So a tester shall observe the timed trace σ ′ 1 = (1•?a 1 )•(2•?a 2 )•(12•?a 3 )•(13•!b 2 )•(14•!b 3 )•0 and the SUT executes the timed trace σ 1 = (3•?a 1 ) • (4•?a 2 ) • (11•!b 2 ) • (12•!b 3 ) • (14•?a 3 ).0. Note that the outputs !b 2 and !b 3 follow ?a 3 in σ ′ 1 contrary to the trace σ 1 ∈ TTraces(Spec). This means that the tester does not wait for !b 2 and !b 3 before sending ?a 3 despite the fact that the SUT sends !b 2 and !b 3 before receiving ?a 3 .

4. 1

 1 Local Timed Traces and Action-interleaving in Asynchronous Timed Traces We address the derivation of local timed traces from asynchronous traces. Let S ∈ TIOA(I, O) and let ρ = (α i ) i=1..n in Seq( [S] ⊲⊳∆ ) be an asynchronous execution sequence. Each occurrence of a silent action τ a in an asynchronous execution sequences can be interpreted as the reception/transmission of input/output a. For ρ[i] = α i ∈ I ∪ O, let us denote by ζ ρ[i] the unique silent action associated with the visible action ρ[i], when it exists. Notice that either ρ[i] is an input action and ρ[i] ≺ ρ ζ ρ[i] or ρ[i] is an output action and ζ ρ[i] ≺ ρ ρ[i]: this is because the actions in a queue are delivered according to their positions in the queue. Moreover, ζ ρ[i] ≺ ρ ζ ρ[j] whenever ρ[i], ρ[j] are both either inputs or outputs and ρ[i] ≺ ρ ρ[j]. We say that ρ is regular if for every ρ[i] ∈ I ∪ O, ζ ρ[i] exists in ρ. A regular asynchronous timed trace is constructed from a regular asynchronous execution sequence. The local execution sequence associated with a regular asynchronous execution sequence ρ = (α i ) i=1..n , denoted by apply(ρ), is the timed word obtained from ρ by deleting the visible actions in I ∪ O and replacing each silent action ζ ρ[i] (1 ≤ j ≤ n) with the corresponding visible action ρ[i].

Example

  We have that |ρ| = 22. We have that ζ ρ[2] = ρ[6] = τ a1 because τ a1 corresponds to the remote execution of ?a 1 that is transmitted at the time 1. ζ ρ[17] = ρ[11] = τ b because this occurrence of τ b2 corresponds to the transmission of !b 2 and !b 2 is observed later at the position 17. We can check that ζ ρ[15] = ρ[22] = τ a3 . Then apply

Fig. 3 :

 3 Fig. 3: Automata for the FIFOs.

  Tester that can generate two grasps and releases. envLevel < oldLevel (c) Test purpose to increase and then decrease the intensity of the light. envLevel < Max && envLevel > oldLevel (d) Test purpose to increase the intensity of the light and then switch it off.

Fig. 4 :

 4 Fig. 4: Tester and test purpose automata.

  State 0: GRASP until x / ∈ [0, 2[. Goto state 1. State 1: delay until envLevel = 0. Goto state 2. State 2: RESET until x ∈ [0, 2[. Goto state 3. State 3: RELEASE until x / ∈ [0, 2[. Goto state 4. State 4: GRASP until x ∈ [0, 2[. Goto state 5. State 5: delay until x / ∈ [0, 2[. Goto state 6. State 6: RESET until either x ∈ [0, 2[ and then goto state 7 or envLevel = M ax and then goto state 12. State 7: RESET until envLevel = M ax. Goto state 8. State 8: RELEASE until x / ∈ [0, 2[. Goto state 9. State 9: delay until envLevel = 0 and envLevel = M ax. Goto state 10. State 10: delay until purpose.Goal. Goto state 11. State 11: envLevel = 0 and purpose.Goal, reached. State 12: RESET until x ∈ [0, 2[. Goto state 8.

⋆ This work has been partially supported by the French research project ANR VACSIM.

Input/Output Interleaving and ∆-Testability Criterion Asynchronous timed traces are remote observations of local timed traces executed by the implementation. The execution order of actions may differ from the observation

Note that there are three more patterns.

We model-checked that the 2 nd FIFO cannot overflow.

The winning and losing conditions are always implicitly observable.

Using the pre-release version 0.17.


J L Fouquet

H Thuillier

J M Vanherpe

A P Wojda

ON MINIMUM (K q , k) STABLE GRAPHS

Keywords: Mathematics Subject Classification, 035 C Stable graphs, The research of A, P

A graph G is a (Kq, k) stable graph (q ≥ 3) if it contains a Kq after deleting any subset of k vertices (k ≥ 0). In the paper "On (Kq; k)-stable graphs", (http://onlinelibrary.wiley.com/doi/10.1002/jgt.21705/full), to appear in Journal of Graph Theory, Żak has proved a conjecture of Dudek et al. (in "(H, k) stable graphs with minimum size", Discuss. Math. Graph Theory, 28, 2008 ) stating that for sufficiently large k the number of edges of a minimum (Kq, k) stable graph is (2q -3)(k + 1) and that such a graph is isomorphic to sK 2q-2 +tK 2q-3 where s and t are integers such that s(q -1)+t(q -2)-1 = k. We have proved in [3] that for q ≥ 5 and k ≤ q 2 + 1 the graph K q+k is the unique minimum (Kq, k) stable graph. We are interested in the (Kq, κ(q)) stable graphs of minimum size where κ(q) is the maximum value for which for every nonnegative integer k < κ(q) the only (Kq, k) stable graph of minimum size is K q+k and by determining the exact value of κ(q).

Introduction

For terms not defined here we refer to [START_REF] Bondy | Graph Theory[END_REF]. As usual, the order of a graph G is the number of its vertices and the size of G is the number of its edges (denoted by e(G)). The disjoint union of two graphs G 1 and G 2 is denoted by G 1 + G 2 . The union of p mutually disjoint copies of a graph G is denoted by pG. For any set A of vertices, we denote by G[A] the subgraph induced by A and by G -A the subgraph induced by V (G) -A. If A = {v} we write G -v for G -{v}. For any set F of edges, we denote by G -F the spanning subgraph (V (G), E(G) -F ). If F = {e} we write G -e instead of G -{e}. A complete subgraph of order q of G is called a q-clique of G. The complete graph of order q is denoted by K q . When a graph G contains a q-clique as subgraph, we say "G contains a K q ". In [START_REF] Katona | Extremal P 4 -stable graphs[END_REF] Horváth and Katona considered the notion of (H, k) edge stable graph 1 : given a simple graph H, an integer k and a graph G containing H as subgraph, G is a an (H, k) edge stable graph whenever the deletion of any set of k edges does not lead to a H-free graph. These authors consider (P n , k) edge stable graphs and prove a conjecture stated in [START_REF] Frankl | Extremal k-edge hamiltonian hypergraphs[END_REF] on the minimum size of a (P 4 , k) edge stable graph. In [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF], Dudek, Szymański and Zwonek investigated the vertex version of this notion and introduced the (H, k) stable graphs. Definition 1.1. [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] Given an integer k ≥ 0 and a graph H without isolated vertices, a graph G containing a subgraph isomorphic to H is said to be an (H, k) stable graph if, for every subset S of k vertices, G -S contains (a subgraph isomorphic to) H. Definition 1.2. A (H, k) stable graph with minimum size is called minimum (H, k) stable graph. The size of a minimum (H, k) stable graph shall be denoted by stab (H, k).

Note that if G is an (H, k) stable graph with minimum size then the graph obtained from G by addition or deletion of some isolated vertices is also minimum (H, k) stable. Hence we shall assume that all the graphs considered in the paper have no isolated vertices. It is clear that H is the unique (H, 0) stable graph with minimum size.

In this paper we consider (K q , k) stable graphs with q ≥ 2. Since K q+k is (K q , k) stable, note that a trivial upper bound for stab(K q , k) is q+k 2 . It is an easy exercise to see that stab(K 2 , k) = k + 1 and that the matching (k + 1)K 2 is the unique minimum (K 2 , k) stable graph.

Dudek, Szymański and Zwonek have proved in [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] that stab(K 3 , k) = 3(k + 1) for k ≥ 0 and stab(K 4 , k) = 5(k + 1) for k ≥ 1 and they have obtained an upper bound for stab(K q , k) for sufficiently large k. More precisely they have obtained the following result.

Theorem 1.3. [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] For every q ≥ 5, there exists an integer k(q) such that for every

k ≥ k(q), stab(K q , k) ≤ (2q -3)(k + 1).
In order to obtain Theorem 1.3, the authors consider the graph

G = sK 2q-2 + (r - s)K 2q-3 with q ≥ 5, k ≥ (q -1)(q -2), r ∈ {1, • • • , k + 1}, s ∈ {0, • • • ,
r} and r(q-2)+s-1 = k and note that the number of edges of G is (2q-3)(k+1). A smaller bound for k(q) can be obtained by the following Proposition 1.4 (consequence of an old result of J.J. Sylvester [START_REF] Sylvester | Question 7382[END_REF]; see a proof at the end of Section 2), and more generally apart from k ∈ {0, • • • , q -4}, Theorem 1.6 below gives a better upper bound than q+k 2 for stab(K q , k). Proposition 1.4. Let q be an integer ≥ 4. Set

A(q) = 0≤i≤q-4 {i(q -1) + j | 0 ≤ j ≤ q -4 -i} and B(q) = {b ∈ N | 0 ≤ b ≤ (q -2)(q -3) -2} -A(q).
Let k be a nonnegative integer. There exist integers s and t such that s(q -1) + t(q -2)

-1 = k if and only if k ∈ B(q) or k ≥ k(q) = (q -3)(q -2) -1. For such a pair (s, t), G = sK 2q-2 + tK 2q-3 is (K q , k) stable and e(G) = (2q -3)(k + 1). Note that |A(q)| = (q-3)(q-2) 2 and |B(q)| = |A(q)| -1.
Lemma 1.5. Let q ≥ 4 and k ≥ 0 be integers. Then k ∈ A(q) if and only if [ k+1 q-1 , k+1 q-2 ] contains no integer. Theorem 1.6. Let q ≥ 3 and k ≥ 0 be integers. Set A(3) = B(3) = ∅, and for q ≥ 4 A(q) and B(q) are the sets defined in Proposition 1.4. For every positive integer r set

φ(r) = 1 2 q -1 + k + 1 r q -2 - k + 1 r r + 2(k + 1) . Then, stab(K q , k) is at most equal to • φ(1) = 1 2 (q + k -1)(q + k) if k ≤ q -4 (note that k is in A(q)), • M in {φ( k+1 q-1 ), φ( k+1 q-1 + 1)} if k ∈ A(q) and k ≥ q -1, • (2q -3)(k + 1) if k ∈ B(q) or k ≥ k(q) = (q -3)(q -2) -1 (note that φ(r) = (2q -3)(k + 1) for every integer r ∈ [ k+1 q-1 , k+1 q-2 ]
). We shall give a proof of Theorem 1.6 in Section 3 by considering (K q , k) stable graphs having cliques as components and having the minimum number of edges. As a consequence, if every component of a mimimum (K q , k) stable graph is complete (see Problem 1.15) then the upper bound given in Theorem 1.6 is the exact value for stab(K q , k).

In light of their results, Dudek, Szymański and Zwonek propose the following conjecture.

Conjecture 1.7. [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] There exists an integer k(q) such that for every k ≥ k(q), stab(K q , k) = (2q -3)(k + 1).

Note that Conjecture 1.7 is true for q ∈ {3, 4}. In [START_REF] Fouquet | On (Kq, k) vertex stable graphs with minimum size[END_REF] we have proved that stab(K 5 , k) = 7(k+1) for k ≥ 5, which confirms Conjecture 1.7 for q = 5. Moreover, we have characterized (K q , k) stable graphs with minimum size for q ∈ {3, 4, 5}. The following theorem summarizes these results.

Theorem 1.8. [START_REF] Fouquet | On (Kq, k) vertex stable graphs with minimum size[END_REF] Let G be a minimum (K q , k) stable graph, with q ∈ {3, 4, 5} and k ≥ k(q) with k(3) = 0, k(4) = 1, k(5) = 5. Then G = sK 2q-2 + tK 2q-3 , for any choice of s and t such that s(q -1) + t(q -2) -1 = k. Moreover, K 5+k is the unique minimum (K 5 , k) stable graph for k ∈ {1, 2, 3}, K 9 and K 6 + K 7 are the only minimum (K 5 , 4) stable graphs.

An important fact is that Conjecture 1.7 of Dudek, Szymański and Zwonek has been recently solved by Andrzej Żak [START_REF] Żak | On (Kq; k)-stable graphs[END_REF], who has characterized also the extremal graphs.

Theorem 1.9. [START_REF] Żak | On (Kq; k)-stable graphs[END_REF] Let q ≥ 2, k ≥ 0 be nonnegative integers. Then stab(K q , k) ≥ (2q -3)(k + 1), with equality if and only if k = s(q -1) + t(q -2) -1 for some nonnegative integers s and t. In particular, stab(K

q , k) = (2q -3)(k + 1) for k ≥ (q -3)(q -2) -1. Furthermore, if G is a (K q , k) stable graph having exactly (2q -3)(k + 1) edges then G = sK 2q-2 + tK 2q-3
where s and t are nonnegative integers such that s(q -1) + t(q -2) -1 = k. Remark 1.10. Since (K q , k) stable graphs with minimum size for q ∈ {3, 4, 5, 6} have been characterized (see Theorem 1.8 for q ≤ 5 and [START_REF] Żak | On (Kq; k)-stable graphs[END_REF] for q = 6), to close the study of minimum (K q , k) stable graphs we have only to consider q ≥ 7 and k ∈ A(q) (the set defined in Proposition 1.4).

We have proved in [START_REF] Fouquet | On (Kq, k) vertex stable graphs with minimum size[END_REF] that K q+k is the unique minimum (K q , k) stable graph for q ≥ 4 and k ∈ {1, 2}, that K q+3 is the unique minimum (K q , 3) stable graph for q ≥ 5 and in [START_REF] Fouquet | On (Kq, k) stable graphs with small k[END_REF] that K q+k is the unique (K q , k) stable graph for q ≥ 6 and

k ≤ q 2 + 1. Remark that q+k 2 -(2q -3)(k + 1) = (q-k-3)(q-k-2) 2
and that this integer is positive for q ≥ 3 and k / ∈ {q -3, q -2}. Then, as a consequence of Proposition 1.4, for q ≥ 4 and for every integer k for which k ∈ B(q) -{q -3, q -2} or k ≥ (q -3)(q -2) -1 the graph K q+k is not minimum (K q , k) stable. Hence, the set {k ∈ N | K q+k is minimum (K q , k) stable} is bounded above, and we propose the following definition.

Lemma 2.3. [2] Let G be an (H, k) stable graph with k ≥ 1 and e ∈ E(G) such that G -e is not (H, k) stable. Then G is exactly (H, k) stable and G -e is exactly (H, k -1) stable.
Definition 2.4. [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] Let G be an (H, k) stable graph. If G -e is not (H, k) stable for every edge e ∈ E(G), G is said to be minimal (H, k) stable. Remark 2.5. In [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF]

, k 2 , ..., k r , with 0 ≤ k i ≤ k, such that i) for every i, with 1 ≤ i ≤ r, G i is exactly (H, k i ) stable, ii) r i=1 k i + (r -1) = k , G is minimal (H, k) stable if and only if for every i, 1 ≤ i ≤ r, G i is minimal (H, k i ) stable. Moreover, if G is minimum (H, k) stable then for every i, 1 ≤ i ≤ r, G i is minimum (H, k i ) stable. Proof. For each i, 1 ≤ i ≤ r,
S i the set S ∩ V (G i ). Clearly, there exists i 0 ∈ {1, • • • , r} such that |S i0 | ≤ k i0 = |T i0 |-1. Then, G i0 -S i0 contains a subgraph isomorphic to H, that is, G is exactly (H, |T | -1)
stable, and we have

r i=1 k i + (r -1) = k.
Let e be an edge of G and let G i be the component containing e.

Claim. G -e is (H, k) stable if and only if

G i -e is (H, k i ) stable. Proof. Suppose that G i -e is (H, k i ) stable. Let U be a H-transversal of G -e. Set U i = U ∩ V (G i -e) = U ∩ V (G i ) and for every j = i, U j = U ∩ V (G j ). Since (G i -e) -U i and each G j -U j , j = i, contain no subgraphs of G -e isomorphic to H, we have for every j, 1 ≤ j ≤ r, |U j | ≥ k j + 1. Then, |U | = r j=1 |U j | ≥ k + 1.
Hence, for every set S of k vertices (G -e) -S contains a subgraph isomorphic to H, that is, G -e is (H, k) stable. Conversely, suppose that G i -e is not (H, k i ) stable. Let T i be a H-transversal of (G i -e) -T i having k i vertices. For every j = i let T j be a H-transversal of G j having k j + 1 vertices. The set T = ∪ r j=1 T j has k vertices and is a H-transversal of G -e, that is, G -e is not (H, k) stable. Thus, G is minimal (H, k) stable if and only if for every i,

1 ≤ i ≤ r, G i is minimal (H, k i ) stable.
Note that, by replacing a minimal (H, k i ) stable component G i by any minimal (H, k i ) stable graph G i (connected or not), we obtain again a minimal (H, k) stable graph. Thus, if G is minimum (H, k) stable then for every i,

1 ≤ i ≤ r, G i is minimum (H, k i ) stable. Remark 2.9. Let r be an integer ≥ 2, k 1 , • • • , k r be r non negative integers and k = r i=1 k i + (r -1). If for every i, 1 ≤ i ≤ r, G i is a minimum (H, k i ) stable graph then the disjoint union G 1 + G 2 + • • • + G r
may not be a minimum (H, k) stable graph. For example, K q is minimum (K q , 0) stable, 2K q and K q+1 are minimal (K q , 1) stable, but for q ≥ 4 since e(2K q ) > e(K q+1 ), the graph 2K q is not minimum (K q , 1) stable.

Given relatively prime positive integers a 1 , • • • , a n , let us consider the integers that can be expressed as a sum

k 1 a 1 + k 2 a 2 + • • • + k n a n , where k 1 , k 2 , • • • , k n are nonnegative integers.
Any such integer is said to be representable. Recall that the Frobenius Problem is the following: find the largest non-representable integer (called the Frobenius number and denoted by g(a 1 , ..., a n )). If n = 2, the Frobenius number is given by the formula g(a 1 , a 2 ) = a 1 a 2 -a 1 -a 2 . This formula was discovered by J. J. Sylvester in 1884 [START_REF] Sylvester | Question 7382[END_REF] who also demonstrated that there are a total of N (a 1 , a 2 ) = (a1-1)(a2-1) 2 non-representable integers. For the particular case a 2 = a 1 -1 one obtains explicitely the set of non-representable integers.

Lemma 2.10. [START_REF] Sylvester | Question 7382[END_REF] Let a be an integer ≥ 3 and the function α

: N × N -→ N such that α(s, t) = sa + t(a -1). Set A = 0≤i≤a-3 {ia + j | 1 ≤ j ≤ a -2 -i}.
Every b ∈ N -A is representable (that is there exists a pair {s, t} of nonnegative integers such that b = sa+t(a-1)), and every b in A is not representable. Moreover, every representable b has a unique representation sa+t(a-1) such that 0 ≤ t ≤ a-1.

We shall give a proof of Lemma 2.10 for completeness.

Proof of Lemma 2.10 Note that M ax(

A) = (a -1)(a -2) -1, |A| = (a-1)(a-2) 2
and for s ≥ 0 and t ≥ 1, α(s, t) = α(s + 1, t -1) -1. Consider the infinite matrix {α(s, t)} s≥0, t≥0 . For any t ≥ 0 the values of the diagonal {α(i, t-i) | 0 ≤ i ≤ t} are the consecutive integers {t(a-1)+i | 0 ≤ i ≤ t}. For s ≥ 0, the values of the (partial) diagonal {α(s

+ i, a -i -1) | 0 ≤ i ≤ a -1} are the consecutive integers sa + (a -1) 2 , sa + (a -1) 2 + 1, • • • , sa + a(a -1).
Since α(0, a -1) = α(a -2, 0) + 1 and for every s ≥ 0 α(s + a -1, 0) + 1 = α(s + 1, a -1) = sa + a(a -1) + 1, every integer b ≥ (a -2)(a -1) appears in

{α(i, a -2 -i) | 0 ≤ i ≤ a -2} ∪ ( s≥0 {α(s + i, a -i -1) | 0 ≤ i ≤ a -1}. Let B = 0≤i≤a-3 {α(j, i -j) | 0 ≤ j ≤ i} = 0≤i≤a-3 {i(a -1) + j | 0 ≤ j ≤ i}.
Clearly |B| = |A|. It is easy to check that A and B are disjoint sets and that A ∪ B = {0, 1, • • • , (a -2)(a -1) -1}. Thus, every b ∈ A is not representable and for every integer b ∈ N -A there exists a unique pair (s, t) with s ≥ 0 and 0 ≤ t ≤ a -1 such that b = sa + t(a -1).

Remark 2.11. It is easy to see that every representable b < a(a -1) has a unique representation. For a representable b ≥ a(a-1), since we can choose values of t ≥ a, it is possible that b = α(s, t) = α(s , t ) for distinct pairs (s, t) and (s , t ). Indeed, if s ≥ a -1 then for every positive integer r ≤ s a-1 , α(s, t) = α(s -r(a -1), ra + t)).

Proof of Proposition 1.4

Let us apply Lemma 2.10 to a = q -1 and b = k + 1. B(q) is the set of integers k ≤ (q -3)(q -2) -3 such that k + 1 is representable as s(q -1) + t(q -2). More precisely

B(q) = 1≤i≤q-4 {i(q -2) + j -1 | 0 ≤ j ≤ i}.
It is easy to see that the set of integers k such that k + 1 is not representable as s(q -1) + t(q -2) is

A(q) = 0≤i≤q-4 {i(q -1) + j | 0 ≤ j ≤ q -4 -i}.
A minimum K q -transversal of G = sK 2q-2 + tK 2q-3 contains exactly s(q -1) + t(q -2) = k + 1 vertices, that is G is (K q , k) stable, and it is easy to check that e(G) = (2q -3)(k + 1).

Proof of Lemma 1.5

If there exist integers s and t such that s(q-1)+t(q-2) = k+1 then k+1 q-1 = s+t-t q-1 and k+1 q-2 = s + t + s q-2 , and hence

r = s + t ∈ [ k+1 q-1 , k+1 q-2 ]. Conversely, let r ∈ [ k+1 q-1 , k+1 q-2 ]. Then, q -2 ≤ k+1 r ≤ q -1. If k + 1 = r(q -1) then we are done. If k+1 q-1 < r then q -2 = k+1 r
is the quotient in the division of k + 1 by r. Hence, if s denotes the remainder then k + 1 = r(q -2) + s = s(q -1) + (r -s)(q -2). We conclude by applying Proposition 1.4.

Minimum (K q , k) stable graphs

In this section we are interested in (K q , k) stable graphs with minimum size (q ≥ 3). Recall that stab(K q , k) = Min{e(G) | G is (K q , k) stable}.

3.1. Some known results. We give here some known results about this topic. By Remark 2.5 and Lemma 2.6 we have: Properties 3.1. [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] A minimal (K q , k) stable graphs G has the following properties:

P 1 ) G is exactly (K q , k) stable. P 2 ) For every edge e, G -e is exactly (K q , k -1) stable. P 3 ) For every vertex v, G -v is exactly (K q , k -1) stable. P 4 ) Every vertex of G belongs to some q-clique of G. P 5 ) Every edge of G belongs to some q-clique of G.

Remark 3.2. For any two integers q ≥ 3 and k ≥ 1, K q+k is minimal (K q , k) stable.

Proposition 3.3. [4] K 5 is the unique minimum (K 4 , 1) stable graph, K 6 is the unique minimum (K 4 , 2) stable graph and for every integer q ≥ 5 and every integer k ∈ {1, 2, 3}, K q+k is the unique minimum (K q , k) stable graph.

Dudek et al. [2] defined the family

A (Kq,k) r with k ≥ 0, q ≥ 3, 1 ≤ r ≤ k + 1 as the family of graphs consisting of r complete graphs K ij with i 1 ≥ • • • ≥ i r ≥ q satisfying the condition r i=1 (i j -q)+(r -1) = k and they proved that every graph in A (Kq,k) r is minimal (K q , k) stable. We observe that if a (K q , k) stable graph G is a disjoint union of r ≥ 1 cliques K ij , 1 ≤ j ≤ r, then by Theorem 2.8, G ∈ A (Kq,k) r . They defined a graph G ∈ A (Kq,k) r
as a balanced union if |i j -i l | ∈ {0, 1} for every j and l in {1, 2, • • • , r} and they proved that given q, k and r there is exactly one balanced union

B (Kq,k) r in A (Kq,k) r
, and that B (Kq,k) r has the minimum number of edges among the graphs in A (Kq,k) r . In [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] the following lemma has been given. We give its proof for completeness. Lemma 3.4. [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] Let G 0 be a (K q , k 0 ) stable graph (k 0 ≥ 0) which has the minimum size among all graphs beeing a disjoint union of r cliques (r ≥ 1) G j ≡ K q+kj with 1 ≤ j ≤ r, k j ≥ 0. There exist nonnegative integers s and k such that 0 ≤ s ≤ r -1,

G 0 = sK q+k+1 + (r -s)K q+k with r(k + 1) + s = k 0 + 1 and e(G 0 ) = 1 2r (r(q -1) + k 0 + 1 -s) (r(q -2) + k 0 + 1 + s) .
Proof. Suppose, without loss of generality, that k 1 ≥ k 2 ≥ • • • ≥ k r and that there exist two components G i and G j with i < j such that k i -k j ≥ 2. By substituting G i ≡ K q+ki-1 for G i and G j ≡ K q+kj +1 for G j , we obtain a new (K q , k) stable graph G 0 such that e(G 0 ) = e(G 0 ) -(k i -k j -1) < e(G 0 ), which is a contradiction. Thus, for any i and any j, 0 ≤ |k i -k j | ≤ 1. Hence, either for any i and any j k i and k j have the same value k and we have G 0 = rK q+k with k ≥ 0, or there exist distinct k i and k j and we have

G 0 = sK q+k+1 + (r -s)K q+k with k ≥ 0 and 0 ≤ s ≤ r -1. Hence, a minimum K q -transversal of G 0 has k 0 + 1 = s(k + 2) + (r -s)(k + 1) = s + r(k + 1) vertices. Note that r divides k 0 + 1 -s. We have 2e(G 0 ) = s(q + k + 1)(q + k) + (r -s)(q + k)(q + k -1). Since k + 1 = k0+1-s r
, we obtain e(G 0 ) = 1 2r (r(q -1) + k 0 + 1 -s)(r(q -2) + k 0 + 1 + s).

Remark 3.5. In Lemma 3.4 the integers q, k 0 and r are given. Given q and k 0 , in order to obtain an upper bound for stab(K q , k 0 ) we will determine the values of r for which e(G 0 (r)) = 1 2r (r(q -1)

+ k 0 + 1 -s)(r(q -2) + k 0 + 1 + s)) is minimum.
We note that if every component of a minimum (K q , k 0 ) stable graph is complete then the minimum value of e(G 0 (r)) is exactly stab(K q , k 0 ).

3.2. Proof of Theorem 1.6. First we give a technical lemma used for proving Theorem 1.6.

Lemma 3.6. Let a and b be positive integers and for x > 0 consider the real-to-real function . We note that if r is a positive integer then f (r) is a positive integer. Now we will find the minimum value of f (r) when r is a positive integer.

f (x) = 1 2 a + 1 + b x a - b x x + 2b . Then, f is continuous on ]0, +∞[, nonincreasing on ]0, b a+1 ], constant on [ b a+1 , b a ] and nondecreasing on [ b a , +∞[. Moreover M in{f (r) | r ∈ N -{0}} is equal to • f (1) = 1 2 (a + b + 1)(a + b) if [ b a+1 , b a ] contains no integer and b < a, • M in {f ( b a+1 ), f ( b a+1 +1)} if [ b a+1 , b a ] contains no

Case 1: [

b a+1 , b a ] ∩ N = ∅. Note that 0 < b a -b a+1 < 1 (that is 0 < b < a(a + 1) ), 0 ≤ b a+1 ≤ a and b a+1 < b a+1 < b a < b a = b a+1 + 1. Case 1.1: b < a. Since b a = 1 and f (r) is non decreasing on [ b a , +∞[, the minimum value is f (1) = 1 2 (a + b + 1)(a + b). Case 1.2: b ≥ a. Since b / ∈ {a, a + 1}, we have b > a + 1 and 1 ≤ b a+1 ≤ a ; hence the minimum value is M in f b a + 1 , f b a + 1 + 1 .
Let β be the remainder of the division of b by a + 1. In order to obtain the value f ( b a+1 ) we must know the integer

p 1 ≥ a + 1 such that b p1+1 < b a+1 ≤ b p1 . Since b a+1 = b-β a+1 , we have p 1 = b(a+1) b-β
, and hence

f b a + 1 = 1 2 (a + 1 + p 1 ) (a -p 1 ) b -β a + 1 + 2b .
In the same way we obtain Proof of Theorem 1.6. In order to avoid confusion between "k" of the statement of Theorem 1.6 and "k" appearing in the proof of Lemma 3.4, let us replace "k" by "k 0 " in the statement of Theorem 1.6. Consider the (K q , k 0 ) stable graph G 0 defined in Lemma 3.4 and see Remark 3.5. We have G 0 = sK q+k+1 + (r -s)K q+k with r(k + 1) + s = k 0 + 1 and e(G 0 ) = 1 2r (r(q -1) + k 0 + 1 -s)(r(q -2) + k 0 + 1 + s). Since k + 1 is the quotient of k 0 + 1 divided by r and s is the remainder, we have s = k 0 + 1 -r k0+1 r . Hence, e(G 0 (r)) = 1 2 q -1 + k 0 + 1 r q -2 -k 0 + 1 r r + 2(k 0 + 1) .

f b a + 1 + 1 = 1 2 (a + 1 + p 2 ) (a -p 2 ) b + a + 1 -β a + 1 + 2b with p 2 = b(a+1) b+a+1-β .
Set a = q -2, b = k 0 + 1 and apply Lemma 3.6 and Lemma 1.5.

3.3. Minimum (K q , k) stable graph for small k. In the following, if no confusion is possible, we simply denote the integer κ(q) by κ.

Lemma 3.7. Suppose that q ≥ 4. If κ is even then stab(K q , κ -1) < e(2K q+ κ 2 -1 ) and stab(K q , κ) ≤ e(K q+ κ 2 + K q+ κ 2 -1 ) . If κ is odd then stab(K q , κ-1) < e(K q+ κ-1 2 +K q+ κ-3

2

) and stab(K q , κ) ≤ e(2K q+ κ-1 2 ) .

Proof. Recall that, by definition of κ, K q+κ-1 is the only minimum (K q , κ -1) stable. If κ is even then 2K q+ κ 2 -1 is exactly (K q , κ -1) stable and K q+ κ 2 + K q+ κ 2 -1 is exactly (K q , κ) stable. If κ is odd then K q+ κ-1

2

+ K q+ κ-3 2 is exactly (K q , κ -1) stable and 2K q+ κ-1 2 is exactly (K q , κ) stable. Lemma 3.8. Let q ≥ 3 and p ≥ 0 be two integers. Then, e(K q+2p ) < e(K q+p + K q+p-1 ) if and only if p 2 + p < 1 2 (q -1)(q -2) and e(K q+2p ) = e(K q+p + K q+p-1 ) if and only if p 0 = 1 2 ( 1 + 2(q -1)(q -2) -1) is an integer and p = p 0 . e(K q+2p+1 ) < e(2K q+p ) if and only if (p + 1) 2 < 1 2 (q -1)(q -2) and e(K q+2p+1 ) = e(2K q+p ) if and only if p 1 = 1 2 ( 2(q -1)(q -2) -1) is an integer and p = p 1 .

Proof. It is easy to check that e(K q+2p ) -e(K q+p + K q+p-1 ) = p 2 + p -1 2 (q -1)(q -2) and e(K q+2p+1 ) -e(2K q+p ) = (p + 1) 2 -1 2 (q -1)(q -2). These polynomials of degree 2 in p have positive roots p 0 = 1 2 ( 1 + 2(q -1)(q -2) -1) and p 1 = 1 2 ( 2(q -1)(q -2) -1) respectively.

Proof of Theorem 1.13. If κ = 2p then, by Lemma 3.7, stab(K q , κ -1) < e(2K q+ κ 2 -1 ). Since κ -1 = 2(p -1) + 1, by Lemma 3.8, p 2 < 1 2 (q -1)(q -2), that is, κ < 2(q -1)(q -2).

1 2

 1 integer and b > a+1, • (2a + 1)b if [ b a+1 , b a ] contains at least one integer r (and is equal to f (r) for every such r). Proof. For x > b we have b x = 0 and f (x) = 1 2 (a + 1)(ax + 2b). For every integer p ≥ 1 and for every x ∈ ] b p+1 , b p ] we have b x = p, and hence f (x) = (a + 1 + p)((a -p)x + 2b). It is easy to see that the function f is continuous on ]0, +∞[, nonincreasing on ]0, b a+1 ], constant on [ b a+1 , b a ] and nondecreasing on [ b a , +∞[. The minimum value for f (x) (with x positive real number) is the integer (2a + 1)b and is reached for every real number x in [ b a+1 , b a ]

Case 2 :

 2 [ b a+1 , b a ] ∩ N = ∅. For any integer r such that b a+1 ≤ r ≤ b a f (r) is equal to the minimum value (2a + 1)b.

  "minimal (H, k) stable graphs" are called "strong (H, k) stable graphs" by the authors. Note that an (H, k) stable graph G is minimal (H, k) stable if and only if for every e ∈ E(G) the graph G -e is exactly (H, k -1) stable. Moreover, a minimal (H, k) stable graph is exactly (H, k) stable. If there exists an edge e of an (H, k) stable graph G such that there are no subgraph isomorphic to H containing e then G -e is an (H, k) stable graph. Hence, we have the following. Every edge of a minimal (H, k) stable graph is contained in a subgraph isomorphic to H. Consequently, every vertex of a minimal (H, k) stable graph is also contained in a subgraph isomorphic to H. Remark 2.7. Clearly, every minimum (H, k) stable graph is minimal (H, k) stable. One may ask what happens for components of an (H, k) stable graph. The following theorem gives us an answer when H is connected. We shall say that a graph containing no subgraph isomorphic to H is (H, -1) stable.

	Lemma 2.6. [2]

Theorem 2.8. Let H be a connected graph containing at least 2 vertices, let G be an exactly (H, k) stable graph, and let G 1 , G 2 , ..., G r , with r ≥ 1, be its components. Then, there exist integers k 1

Wojda was partially supported by polish Ministry of Science and Higher Education.

Definition 1.11. For every integer q ≥ 4, we denote by κ(q) the greatest integer such that for 1 ≤ k < κ(q) the only minimum (K q , k) stable graph is K q+k .

We will focuse our attention on determining the exact value of κ(q). In two previous papers we have proved the following. Theorem 1.12. [START_REF] Fouquet | On (Kq, k) stable graphs with small k[END_REF][START_REF] Fouquet | On (Kq, k) vertex stable graphs with minimum size[END_REF] κ(3) = 1, κ(4) = 3, κ(5) = 4 and for q ≥ 6 κ(q) > q 2 + 1. In this paper we give an upper bound for the value of κ(q). Theorem 1.13. For every q ≥ 4, if κ(q) is even then κ(q) < 2(q -1)(q -2) and if κ(q) is odd then κ(q) < 1 + 2(q -1)(q -2)

We prove that these upper bounds are reached for values of q such that there exists a minimum (K q , κ(q)) stable disconnected graph (note that it is the case for q = 4 and q = 5).

Theorem 1.14. Let q ≥ 4 and suppose that there exists a disconnected minimum

2 (q -1)(q -2) ≤ ρ(q) 2 + ρ(q) then κ(q) = 2ρ(q). Proofs of Theorems 1.13 and 1.14 shall be given in subsection 3.3.

Remark that, by definition of κ(q) and by Theorem 1.9, for every integer k in

every component of any minimum (K q , k) stable graph is complete, but we do not know if it is true for k in { l ∈ N | l ≥ κ(q) and l ∈ A(q)} (where A(q) and B(q) are the sets defined in Proposition 1.4).

If there is no minimum disconnected (K q , κ(q)) stable graph then, by definition of κ(q), there exists a connected minimum (K q , κ(q)) stable graph G q which is not complete. We think that it never happens, so we propose the following problem.

Problem 1.15. Is it true that if G is a minimum (K q , k) stable graph then every component of G is complete?

If the answer is positive then Theorem 1.14 gives the exact value of κ(q) for every q ≥ 4.

General results

Lemma 2.1. [START_REF] Dudek | stable graphs with minimum size(H, k)[END_REF] Let G be an If κ = 2p + 1 then by Lemma 3.7, stab(K q , κ -1) < e(K q+ κ-1

).

Since κ -1 = 2p, by Lemma 3.8, p < 1 2 ( 1 + 2(q -1)(q -2) -1), that is, κ < 1 + 2(q -1)(q -2). Theorem 3.9. Let q ≥ 4 and suppose that there exists a minimum (K q , κ) stable graph G 0 which is disconnected. Then G 0 is isomorphic to

Hence, e(K q+kr+kr-1+1 ) < e(K q+kr ) + e(K q+kr-1 ) and the graph

and by Lemma 3.4 the theorem follows.

Note that Theorem 3.9 implies that there exists at most one disconnected minimum (K q , κ) stable graph and this graph, if it exists, is

Proof of Theorem 1.14. By Lemma 3.7 and Theorem 3.9, if κ is odd then

) ≤ e(K q+κ ) (note that, by Lemma 3.8, it may be possible that e(2K q+ κ-1 2 ) = e(K q+κ ) for some values of q), if κ is even then

) ≤ e(K q+κ ) (note that, by Lemma 3.8, it may be possible that e(K q+ κ 2 + K q+ κ 2 -1 ) = e(K q+κ ) for some values of q). For κ = 2p + 1 we have 1 2

(q + 2p)(q + 2p -1) < (q + p -1) 2 < (q + p)(q + p -1) ≤ 1 2 (q + 2p + 1)(q + 2p) .

This implies that

For κ = 2p we have 1 2 (q +2p-1)(q +2p-2) < (q +p-1)(q +p-2) < (q +p-1) 2 ≤ 1 2 (q +2p)(q +2p-1) .

This implies that (B) p 2 < 1 2 (q -1)(q -2) ≤ p 2 + p .

Combining (A) and (B) yields

This implies that 1 2 (q -1)(q -2) -1 ≤ p < 1 2 (q -1)(q -2) .

Hence, p = ρ(q) = 1 2 (q -1)(q -2) -1. By inequalities (A) and (B), position of 1 2 (q -1)(q -2) in comparison to ρ(q) 2 +ρ(q) determines the parity of κ. Hence, if 1 2 (q -1)(q -2) > ρ(q) 2 + ρ(q) then κ = 2ρ(q) + 1 = 2

If there is no minimum disconnected (K q , κ(q)) stable graph then, by definition of κ(q), there exists a connected minimum (K q , κ(q)) stable graph G q distinct from a clique. Note that if such a graph exists then e(G q ) < M in{e(K q+κ ), e(K q+ κ 2 + K q+ κ 2 -1 )} if κ = κ(q) is even or e(G q ) < M in{e(K q+κ ), e(2K q+ κ-1

2

)} if κ = κ(q) is odd .

A positive answer to Problem 1.15 states that there is no such graph G q .