Yliès Falcone

Jean-Claude Fernandez

Thierry Jéron

Hervé Marchand

Laurent Mounier

More Testable Properties

Testing remains a widely used validation technique for software systems. However, recent needs in software development (e.g., in terms of security concerns) may require to extend this technique in order to address a larger set of properties.

In this article, we explore the set of testable properties within the Safety-Progress classification where testability means to establish by testing that a relation, between the tested system and the property under scrutiny, holds. We characterize testable properties w.r.t. several relations of interest. For each relation, we give a sufficient condition for a property to be testable. Then, we study and delineate a fine-grain characterization of testable properties: for each Safety-Progress class, we identify the subset of testable properties and their corresponding test oracle. Furthermore, we address automatic test generation for the proposed framework by providing a general synthesis technique that allows to obtain canonical testers for the testable properties in the Safety-Progress classification. Moreover, we show how the usual notion of quiescence can be taken into account in our general framework, and, how quiescence improves the testability results. Then, we list some existing testing approaches that could benefit from this work by addressing a wider set of properties. Finally, we propose Java-PT, a prototype Java toolbox that implements the results introduced in this article.

1 Let us recall that safety properties are the properties stating that "a bad thing should not happen".

2 Let us recall that a co-safety property is a property whose negation is a safety property.

Introduction

Due to its ability to scale up well and its practical efficiency, testing remains one of the most effective and widely used validation techniques for software systems. However, due to recent needs in the software industry (for instance in terms of security), it is important to reconsider the classes of requirements this technique allows to validate or invalidate. The aim of a testing stage may be either to find defects or to witness expected behaviors on an implementation under test (IUT). From a practical point of view, a test campaign consists in producing a test suite (test generation) from some initial system description, and executing it on the system implementation (test execution). The test suite consists in a set of test cases, where each test case is a sequence of interactions to be executed by an external tester (performed on the points of control and observation, PCOs). Any execution of a test case should lead to a test verdict, indicating if the system succeeded or not on this particular test (or if the test was not conclusive).

Since testing is intrinsically a partial validation technique, an important issue raised when conducting a test campaign is to produce and select the most relevant test cases. A possible approach consists in using a property to drive the test generation and/or test execution steps. In this case, the property is used to generate the so-called test purposes [START_REF] Koch | Autolink: A tool for automatic test generation from SDL specifications[END_REF][START_REF] Jard | TGV: theory, principles and algorithms[END_REF] so as to select test cases according to some predefined abstract test scenario. A property may also represent the desired or undesired behavior of the system. As an example, such a property may formalize some security policy describing both prohibited behaviors and user expectations, as considered in [START_REF] Le Traon | Testing Security Policies: Going Beyond Functional Testing[END_REF][START_REF] Mallouli | A Formal Approach for Testing Security Rules[END_REF]. Moreover, several approaches (e.g., [START_REF] Constant | Integrating Formal Verification and Conformance Testing for Reactive Systems[END_REF]) combine classical testing techniques and property verification so as to improve the test activity. Most of these approaches used safety 1 and co-safety 2 properties. Then, a natural question is whether other kinds of properties can be tested, which arises in defining a precise notion of testability.

In [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF][START_REF] Grabowski | SDL and MSC based test case generation-an overall view of the SAMSTAG method[END_REF], Nahm, Grabowski, and Hogrefe addressed the testability issue by discussing the set of temporal properties that can be tested on an implementation. A property is said to be testable if, from a finite test execution σ, it is possible to determine if a given relation R holds between the set of executions satisfying this property and the set of (finite and infinite) executions that could be produced by possible continuations of σ. Thus, depending on the choice of the relation R, a test campaign can answer specific questions such as: R1: Is the set of execution sequences of the IUT included in the set of execution sequences described by the property? R2: Is the set of execution sequences described by the property included in the set of execution sequences of the IUT? R3: Is the set of execution sequences of the IUT equal to the set of execution sequences described by the property? R4: Do the set of execution sequences of the IUT and the set of execution sequences described by the property intersect?

In [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF][START_REF] Grabowski | SDL and MSC based test case generation-an overall view of the SAMSTAG method[END_REF], this notion of testability is studied w.r.t. the Safety-Progress classification (see [START_REF] Chang | Characterization of Temporal Property Classes[END_REF] and Sect. 4) for infinitary properties. The announced classes of testable properties are the safety and guarantee 3 classes. Then, it is not too surprising that most of the previously depicted approaches used safety and co-safety properties during testing. Then, an interesting question is "Are there other properties (beyond safety and guarantee properties) that are also testable?". Answering positively this question would open the way to design and extend testing frameworks so that they can validate a broader class of expected behaviors of software systems, and thus would allow to address the validation of nowadays more and more complex requirements of software systems. As we shall see, in this article we give a positive answer to this question by exhibiting properties in the Safety-Progress classification that are strictly more expressive than safety and guarantee properties.

Context. In this paper, we shall use the same notion of testability. We consider a generic approach, where an underlying property is compared to the possibly infinite executions of the IUT triggered by a tester. This property expresses finite and infinite4 observable behaviors (which may be desired or not). Obviously, the challenge addressed by a tester is to be able to perform this aforementioned comparison using only a finite execution of the IUT. Note that in practice the property under scrutiny is sometimes expressed using more abstract events than the ones occurring at the IUT's execution level. However, this testability problem can still be addressed while abstracting this alphabet discrepancy. Moreover, a characteristic of this testability definition is that it does not require the existence of an executable specification to generate the test cases. As we shall see, using a property (instead of an executable specification) allows to encompass several existing conformance testing approaches.

Main contributions. This article contributes to propertyoriented testing activities by leveraging the use of an extension of the Safety-Progress classification dedicated to runtime techniques. More specifically, the contributions of the article are as follows:

1. to propose a general approach for property-oriented software testing discussed along four relevant implementation relations, that compare the set of executions of the IUT with those described by a property (e.g., inclusion of the former in the later), and that represent a comprehensive set of property-oriented testing activities; 2. to propose a formal framework that generalizes some existing testing activities (e.g., conformance testing) and provides a formal basis for some other testing activities; 3. to give a precise characterization of testable properties that extends the initial results on testability in [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF][START_REF] Grabowski | SDL and MSC based test case generation-an overall view of the SAMSTAG method[END_REF] by showing that lots of interesting properties (neither safety nor guarantee) are also testable (i.e., there exist test executions allowing to produce a verdict); 4. to propose a framework that allows to easily obtain test oracles producing verdicts according to the possible test executions; 5. to show how this material can be applied to existing test generation frameworks; 6. and, finally, to present the Java toolbox Java-PT, a software implementation allowing a test designer to improve a test activity using a property, following the results proposed in the article.

A preliminary version of this paper appeared in the proceedings of ICTSS '10 [11]. This paper brings the following additional contributions. Firstly, the paper is given a more detailed theoretical treatment. Concerning the implementation relations, we explore the set of testable properties for three additional implementation relations (in [START_REF] Falcone | More Testable Properties[END_REF] only relation R1 mentioned above was studied). Moreover, we add additional examples and complete proofs for all announced results. We propose a deeper study of related work, first by describing some testing frameworks that can be leveraged by the results provided by this paper, and second by showing that our results also encompass the (usual) notion of conformance testing [START_REF] Tretmans | A formal approach to conformance testing[END_REF]. Finally, we introduce Java-PT by giving some implementation details and usage examples.

Paper organization. The remainder of this paper is organized as follows. First, we present in Sect. 2 a small motivating example that will be used in the rest of the paper. In Sect. 3, some preliminary concepts and notation are introduced. A quick overview of the Safety-Progress classification of properties for runtime validation techniques is given in Sect. [START_REF] Chang | Characterization of Temporal Property Classes[END_REF]. Section 5 introduces the notion of testability considered in this paper. In Sect. 6, testable properties are characterized. Automatic test generation is addressed in Sect. 7, and then we show in Sect. 8 how to take into account some notion of quiescence from the IUT. Next, in Sect. 9, we overview related work and propose a discussion on the results provided by this paper. A presentation of Java-PT, a prototype tool implementing the results afforded by this paper, is given in Sect. [START_REF] Brinksma | Temporal and modal logic[END_REF]. Finally, Sect. 11 gives some concluding remarks and raised perspectives. To lighten the presentation of the Safety-Progress classification some concepts are presented informally, the corresponding formal definitions can be found in Appendix A. In order to facilitate the reading of this article, some proofs are sketched, complete versions can been found in Appendix B, and, the main notations used throughout the article are summarized in Appendix C.

Maintenance Mode

A motivating example

In this section, using an example, we illustrate informally that there exist interesting properties to be validated which do not belong to the safety and guarantee classes.

Let us consider a (very simple) operating system, providing three execution modes:

a non-secure mode, in which only non-secure operations (op-uns) are allowed and their results should be not encrypted (uncrypt); a secure mode, in which only secure (op-sec) operations can be performed, but such that (i) every occurrence of a secure operation should be (automati-cally) logged (log) by the system, and (ii) results of secure operations should be encrypted (crypt); a system maintenance mode, in which every operation is permitted.

Switching from the non-secure mode to the secure one needs some authentication. It is achieved by emitting a request (auth-req). Such a request can be either granted by the system (grant), or denied (deny). A logout operation (logout) allows to switch back to the non-secure mode. The maintenance mode can be accessed only from the secure mode through action maintain. Again, this access can be either granted or denied by the system. This very abstract system specification can be expressed by the finite-state automaton depicted in Fig. 1. Its alphabet is Σ = {op-uns, op-sec, auth-req, grant, deny, log, crypt, uncrypt, logout, maintain}. Square states are the accepting states. The non-secure mode (highlighted in red) consists in states {1, 4}, the secure mode (highlighted in green) in states {3, 5, 6} and the maintenance mode (highlighted in blue) in state {9}. States 2 and 8 are transient states between these modes. State 7 is an "error" state, from which no accepting state is reachable. Testing this system essentially means testing several distinct properties:

a property ψ os 1 , stating that "secure operations are not allowed in the non-secure mode"; a property ψ os 2 , stating that "the maintenance mode is accessible from the secure mode"; a property ψ os 3 , stating that "secure operations are not allowed in the non-secure mode, or, the maintenance mode is called when no operation is ongoing"; a property ψ os 4 , stating that "each secure operation performed has to be logged"; a property ψ os 5 , stating that "the user should be eventually permanently disconnected"; etc.

Property ψ os

1 is clearly a safety property: once violated during an execution sequence, it remains false (on this execution) forever. Property ψ os 2 is called a guarantee property in the Safety-Progress classification: once satisfied during an execution sequence, it remains true (on this execution) forever.

Such properties are known to be testable [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF] in the following sense: it is possible to produce a tester able to report a violation of ψ os 1 (resp., a satisfaction of ψ os 2 ) during a finite test execution. Property ψ os 4 corresponds to a so-called response property in the Safety-Progress classification. In particular, valid execution sequences with respect to ψ os 4 may contain (possibly infinitely many) invalid prefixes. Therefore, finding, during a test campaign, a finite invalid execution sequence is not a sufficient condition to reject the IUT. We shall see however in this article, that, under certain conditions, this property can be also considered as testable, and how to produce a corresponding tester. Such a result clearly extends previous work ( [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF][START_REF] Grabowski | SDL and MSC based test case generation-an overall view of the SAMSTAG method[END_REF]), and allows to test a much larger class of properties than the ones considered so far.

Preliminaries and notation

In this section, we introduce some preliminary concepts and notations.

Sequences and execution sequences

The notion of sequence is used to formalize executions. Given an alphabet of actions Σ, a sequence σ on Σ is a total function σ : I → Σ where I is either the integer interval [0, n] for some n ∈ N, or N itself; where N is the set of non-negative integers (including 0). The empty sequence is denoted by . We denote by Σ * the set of finite sequences over Σ, by Σ + def = Σ * \ { } the set of non-empty finite sequences over Σ, and by Σ ω the set of infinite sequences over

Σ. Σ * ∪ Σ ω is noted Σ ∞ . The length (number of elements) of a finite sequence σ is noted |σ|. For σ ∈ Σ + and n ∈ [0, |σ| -1], the (n + 1)- th element of σ is noted σ n . For σ ∈ Σ * , σ ∈ Σ ∞ , σ • σ is the concatenation of σ and σ . The sequence σ ∈ Σ * is a strict prefix of σ ∈ Σ ∞ (equivalently σ is a strict continuation of σ), noted σ ≺ σ , when ∀i ∈ [0, |σ| -1] : σ i = σ i and |σ| < |σ |. When σ ∈ Σ * , we note σ σ def = σ ≺ σ ∨ σ = σ . The set of prefixes of σ ∈ Σ ∞ is pref (σ) def = {σ ∈ Σ * | σ σ}. For a finite sequence σ ∈ Σ * , the set of finite continuations is cont(σ) def = {σ ∈ Σ * | σ σ }. For σ ∈ Σ ∞ \ { } and n < |σ|, σ •••n is the prefix of σ containing the n + 1 first elements.

The IUT as a generator of execution sequences

The IUT is a program P abstracted as a generator of execution sequences. During a program execution, we are interested in a restricted set of operations that may influence the truth value of the properties we want to test 5 . We abstract these operations by an alphabet Σ. We denote by P Σ a program with alphabet Σ. The set of execution sequences of P Σ is denoted by Exec(P Σ ) ⊆ Σ ∞ . This set is prefix-closed, i.e., ∀σ ∈ Exec(P Σ ) : pref (σ) ⊆ Exec(P Σ ).

We use Exec f (P Σ ) (resp. Exec ω (P Σ )) to refer to the finite (resp. infinite) execution sequences of P Σ , that is:

-Exec f (P Σ ) def = Exec(P Σ ) ∩ Σ * , -Exec ω (P Σ ) def = Exec(P Σ ) ∩ Σ ω .

Labelled Transition Systems

A Labelled Transition System (LTS) defined over an al- phabet Σ is a 4-tuple G = (Q G , q G init , Σ, -→ G ) where Q G is a non-empty set of states and q G init ∈ Q G is the initial state. -→ G ⊆ Q G × Σ G × Q G is the transition relation. For Q ⊆ Q G , we note Q def = Q G \Q , the complement of Q in Q G . Moreover, for σ ∈ Σ * of length n and q, q ∈ Q G , we note q σ -→ G q when ∃q 1 , . . . , q n-1 ∈ Q G : q σ0 -→ G q 1 ∧ q n-1 σn-1 -→ G q ∧ ∀i ∈ [1, n -2] : q i σi -→ G q i+1 . For q ∈ Q G , Reach G (q) def = {q ∈ Q G | ∃σ ∈ Σ * : q σ -→ G q } is the set of reachable states from q. For X ⊆ Q G , the set of co-reachable states from X is defined as CoReach G (X) def = {q ∈ Q G | Reach G (q) ∩ X = ∅}. For σ ∈ Σ ∞ ,
the run of σ on G is the sequence of states involved in the execution of σ on G. It is formally defined as run(σ, G)

def = q 0 • q 1 • • • where ∀i : q i σi -→ G q i+1 ∧ q 0 = q G init . An LTS G is said to be deterministic if ∀q ∈ Q G , ∀e ∈ Σ, ∀q 1 , q 2 ∈ Q G : (q e -→ G q 1 ∧ q e -→ G q 2 ) ⇒ q 1 = q 2 . Finally, G is said to be Σ -complete for Σ ⊆ Σ whenever ∀q ∈ Q G , ∀a ∈ Σ , ∃q ∈ Q G : q a -→ G q . G is said to be complete if it is Σ-complete.
Previous notations transpose to Moore automata (LTSs with output function), Streett automata (the automata used to define properties), and IOLTS (Input Output LTS) that will be introduced in the remainder of this paper.

Properties as sets of execution sequences

A finitary property (resp. an infinitary property) is a subset of execution sequences of Σ * (resp. Σ ω ) (i.e., a finitary or infinitary language). Given a finite (resp. infinite) execution sequence σ and a finitary property φ (resp. infinitary property ϕ), we say that σ satisfies φ (resp. ϕ) when σ ∈ φ, noted φ(σ) (resp. σ ∈ ϕ, noted ϕ(σ)). A consequence of this definition is that properties we will consider are restricted to linear time execution sequences, excluding properties defined on powersets of execution sequences and branching properties (cf. [START_REF] Brinksma | Temporal and modal logic[END_REF]). [START_REF] Falcone | Runtime Verification of Safety-Progress Pro-perties[END_REF] In this paper we are interested in runtime properties, namely the properties that can be used in runtime-based validation techniques (e.g., runtime verification, testing). As stated in the introduction, we need to consider both finite and infinite execution sequences that a program may produce. Runtime properties should characterize satisfaction for both kinds of sequences (finite and infinite) in a uniform way. To do so, we define r-properties as pairs Π = (φ, ϕ) ⊆ Σ * × Σ ω i.e., φ is a finitary language and ϕ an infinitary language. We say that σ ∈ Exec(P Σ ) satisfies (φ, ϕ), noted Π(σ), when σ ∈ Σ * ∧ φ(σ) ∨ σ ∈ Σ ω ∧ ϕ(σ). The negation of a finitary property φ (resp. an infinitary property ϕ) w.r.t. an alphabet Σ is Σ * \ φ (resp. Σ ω \ ϕ), denoted φ (resp. ϕ) when clear from context. The definition of the negation of an rproperty follows from the definition of the negation for finitary and infinitary properties. For an r-property (φ, ϕ), we define (φ, ϕ) as (φ, ϕ). Boolean combinations of rproperties are defined in a natural way. For * ∈ {∨, ∧},

Runtime properties

(φ 1 , ϕ 1 ) * (φ 2 , ϕ 2 ) def = (φ 1 * φ 2 , ϕ 1 * ϕ 2 ).
In the sequel, we will need the notion of positive and negative determinacy [START_REF] Pnueli | PSL Model Checking and Run-Time Verification Via Testers[END_REF], first introduced by Pnueli and Zaks to define monitorability (i.e., to state when it is worth verifying a property at runtime). Here we rephrase this notion in our context of r-properties.

Definition 1 (Positive/Negative determinacy of an r-property [START_REF] Pnueli | PSL Model Checking and Run-Time Verification Via Testers[END_REF]). An r-property Π ⊆ Σ * × Σ ω is said to be:

-positively determined by σ ∈ Σ * if ∀µ ∈ Σ ∞ : Π(σ • µ), denoted ⊕-determined (σ, Π); -negatively determined by σ ∈ Σ * if ∀µ ∈ Σ ∞ : ¬Π(σ • µ). denoted -determined (σ, Π).
Intuitively, an r-property Π is positively (resp. negatively) determined by a finite sequence σ, if σ satisfies (resp. does not satisfy) Π and every finite and infinite continuation does (resp. does not) satisfy the r-property. Remark 1. One can remark that an r-property Π is positively determined iff ¬Π is negatively determined, that is:

∀σ ∈ Σ * , ∀Π ⊆ Σ * × Σ ω : ⊕-determined (σ, Π) ⇔ -determined (σ, ¬Π).

A Safety-Progress classification for runtime techniques

The Safety-Progress (SP) classification of properties [START_REF] Manna | A Hierarchy of Temporal Properties[END_REF][START_REF] Chang | Characterization of Temporal Property Classes[END_REF] introduces a hierarchy between regular (linear time) properties 6 initially defined as sets of infinite execution sequences. The classification has been extended in [START_REF] Falcone | Runtime Verification of Safety-Progress Pro-perties[END_REF] to also deal with finite-length execution sequences by revisiting it using r-properties. In this section, we recall the necessary concepts of the extended version of the Safety-Progress classification.

Informal presentation

The Safety-Progress classification is an alternative to the classical Safety-Liveness [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF][START_REF] Alpern | Defining liveness[END_REF] dichotomy. Unlike this later, the Safety-Progress classification is a hierarchy and not a partition, and provides a finer-grain classification of properties in a uniform way according to 4 views [START_REF] Chang | The Safety-Progress Classification[END_REF]: a language-theoretic view (seeing properties as languages built using specific operators), a logical view (seeing properties as LTL formulas), a topological view (seeing properties as open or closed sets), and an automata view (seeing properties as accepted words of Streett automata [START_REF] Streett | Propositional Dynamic Logic of looping and converse[END_REF]).

Recall that the Safety-Liveness classification partitions properties into two classes: safety properties (stating that "a bad thing should not happen") and liveness properties (stating that "a good thing should eventually happen"). The Safety-Progress classification introduces four basic classes of properties that are distinguished according to how a good thing is supposed to happen during an (infinite) execution:

safety properties require that only good things happen; guarantee properties require that a good thing happens at least once; response properties require that a good thing happens infinitely often; persistence properties require that a good thing happens persistently (equivalently, to not occur a finite number of times).

Moreover, two composite classes are defined over basic classes: obligation (resp. reactivity) properties are obtained by finite Boolean combinations of safety and guarantee (resp. response and persistence) properties. Any linear-time property, i.e., that can be expressed as a set of sequences, belongs to the reactivity class.

A graphical and hierarchical representation of the Safety-Progress classification of properties is depicted in Fig. 2. A link between two classes means that the upper class strictly contains the lower one. Further details and results can be found in [START_REF] Falcone | What can you verify and enforce at runtime? Software Tools for Technology Transfer[END_REF]. Here, we consider only

Safety

Persistence Response Obligation Reactivity Guarantee Fig. 2. The SP classification the needed results from the language-theoretic and the automata views.

The language-theoretic view of r-properties

The language-theoretic view of the SP classification is based on the construction of infinitary properties and finitary properties from finitary ones. It relies on the use of four operators A, E, R, P (building infinitary properties) and four operators A f , E f , R f , P f (building finitary properties) applied to finitary properties. Formal definitions were introduced in [START_REF] Falcone | What can you verify and enforce at runtime? Software Tools for Technology Transfer[END_REF] and are recalled in Appendix A. In the following ψ ⊆ Σ * is a finitary property.

A(ψ) consists of all infinite words σ s.t. all prefixes of σ belong to ψ. E(ψ) consists of all infinite words σ s.t. some prefixes of σ belong to ψ. R(ψ) consists of all infinite words σ s.t. infinitely many prefixes of σ belong to ψ. P (ψ) consists of all infinite words σ s.t. all but finitely many prefixes of σ belong to ψ.

A f (ψ) consists of all finite words σ s.t. all prefixes of σ belong to ψ. One can observe that A f (ψ) is the largest prefix-closed subset of ψ. E f (ψ) consists of all finite words σ s.t. some prefixes of σ belong to ψ. One can observe that E f (ψ) = ψ • Σ * . R f (ψ) consists of all finite words σ s.t. ψ(σ) and there exists an infinite number of continuations σ of σ also belonging to ψ. P f (ψ) consists of all finite words σ belonging to ψ s.t. there exists a continuation σ of σ s.t. σ persistently has continuations staying in ψ.

Example 1 (Language operators). Let us illustrate the application of the previously introduced language operators on some finitary properties:

-Let us consider Σ 1 = {a, b, c} and the finitary property

ψ 1 = a * • b * + c • (c + a) * • b +
defined by the deterministic finite-state automaton (DFA) in Fig. 3a with accepting states 1, 2. We have:

-A(ψ 1 ) = a ω + a + • b ω , A f (ψ 1 ) = a * • b * , -E(ψ 1 ) = Σ ω 1 , E f (ψ 1 ) = Σ * 1 , -R(ψ 1 ) = a ω + a * • (b + (c • (a + c) * • b) • b ω , R f (ψ 1 ) = a * + a * • (b + (c • (a + c) * • b) • b * , -P (ψ 1 ) = a ω + a * • (b + (c • (a + c) * • b) • b ω , P f (ψ 1 ) = a * + a * • (b + (c • (a + c) * • b) • b * . -Let us consider Σ 2 =
{a, b}, and the finitary property ψ 2 = (a • b) + defined by the DFA depicted in Fig. 3b. We have:

(a) A ψ 1 defining ψ 1 = a * • b * + c • (c + a) * • b + 1 2 3 4 a b a b (b) A ψ 2 defining ψ 2 = (a • b) + Fig. 3. DFA for ψ 1 and ψ 2 -A(ψ 2 ) = A f (ψ 2 ) = ∅, -E(ψ 2 ) = a • b • Σ ω 2 , E f (ψ 2 ) = a • b • Σ * 2 , -R(ψ 2 ) = a • b • (a • b) ω , R f (ψ 2 ) = a • b • (a • b) * , -P (ψ 2 ) = P f (ψ 2 ) = ∅.

4.3

The automata view of r-properties [START_REF] Falcone | Runtime Verification of Safety-Progress Pro-perties[END_REF] We define a variant of deterministic and complete Streett automata (introduced in [START_REF] Streett | Propositional Dynamic Logic of looping and converse[END_REF] and used in [START_REF] Chang | The Safety-Progress Classification[END_REF]). We add to original Streett automata an acceptance condition for finite sequences in such a way that these automata uniformly define r-properties.

Definition 2 (Streett automaton). A deterministic Streett automaton

A is a tuple (Q A , q A init , Σ, -→ A , {(R 1 , P 1 ), . . . , (R m , P m )}). The set Q A is the set of states,

q A init ∈ Q A is the initial state. -→ A : Q A ×Σ → Q A is the (complete) transition function. {(R 1 , P 1 ), . . . , (R m , P m )}
is the set of accepting pairs, for i ∈ [1, m], R i ⊆ Q A and P i ⊆ Q A are the sets of recurrent and persistent states respectively. Without loss of generality, we suppose that in the considered Streett automata, all states are reachable from the initial state: Reach A (q A init ) = Q A . An automaton with m accepting pairs is called an mautomaton. A plain-automaton is a 1-automaton, and R 1 and P 1 are then referred as R and P . For an execution sequence σ ∈ Σ ω on a Streett automaton A, vinf (σ, A) denotes the set of states appearing infinitely often in run(σ, A). Definition 3 (Acceptance conditions of Streett automata). Considering an m-automaton A = (Q A , q A init , Σ, -→ A , {(R 1 , P 1 ), . . . , (R m , P m )}), the acceptance conditions are defined as follows.

-

For σ ∈ Σ ω , A accepts σ if ∀i ∈ [1, m] : vinf (σ, A) ∩ R i = ∅ ∨ vinf (σ, A) ⊆ P i .
An infinite sequence σ is accepted by A if, during the run of σ on A, the set of states visited infinitely often are either all in P i -states or contains at least one R i -state, for each i ∈ [1, m].

A f (ψ 1 ), A(ψ 1 )), (E f (ψ 2 ), E(ψ 2 )), (R f (ψ 2 ), R(ψ 2 ))
-For σ ∈ Σ * , A accepts σ if q A init σ -→ A q ⇒ ∀i ∈ [1, m] : q ∈ R i ∪ P i .
A finite sequence σ is accepted by A if the run of σ on A ends in either a P i -state or in a R i -state, for each i ∈ [1, m].

Example 2 (Acceptance conditions of Streett automata).

Following the definition of the acceptance conditions, we can determine the accepted sequences of some Streett automata:

-The Streett automaton A Π1 in Fig. 4a

A Π3 is R f (ψ 2 ) (resp. R(ψ 2 )).
As stated before, in the automata view, Streett automata are used to define r-properties:

Definition 4 (r-property defined by a Streett automaton). A Streett automaton A defines an r-property (φ, ϕ) ⊆ Σ * × Σ ω if and only if the set of finite sequences accepted by A equals φ and the set of infinite sequences accepted by A equals ϕ.

The hierarchy of r-properties

The hierarchical organization of r-properties can be seen in the language view using the operators and in the automata view using syntactic restrictions on Streett automata.

Definition 5 (Safety-Progress classes). An r-property Π, defined by

A Π = (Q A Π , q A Π init , Σ, -→ A Π , {(R 1 , P 1 ), . . . , (R m , P m )})
, is said to be:

-A safety r-property if Π = (A f (ψ), A(ψ)) for some ψ ⊆ Σ * or equivalently A Π is a plain-automaton s.t. R = ∅ and there is no transition from P to P . -A guarantee r-property if Π = (E f (ψ), E(ψ)) for some ψ ⊆ Σ * or equivalently A Π is a plain-automaton s.t. P = ∅ and there is no transition from R to R. -An m-obligation r-property if Π = m i=1 (S i (ψ i ) ∪ G i (ψ i )) or Π = m i=1 (S i (ψ i ) ∩ G i (ψ i ))
where S(ψ i ) (resp. G(ψ i )) are safety (resp. guarantee) r-properties defined over the ψ i and the ψ i ; or equivalently A Π is an m-automaton s.t. for i ∈ [1, m] there is no transition from P i to P i and from R i to R i .

P P P R R R R R R R P P P P Safety Guarantee Response Persistence
-A response r-property if Π = (R f (ψ), R(ψ)) for some ψ ⊆ Σ * or equivalently A Π is a plain-automaton s.t. P = ∅. -A persistence r-property if Π = (P f (ψ), P (ψ)) for some ψ ⊆ Σ * or equivalently A Π is a plain-automaton s.t. R = ∅.
-A reactivity r-property if Π is obtained by finite Boolean combinations of response and persistence r-properties or equivalently A Π is an unrestricted automaton.

An r-property of a given class is pure when not belonging to any other sub-class.

Example 3 (r-properties).

-The Streett automaton A Π1 in Fig. 4a is a safety automaton and defines the safety r-property (A f (ψ 1 ), A(ψ 1 )) built upon ψ 1 .

-The Streett automaton A Π2 in Fig. 4b is a guarantee automaton and defines the guarantee r-property

(E f (ψ 2 ), E(ψ 2 )) built upon ψ 2 .
-The Streett automaton A Π3 in Fig. 4c is a response automaton and defines the response r-property

(R f (ψ 2 ), R(ψ 2 )) built upon ψ 2 .
Example 4 (r-properties for the operating system). The global specification of the operating system introduced in Section 2 can be formalized as one general reactivity r-property Π op defined by the Streett automaton A Π op depicted in Fig. 5. For the sake of readability, we have represented only the most interesting transitions of the automaton. In the states where transitions are omitted for some events, there is implicitly a transition starting from this state, labelled with each omitted event, and ending in state 7. Note that, using an r-property (here through recurrent and persistent states of a Streett automaton) allow us to more precisely formalize the specification for infinite sequences. Moreover, additionally to the properties mentioned in Section 2, the automaton formalizes additional requirements. For instance, authentication granting should be "fair": the authentication request can not be denied forever (e.g., the execution (auth-req • deny) ω is not accepted by the automaton). Moreover, from this reactivity r-property, one can derive several smaller r-properties defined using Streett automata. These r-properties formalize the informal properties introduced in Section 2.

-The safety r-property Π op 1 formalizes the property ψ op 1 and is defined by States are grouped according to whether they are recurrent or not (respectively denoted by "R" and "R"), and persistent or not (respectively denoted by "P " and "P "). Arrows represent possible transitions between groups of states7 . For instance, for safety automata, there are P -states, P -states, and only R-states.

A Π op
For this kind of automata, the P -states can be distinguished according to whether P -states can be reached (the right-hand side group of states) or not (the lefthand side group of states).

To refine Fig. 2, a graphical representation of the Safety-Progress hierarchy of properties is depicted in Fig. 8: for each class of properties, characterizations are recalled in the language-theoretic and automata views, as defined in Definition 5.

Some notions of testability

Recall that Exec(P Σ ) = Exec f (P Σ ) ∪ Exec ω (P Σ ). From some finite interaction with the underlying IUT, the tester observes a sequence of events σ in Σ * . We study the conditions, for a such tester, using this sequence σ, to determine whether a given relation holds between the set of all (finite and infinite) execution sequences that can be produced by the IUT (Exec(P Σ )), and the set of sequences satisfying the r-property Π. Roughly speaking, the challenge addressed by a tester is thus to determine a

Guarantee

Response

Persistence verdict between Π and Exec(P Σ ), from a finite sequence taken from Exec f (P Σ ) 8 . Let us recall that the r-property is a pair consisting of a set of finite sequences and a set of infinite sequences. In the sequel, we shall compare this pair to the set of (finite and infinite) execution sequences of the IUT. As noticed in [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF], one may consider several possible relations between the execution sequences produced by the program and those described by the property. Those relations are recalled here in the context of r-properties.

P i P i , R i R i i [Safety i ∪ Guarantee i ] (A f (ψ), A(ψ)) (E f (ψ), E(ψ)) (R f (ψ), R(ψ)) (P f (ψ), P (ψ)) i [Response i ∪ Persistence i ] R = ∅ R = ∅, P P P = ∅, R R P = ∅
Definition 6 (Relations between IUT sequences and an r-property [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF]). The possible relations of interest between Exec(P Σ ) and Π = (φ, ϕ) are:

-Exec f (P Σ ) ⊆ φ and Exec ω (P Σ ) ⊆ ϕ: the IUT respects the r-property; all behaviors of the IUT are allowed by the r-property (denoted Exec(P Σ ) ⊆ Π).

-Exec f (P Σ ) = φ and Exec ω (P Σ ) = ϕ: the observable behaviors of the IUT are exactly those described by the r-property (denoted Exec(P Σ ) = Π).

-Exec f (P Σ ) ∩ φ = ∅ and Exec ω (P Σ ) ∩ ϕ = ∅: the behaviors expected by the r-property and those of the IUT are not disjoint (denoted Exec(P Σ ) ∩ Π = ∅).

φ ⊆ Exec f (P Σ ) and ϕ ⊆ Exec ω (P Σ ): the IUT implements the r-property; all behaviors described by the r-property are feasible by the IUT (denoted Π ⊆ Exec(P Σ )).

We use R to denote a relation ranging over the ones described in Definition 6. By R(Exec(P Σ ), Π), we denote that the relation R holds between Exec(P Σ ) and Π. The test verdict is thus determined according to the conclusions that one can obtain for the considered relation. In essence, a tester can and must only determine a verdict from a finite test execution σ ∈ Exec f (P Σ ). In Sect. 6, we will also study the conditions to state weaker verdicts on a single execution sequence.

Definition 7 (Verdicts [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF]). Given a relation R between Exec(P Σ ) and Π, and a finite test execution σ ∈ Exec f (P Σ ), the tester produces verdicts as follows:

pass if σ allows to determine that R holds; fail if σ allows to determine that R does not hold; unknown9 otherwise.

We note verdict(σ, R(Exec(P Σ ), Π)) the verdict that the observation of σ allows to determine. Let us remark the two following practical problems:

-In general, the IUT may be a program producing infinite-length execution sequences. Obviously these sequences cannot be evaluated by a tester w.r.t. Π. -Moreover, finite execution sequences contained in the r-property cannot be processed easily. For instance:

if for example a guarantee or response r-property Π the test execution exhibits a sequence σ / ∈ Π, deciding to stop the test is a critical issue. Actually, nothing allows to claim that a future continuation of the test execution would not exhibit a new sequence belonging to the r-property, i.e., σ ∈ Σ

∞ s.t. Π(σ • σ ). -conversely, for example a safety r-property Π, the test might exhibit σ ∈ Exec f (P Σ ) s.t. Π(σ), but continuing the test might also exhibit σ ∈ Σ * s.t. σ • σ ∈ Exec f (P Σ ) ∧ ¬Π(σ • σ ).
Thus, the test should be stopped only when there is no doubt regarding the verdict to be established. Following [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF], we propose a notion of testability that takes into account the aforementioned practical limitations, and that is set in the context of the Safety-Progress classification.

Definition 8 (Testability

(Q O , q O init , Σ, -→ O , Γ O ). The finite set Q O denotes the control states and q O init ∈ Q O is the initial state. The complete function -→ O : Q O × Σ → Q O is the transition function. The output function Γ O : Q O →
{pass, fail , unknown} produces verdicts in such a way that any state q emitting a pass or a fail verdict is final, i.e., ∀q ∈ Q O : Γ O (q) ∈ {pass, fail } ⇒ q e -→ O q, for any e ∈ Σ.

Definition 10 (Soundness and completeness of a test oracle). The output function Γ

O of a test oracle O = (Q O , q O init , Σ, -→ O , Γ O
) should produce verdicts in the following way:

-soundness: ∀q ∈ Q O : * Γ O (q) = pass ⇒ ∀σ ∈ Exec f (P Σ ) : q O init σ -→ O q ⇒ verdict(σ, R(Exec(P Σ ), Π)) = pass * Γ O (q) = fail ⇒ ∀σ ∈ Exec f (P Σ ) : q O init σ -→ O q ⇒ verdict(σ, R(Exec(P Σ ), Π)) = fail , -completeness: ∀σ ∈ Σ * : * σ ∈ Exec f (P Σ ) ∧ verdict(σ, R(Exec(P Σ ), Π)) = pass ⇒ ∃q ∈ Q O : q O init σ -→ O q ∧ Γ O (q) = pass * σ ∈ Exec f (P Σ ) ∧ verdict(σ, R(Exec(P Σ ), Π)) = fail ⇒ ∃q ∈ Q O : q O init σ -→ O q ∧ Γ O (q) = fail .
Intuitively, a test oracle is sound if the verdicts it produces are correct regarding the relation between Exec(P Σ ) and Π. It is complete if it produces the appropriate verdict for every finite sequence permitting so. Note that, implicitly, the unknown evaluation is never produced after a fail or pass verdict.

Testable properties without executable specification

In this section we shall see that the framework of rproperties (Sect. 4) allows to determine the testability, according to several relations between Exec(P Σ ) and Π, of the different classes of properties using positive and negative determinacy (Definition 1). Moreover, this framework also provides a computable test oracle. Furthermore, we will be able to characterize which test sequences allow to establish sought verdicts. Then, we will determine which verdict has to be produced in accordance with a given test sequence.

6.1 For the relation Exec(P Σ ) ⊆ Π

Obtainable verdicts and sufficient conditions

For the relation Exec(P Σ ) ⊆ Π, the unique verdicts that may be produced are fail and unknown. We explicit this below.

A pass verdict means that all execution sequences of the IUT P Σ belong to Π. The unique case where it is possible to establish a pass verdict is in the trivial case where Π = (Σ * , Σ ω ), i.e., the r-property Π is always satisfied. Obviously, any implementation with alphabet Σ satisfies this relation. In other cases, in practice it is impossible to obtain such a verdict (whatever is the property class under consideration), since the whole set Exec(P Σ ) is usually unknown from the tester. For instance, one can imagine a guarantee property Π s.t. first ∃σ ∈ Exec f (P Σ ) : Π(σ) (and thus ∀σ ∈

Σ ∞ : Π(σ • σ )) and second ∃σ ∈ Exec f (P Σ ) : ¬Π(σ ) and ∀σ ∈ Σ ∞ : ¬Π(σ • σ ).
Remark 2. In the following, we will also study the conditions under which it is possible to state weak pass verdicts, when reasoning on a single execution sequence of the IUT. For instance, for the previously mentioned guarantee r-property, we will produce a weak pass verdict for the sequence σ.

A fail verdict means that there exist some sequences of the program which are not in Π. In order to produce a fail verdict, it is sufficient to exhibit an execution sequence of P Σ s.t. Π is negatively determined by this sequence:

Property 1 (Sufficient condition to produce a fail verdict). Negative determinacy is a sufficient condition for a sequence to be associated to a fail verdict:

verdict(σ, Exec(PΣ) ⊆ Π) = fail if -determined (σ, Π) unknown otherwise
Hence, the aim of the test campaign will be to generate sequences σ of Σ * that negatively determine Π and to play them on the implementation. For each SP class, we state the conditions under which the properties of this class are testable, i.e., the conditions to exhibit a fail verdict.

In the language view, the testability conditions of r-properties are given on the finitary properties (ψ or ψ i for i ∈ [1, n]) over which r-properties are built. In the automate view, the testability conditions are given through syntactic criteria on the automata defining rproperties.

Theorem 1 (Testability of Exec

(P Σ ) ⊆ Π). Given A Π = (Q A Π , q A Π init , -→ A Π , {(R 1 , P 1 ), . . . , (R m , P m )}) de- fining an r-property Π built over ψ ⊆ Σ * or ψ i ⊆ Σ * for i ∈ [1, n],
according to the class of Π, the testability conditions expressed both in the language-theoretic and automata views are given in Table 1 10 .

Exec(P Σ ) ⊆ Π

Testability Condition

Testability Condition (language view) (automata view) Proof. The complete proof is given in Appendix B.1.

Safety (Af (ψ), A(ψ)) | R = ∅, P P ψ = ∅ P = ∅ Guarantee (Ef (ψ), E(ψ)) | P = ∅, R R {σ ∈ ψ | pref (σ) ∪ cont(σ) ⊆ ψ} = ∅ R \ CoReachA Π (R) = ∅ Obligation k i=1 (Si(ψi) ∪ Gi(ψ i )) k i=1 ψi ∩ {σ ∈ ψ i | pref (σ) ∪ cont(σ) ⊆ ψ i } = ∅ k i=1 (Si(ψi) ∩ Gi(ψ i )) k i=1 ψi ∪ {σ ∈ ψ i | pref (σ) ∪ cont(σ) ⊆ ψ i } = ∅ Pi Pi, Ri Ri k i=1 Pi ∩ Ri \ CoReachA Π (Ri) = ∅ Response (Rf (ψ), R(ψ)) | P = ∅ {σ ∈ ψ | cont(σ) ⊆ ψ} = ∅ R \ CoReachA Π (R) = ∅ Persistence (Pf (ψ), P (ψ)) | R = ∅ {σ ∈ ψ | cont(σ) ⊆ ψ} = ∅ P \ CoReachA Π (P ) = ∅
The proof is done according to the Safety-Progress classes.

-In the language view, for each pair of operators X f /X with X ∈ {A, E, R, P }, one can see that when a sequence is in one of the mentioned sets, the r-property (X f (ψ), X(ψ)) is negatively determined: e.g., for a safety r-property

(A f (ψ), A(ψ)) built upon ψ ⊆ Σ * , when σ ∈ ψ, we have -determined (σ, (A f (ψ), A(ψ))).
Indeed, every finite (resp. infinite) continuation of σ cannot belong to A f (ψ) (resp. A(ψ)) because it has at least one prefix not in ψ. -In the automata view, according to the syntactic restrictions on automata for Safety-Progress classes and the acceptance conditions, one can see that when a run of a sequence ends in a state in the mentioned set of states, the corresponding sequence negatively determines the underlying r-property 11 . This allows us, according to Property 1, to produce a fail verdict. For instance, for safety r-properties, when the run of a sequence σ ends in a P state, σ negatively determines the underlying r-property. Indeed, according to the acceptance criterion of Streett automata, since there is no transition from P -states to P -states, every finite and infinite continuation of σ does not satisfy the underlying property.

Example 5 (Testability of some r-properties w.r.t. the relation Exec(P Σ ) ⊆ Π). We present the testability of some r-properties introduced in Example 3. The safety r-property Π 1 is testable w.r.t. the relation Exec(P Σ1 ) ⊆ Π 1 . Indeed in the language view, the property is built on ψ 1 and there are sequences belonging to Σ * 1 \ ψ 1 (the corresponding DFA has a non accepting state). In the automata view, for A Π1 , we have 3 ∈ P (reachable from the initial state).

The guarantee r-property Π 2 is testable w.r.t. the relation Exec(P Σ2 ) ⊆ Π 2 . Indeed in the language view, the property is built on ψ 2 and there are sequences belonging 11 One can remark that, for

X ⊆ Q A Π , X \ CoReach A Π (X) = ∅ can be equivalently written {q ∈ X | Reach A Π (q) ⊆ X} = ∅. to Σ * 2 \ ψ 2 s.t.
all prefixes of theses sequences and all its continuations are also in Σ * 2 \ ψ 2 . In the automata view, for A Π2 , there is a (reachable) state in R from which all reachable states are in R: state 4.

The response r-property Π 3 is testable w.r.t. the relation Exec(P Σ2 ) ⊆ Π 3 . Indeed in the language view, the property is built on ψ 2 and there are sequences belonging to Σ * 2 \ ψ 2 s.t. all continuations of these sequences belong to Σ * 2 \ψ 2 as well. In the automata view, for A Π3 , there is a (reachable) state in R from which all reachable states are in R: state 5.

The response r-property Π 4 , defined by the Streett automaton depicted in Fig. 14b, is not testable w.r.t. the relation Exec(P Σ2 ) ⊆ Π 4 . Indeed, in the automata view, for A Π4 , we have

R \ CoReach A Π 4 (R) = ∅ since R = {2}, 1 ∈ Reach A Π 4 (2)
, and 1 ∈ R. In other words, for every finite sequence σ, there exist infinite continuations satisfying Π 4 (visiting infinitely often state 1 in the automaton) and infinite continuations not satisfying Π 4 (staying persistently in state 2 in the automaton).

Example 6 (Testability of the r-properties of the operating system w.r.t. the relation Exec(P Σ ) ⊆ Π). Similarly, we can present the testability of the r-properties for the operating system.

-The r-property Π op is testable w.r.t. the relation Exec(P Σ ) ⊆ Π op where Σ is the alphabet used in the definition of Π op . -The r-property Π op i is testable w.r.t. the relation Exec(P Σ ) ⊆ Π op i , for i ∈ [START_REF] Alpern | Defining liveness[END_REF][START_REF] Chang | Characterization of Temporal Property Classes[END_REF], where Σ is the appropriate alphabet used in the definition of the considered r-property.

-The r-property Π op 5 is not testable w.r.t. the relation Exec(P Σ ) ⊆ Π op 5 , where Σ is the alphabet used in the definition of Π op 5 .

Verdicts to deliver

We now state the verdicts that should be produced by a tester for the possibly infinite sequences of the IUT.

Exec(P Σ ) ⊆ Π

Testability Condition Testability Condition (language view) (automata view)

Safety (Af (ψ), A(ψ)) | R = ∅, P P {σ ∈ ψ | pref (σ) ∪ cont(σ) ⊆ ψ} = ∅ P \ CoReachA Π (P ) = ∅ Guarantee (Ef (ψ), E(ψ)) | P = ∅, R R ψ = ∅ R = ∅ Obligation k i=1 (Si(ψi) ∪ Gi(ψ i )) m i=1 ψ i = ∅ k i=1 (Si(ψi) ∩ Gi(ψ i )) m i=1 ({σ ∈ ψi | pref (σ) ∪ cont(σ) ⊆ ψi} ∩ ψ i ) = ∅ Pi Pi, Ri Ri m i=1 (Pi \ CoReachA Π (Pi) ∪ Ri) = ∅ Response (Rf (ψ), R(ψ)) | P = ∅ {σ ∈ ψ | pref (σ) ∪ cont(σ) ⊆ ψ} = ∅ R \ CoReachA Π (R) = ∅ Persistence (Pf (ψ), P (ψ)) | R = ∅ {σ ∈ ψ | pref (σ) ∪ cont(σ) ⊆ ψ} = ∅ P \ CoReachA Π (P ) = ∅ Table 2.
Conditions to produce a weak pass verdict for the relation Exec(P Σ ) ⊆ Π

In the language view, each testability condition is expressed as a composition of some ψ i , where the

ψ i ⊆ Σ * (i ∈ [1, n]
) are used to build the r-property. When σ belongs to Exec f (P Σ ) and the exhibited sets, the test oracle should deliver fail since the underlying r-property is negatively determined. Conversely, when σ ∈ Exec f (P Σ ) and σ is not in the exhibited sets, the test oracle can only deliver unknown.

In practice, those verdicts are determined by a test oracle, i.e., a computable function reading an interaction sequence. In our framework, test oracles are obtained from Streett automata. We defer the computation of the test oracle to Sect. 7, as we will generate the canonical tester which is a mechanism encompassing the test oracle.

Remark 3. The test oracle can be also obtained from the r-properties described in other views (language-theoretic, logical). Indeed, in [START_REF] Falcone | What can you verify and enforce at runtime? Software Tools for Technology Transfer[END_REF] we describe how to express an rproperty in the automata view from its expression in the language or the logical view.

In this part, we have clarified and extended some results of [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF] about the testability of properties w.r.t. the relation Exec(P Σ ) ⊆ Π. First, we have shown that the safety r-property (Σ * , Σ ω ) always lead to a pass verdict and is vacuously testable. Moreover, we exhibited some r-properties of other classes which are testable, i.e., some obligation, response, and persistence r-properties. The testability conditions are given in the language and automata views. We shall now go one step further in the extension of the results in [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF] by introducing a finer notion of verdict.

Refining verdicts

Similarly to the introduction of weak truth values in runtime verification [START_REF] Bauer | Comparing LTL Semantics for Runtime Verification[END_REF][START_REF] Falcone | Runtime Verification of Safety-Progress Pro-perties[END_REF], it is possible to introduce weak verdicts in testing. In this respect, stopping the test and producing a weak verdict consists in stating that the test execution sequence produced so far belongs (or not) to the property. The idea of satisfaction "if the program stops here" in runtime verification [START_REF] Bauer | Comparing LTL Semantics for Runtime Verification[END_REF][START_REF] Falcone | Runtime Verification of Safety-Progress Pro-perties[END_REF] corresponds to the idea of "the test has shown enough on the implementation" in testing. In this case, testing would be similar to a kind of "active runtime verification": one is interested in the satisfaction of one execution of the program which is steered externally by a tester. Basically, it amounts to not seeing testing as a destructive activity, but as a way to also enhance confidence in the implementation compliance w.r.t. a property.

Under some conditions, it is possible to determine weak verdicts for some classes of properties in the following sense: the verdict is expressed on one single execution sequence σ, and it does not afford any conclusion on the set Exec(P Σ ).

We have seen that, for the relation Exec(P Σ ) ⊆ Π, the only verdicts that can be produced were fail and unknown. Clearly, fail verdicts can still be produced. Furthermore, unknown verdicts can be refined into weak pass verdicts when the sequence σ positively determines the r-property. In this case, the test can be stopped since whatever is the future behavior of the IUT, it will exhibit behaviors that will satisfy the r-property. In this case, it seems reasonable to produce a weak pass verdict and consider new test executions in order to gain in confidence.

The definition of the verdict function, as given in Property 1, can be updated:

Property 2 (Sufficient conditions to produce a fail or a weak pass verdict). Positive determinacy is a sufficient condition for a sequence to be associated to a weak pass verdict. Negative determinacy remains a sufficient condition for a sequence to be associated to a fail verdict. We have, verdict(σ, Exec(P

Σ ) ⊆ Π) =    fail if -determined (σ, Π), weak pass if ⊕-determined (σ, Π), unknown otherwise.
We revisit, for each Safety-Progress class, the situations when weak pass verdicts can be produced for this relation.

Theorem 2 (Producing weak pass verdicts for the relation Exec(P Σ ) ⊆ Π). For each Safety-Progress class, the situations when weak pass verdicts can be produced are given in Table 2.

Proof. Noticing that the notions of positive and negative determinacy are dual, the proof can be conducted similarly to the proof of Theorem 1.

Corollary 1 (Testabity of Exec(P Σ ) ⊆ Π with weak verdict). Testability conditions for Exec(P Σ ) ⊆ Π augmented with weak verdicts are the disjunction of the conditions exposed in Tables 1 and2.

Proof. It is a direct consequence of Theorems 1 and 2.

Definition 11 (Test Oracle with weak verdict).

The notion of test oracle introduced in Definition 9 can be easily extended with the notion of weak pass verdict. Indeed, it suffices to require the following additional constraints relatively to the production of verdicts:

-soundness: ∀q ∈ Q O : Γ O (q) = weak pass ⇒ ∀σ ∈ Exec f (P Σ ) : q O init σ -→ O q ⇒ Π(σ) ∧ ∀σ ∈ Σ * : σ ≺ σ ⇒ verdict(σ , Exec(P Σ ) ⊆ Π) / ∈ {fail , unknown}, -completeness: ∀σ ∈ Exec f (P Σ ) ∩ Π : Π(σ) ∧ ∀σ ∈ Σ * : σ ≺ σ ⇒ verdict(σ , Exec(P Σ ) ⊆ Π) / ∈ {fail , unknown} ⇒ ∃q ∈ Q O : q O init σ -→ O q ∧ Γ O (q) = weak pass.
Soundness (resp. completeness) entails a test oracle to produce a weak pass verdict for a sequence σ only when (resp. as soon as) Π is satisfied by σ and no future continuation of σ can lead to a fail or unknown verdict.

Testability w.r.t. the relation Exec(P Σ ) = Π

The previous reasoning applies for the testability w.r.t. the relation Exec(P Σ ) ⊆ Π apply in a similar fashion. The characterization of testable r-properties is thus the same. Indeed, when one finds a sequence σ ∈ Exec f (P Σ ) s.t. it is possible to find a fail verdict for Exec(P Σ ) ⊆ Π, then this same verdict holds for Exec(P Σ ) = Π, i.e., Exec(P Σ ) ⊆ Π ⇒ Exec(P Σ ) = Π. Note that the same reasoning applies for the weak pass verdict. the results stated for the relation Exec(P Σ ) ⊆ Π, the duality within the Safety-Progress classification. Indeed, for safety and guarantee r-properties (similar duality holds for response and persistence):

Π = (A f (ψ), A(ψ)) ⇒ Π = (E f (ψ), E(ψ)).
Furthermore, one has to notice that ¬(Exec(P Σ ) ⊆ Π) ⇔ Exec(P Σ ) ∩ Π = ∅. Consequently, testability results can be obtained in a rather straightforward manner for this relation. Indeed, the testability conditions to obtain a pass verdict for the relation Exec(P Σ ) ∩ Π = ∅ are the same conditions to obtain a weak pass verdict for the relation Exec(P Σ ) ⊆ Π (expressed in Theorem 2). Moreover, we can show that there exists one guarantee r-property for which it is not possible to obtain a pass verdict. Indeed, by duality with the non-testability of (Σ * , Σ ω ) w.r.t. Exec(P Σ ) ⊆ Π, testing the guarantee r-property (∅, ∅) cannot lead to a pass verdict. Furthermore, we have shown that some r-properties of the other classes are testable 12 as well, i.e., some safety, obligation, response, and persistence r-properties. Finally, we provided testability conditions in the language and automata views. Thus, we have extended and clarified some results of [START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF].

Remark 4 (Producing a weak fail verdict for Exec(P Σ )∩ Π = ∅). By duality, and following the reasoning used to motivate the weak pass verdict for the relation Exec(P Σ ) ⊆ Π, it is possible to produce a weak fail verdict for the relation Exec(P Σ ) ∩ Π = ∅. Thus, the conditions to produce a weak fail verdict are the ones stated in Table 1. Thus the testability conditions for the relation Exec(P Σ ) ∩ Π = ∅ augmented with the weak fail verdict are similarly the disjunction of the conditions expressed in Tables 1 and2.

Example 7 (Testability of some r-properties w.r.t. the relation Exec(P Σ ) ∩ Π = ∅). We present the testability of three r-properties introduced in Example 3 w.r.t.

Exec(P Σ ) ∩ Π = ∅.
The safety r-property Π 1 built from ψ 1 , defined by the Streett automaton depicted in Fig. 4a, is not testable w.r.t. the relation Exec(P Σ1 ) ∩ Π 1 = ∅. Indeed, it does not satisfy the testability condition: the automaton defining ψ 1 does not have an accepting state reachable from the initial state s.t. it is reachable only with accepting states and s.t. all reachable states are accepting ({σ ∈ ψ 1 | pref (σ) ∪ cont(σ) ⊆ ψ 1 } = ∅). However, this property is testable with weak verdicts. Indeed, because of state 3 in A Π1 , it is possible to obtain weak fail verdicts.

The guarantee r-property Π 2 built upon ψ 2 , defined by the Streett automaton in Fig. 4b, is testable w.r.t. the relation Exec(P Σ2 ) ∩ Π 2 = ∅. Indeed, it satisfies the testability conditions for guarantee properties: the automaton defining ψ 2 has a (reachable) accepting state (ψ 2 = ∅) and R = ∅ in A Π2 . The interesting sequences to be played in order to obtain a pass verdict are those leading to state 3. Moreover, it is also possible to produce weak fail verdicts because of state 4 in A Π2 .

The response r-property Π 3 built upon ψ 2 , defined by the Streett automaton in Fig. 4c is not testable w.r.t. the relation Exec(P Σ2 ) ∩ Π 3 = ∅. Similarly, it does not satisfy the testability conditions for response properties.

Similarly, following the previous reasoning:

-The r-property Π op (resp. Π op 2 ) is testable w.r.t. the relation Exec(P Σ )∩Π op = ∅ (resp. Exec(P Σ )∩Π op 2 = ∅) where Σ is the appropriate alphabet used in the definition of the considered r-property.

-The r-property Π op i is not testable w.r.t. the relation [START_REF] Cerná | Relating the hierarchy of temporal properties to model checking[END_REF][START_REF] Chang | Characterization of Temporal Property Classes[END_REF][START_REF] Chang | The Safety-Progress Classification[END_REF], where Σ is the appropriate alphabet used in the definition of the considered r-property.

Exec(P Σ ) ∩ Π op i = ∅, i ∈ [1,

Testability w.r.t. the relation Π ⊆ Exec(P Σ )

It is not possible to obtain verdicts for this relation in the general case. We explicit this below.

In order to obtain a pass verdict for this relation, it would require to prove that all execution sequences described by the property are sequences of the program. This is impossible as soon as the set of sequences described by the r-property is infinite.

In order to obtain a fail verdict, it would require to prove that at least one sequence described by the rproperty cannot be played on the implementation. Even if one finds an execution sequence of the implementation not satisfying the r-property, it does not afford to state that the relation does not hold. Indeed, since the IUT may be non deterministic, another execution of the implementation could exhibit such a sequence. Producing a fail verdict would require a determinism hypothesis on the implementation.

Summary

In this section, the conditions for the testability of properties w.r.t. four relations of interest have been stated. Moreover, the use of a weaker notion of verdict has been motivated and conditions to produce them have been provided.

Automatic test generation w.r.t. the relation Exec(P Σ ) ⊆ Π

In this section, we address test generation for the testing framework introduced in this paper. Here, test generation is based on r-properties, and the purpose of the test campaign is to determine verdicts for a relation between a testable r-property and an IUT. Before entering into the details, we first discuss informally some practical constraints that have to be taken into account for test generation. Then, we will be able to compute the canonical tester (i.e., the most general tester for the relation) (Sect. 7.1), discuss test selection (Sect. 7.2). We focus on test generation w.r.t. the relation Exec(P Σ ) ⊆ Π. Automatic test generation with respect to the relation Exec(P Σ ) ∩ Π = ∅ can be simply derived by duality.

Which sequences should be played? The sequences of interest to play on the IUT are naturally those leading to a fail or a weak pass verdict and these sequences can be used to generate test cases. In the language view (resp. automata view), these sequences are those belonging to the exhibited sets (resp. leading to the exhibited set of states) in testability conditions given in Tables 1 and2. For instance, for a safety r-property Π S = (A f (ψ), A(ψ)) built upon ψ, and defined by a safety automaton A Π S , one should play sequences in ψ or equivalently those leading to P in A Π S .

When to stop the test? When the tested program produces an execution sequence σ ∈ Σ * , a raised question is when to safely stop the test. Obviously, a first answer is when a fail or weak pass verdict has been issued since these verdicts are definitive. Although in other cases, when the test interactions produced some test sequences leading so far to unknown evaluations, the question prevails. It remains to the tester appraisal to decide when the test should be stopped (see Sect. 7.2).

Alphabet and test architecture. In order to address test generation, we will need to distinguish inputs and outputs and the alphabet of the IUT and the r-property. The alphabet Σ of the property is now partitioned into Σ ? (input actions) and Σ ! (output actions). The alphabet of the IUT becomes Σ IU T and is partitioned into Σ IU T ? (input actions) and Σ IU T ! (output actions) with Σ ? = Σ IU T ? and Σ ! = Σ IU T ! . As usual, we also suppose that the behavior of the IUT can be modeled by an IOLTS I = (Q I , q I init , Σ IU T , -→ I ). We do not require the IUT to be input-complete. If the IUT refuses an input, the test execution terminates and the associated verdict is the last produced one (before trying to emit the input), i.e., an unknown verdict. We do not assume neither the IUT to be deterministic.

Computation of the canonical tester

We propose a methodology to build the canonical tester for our framework. The canonical tester for a relation R between an IUT P Σ and an r-property Π is purposed to detect all verdicts for the relation between the r-property and all possible test executions that can be produced with P Σ .

We define canonical testers from Streett automata. To do so, we will reuse a partition of the set of states Definition 12 (Good and bad states). For a Streett automaton

A Π = (Q A Π , q A Π init , Σ, -→ A Π , {(R 1 , P 1 ), . . . , (R m , P m )}), the sets G A Π , G A Π c , B A Π c , B A Π form a par- tition of Q A Π
and designate respectively the good (resp. currently good, currently bad, bad) states:

-G A Π def = {q ∈ Q A Π ∩ m i=1 (R i ∪ P i ) | Reach A Π (q) ⊆ m i=1 (R i ∪ P i )}; -G A Π c def = {q ∈ Q A Π ∩ m i=1 (R i ∪ P i ) | Reach A Π (q) ⊆ m i=1 (R i ∪ P i )}; -B A Π c def = {q ∈ Q A Π ∩ m i=1 (R i ∩ P i ) | Reach A Π (q) ⊆ m i=1 (R i ∩ P i )}; -B A Π def = {q ∈ Q A Π ∩ m i=1 (R i ∩ P i ) | Reach A Π (q) ⊆ m i=1 (R i ∩ P i )}.
Informally, for an r-property Π defined by A Π , a state q ∈ Q A Π is: It is possible to show that if a sequence σ reaches a state in B A Π (resp. G A Π ), then the underlying property Π is negatively (resp. positively) determined by σ.

-in G A Π (

Lemma 1 (Good and Bad states vs determinacy).

Given σ ∈ Σ * , a Streett automaton A Π defining an rproperty Π, and q ∈ Q A Π , we have:

q ∈ G A Π ⇔ ∀σ ∈ Σ * : q A Π init σ -→ A Π q ⇒ ⊕-determined (σ, Π); q ∈ B A Π ⇔ ∀σ ∈ Σ * : q A Π init σ -→ A Π q ⇒ -determined (σ, Π).
Proof. The lemma has been proved in [START_REF] Falcone | What can you verify and enforce at runtime? Software Tools for Technology Transfer[END_REF] in a different context, we propose a proof in Appendix B.2 for the sake of completeness. The proof uses the acceptance conditions of Streett automata, and the fact that we use complete and deterministic automata.

The canonical tester is defined as follows. One can note that the notion of canonical tester is a generalization of the notion of test oracle introduced in Definition 9.

Definition 13 (Canonical Tester). Given a Streett m-automaton

A Π = (Q A Π , q A Π init , -→ A Π , {(R 1 , P 1 ), .
. . , (R m , P m )}) defining a testable r-property Π, the associated canonical tester is the Moore automaton T = (Q T , q T init , Σ, -→ T , Γ T ) where Γ T : Q T → {fail , weak pass, unknown} is the output function producing verdicts and is defined as follows:

-Q T = Q A Π ; -q T init = q A Π init ; --→ T =-→ A Π ; -for q ∈ Q T , Γ T (q) =    unknown when q ∈ B A Π c ∪ G A Π c , fail when q ∈ B A Π , weak pass when q ∈ G A Π .
A Streett automaton is simply transformed into a canonical tester by defining verdicts for its states according to the partition of bad states (in B A Π ) and good states (in G A Π ). They are assigned respectively the fail and weak pass verdicts, while all other states are given the unknown verdict. Note that the test can be stopped when reaching bad or good states. This construction of canonical testers is illustrated in Fig. 9 for the automata dedicated to basic classes of properties (see Fig. 6). The canonical tester built from A Π1 , the Streett safety automaton defining Π 1 , is s.t. the state 3 (a bad state) is assigned the fail verdict.

The canonical tester built from A Π2 , the Streett guarantee automaton defining Π 2 , is s.t. the state 5 (a bad state) is assigned the fail verdict and state 3 (a good state) is assigned the weak pass verdict.

The canonical tester built from A Π3 , the Streett response automaton defining Π 3 is s.t. the state 5 (a bad state) is assigned the fail verdict.

Example 9 (Canonical Testers). The canonical tester for the global specification of the operating system defined by the Streett automaton in Fig. 5 is depicted in Fig. 11. The alphabet partitioning is Σ IU T ? = {?maintain,?req-auth, ?op-sec,?op-uns,?logout} and Σ IU T ! = {!uncrypt,!crypt, !deny,!grant}. Assignments to unknown are omitted for readability.

Similarly, the canonical testers for the r-properties of the operating system are depicted in Fig 12.

Test selection

For a given r-property, the set of potential test sequences to be played is potentially infinite. The purpose of test selection is to produce a (finite) set of test cases s.t. any test case is controllable [START_REF] Jard | TGV: theory, principles and algorithms[END_REF] (it has no choice between the inputs it provides to the IUT) and should produce a sound verdict. Note that a test selection algorithm usually targets a particular verdict, that could be either fail or weak pass in our context. In this case, the Streett automaton describing the property under scrutiny allows to prune the execution sequences that not do lead to the targeted verdict.

A generic test selection algorithm can be viewed as a (non-deterministic) transformation of the canonical tester T = (Q T , q T init , Σ, -→ T , Γ T ) to produce a test case as a controllable IOLTS T C = (Q T C , q T C init , Σ, -→ T C , Γ T C ) such that each execution sequence of T C corresponds to a test execution. States of T C are some states of T . An additional verdict called inconc (inconclusive) replaces the unknown verdict in states from which the targeted verdict cannot be reached anymore. Now, the set of possible verdicts becomes {fail , pass, inconc, unknown}. This algorithm is informally described below (assuming that the target verdict is fail , thus B A Π states):

1. Define Inconc def = Q T \ CoReach T (B A Π )
as the set of states from which the fail verdict is not reachable. 2. Define the output function of TC such that ∀q ∈ Q T \ Inconc : Γ TC (q) = Γ T (q) and ∀q ∈ Inconc : Γ TC (q) = inconc. 3. Remove in -→ TC transitions from -→ T labelled by an input action of the IUT and whose target state is in Inconc: ∀e ∈ Σ IU T ?

, ∀q, q ∈ Q TC :

(q e -→ T q ∧ q ∈ Inconc) ⇒ (q, e, q ) ∈-→ TC (while transitions of -→ T labelled by an output action of the IUT and whose target state is in Inconc are kept in -→ TC ). 4. Make TC controllable, i.e., ensure that it satisfies:

∀e 1 , e 2 ∈ Σ IU T ? , ∀q, q 1 , q 2 ∈ Q TC : (q e1 -→ TC q 1 ∧ q e2 -→ TC q 2 ) ⇒ (q 1 = q 2 ∧ e 1 = e 2 ).
Roughly speaking, based on items 1. and 2., the test selection allows to stop the test and deliver an inconc verdict whenever it is no more possible for the tester to produce a sequence that negatively or positively determines the underlying property. Item 3. says that Inconc states are reached only after outputs, because the tester control inputs it provides and thus may avoid falling in Inconc with inputs.

Example 10 (Test sequences). Applying the test selection algorithm to the various examples we proposed is straightforward. For instance, for A Π op 1 , from the controllable canonical tester, possible test sequences (that can serve as a basis for test cases) include the sequences in (?op-uns•!uncrypt) * •?op-uns•(!crypt+?op-sec). More generally, it consists in generating sequences ending in a verdict state on the controllable canonical tester.

Test selection plays also a particular role to state weak pass verdicts. Indeed, when dealing with sequences satisfying an r-property so far and not positively determining it, test selection should plan the moment for stopping the test. It can be, for instance, when the test lasted more than a given expected duration or when the number of interactions with the IUT reaches a given bound. However, one should not forget that there might exist a continuation, that can be produced by letting the test execution continue, not satisfying the r-property or even

!deny

Fig. 11. Canonical tester for the global specification of the operating system negatively determining it. Here, it thus remains to the tester expertise to state the halting criterion (possibly using quiescence, see Sect. 8).

Remark 5 (More advanced test selection). In practice, one may use the underlying Streett automaton to refine the test selection algorithm by, for instance, further constraining the states that should be visited during a test.

Introducing quiescence

We show in this section how the test generation technique proposed in Sect. 7 can be improved when some notion of quiescence (i.e., an explicit lack of response from the IUT) can be taken into account.

The notion of quiescence in our framework

Quiescence [START_REF] Tretmans | Test generation with inputs, outputs, and quiescence[END_REF][START_REF] Jard | TGV: theory, principles and algorithms[END_REF] was introduced in conformance testing in order to represent IUT's inactivity. In practice, several kinds of quiescence may happen (see [START_REF] Jard | TGV: theory, principles and algorithms[END_REF] for instance). Here we distinguish two kinds of quiescence. Outputlocks (denoted δ o ) represent the situations where the IUT is waiting for an input and produces no outputs. Deadlocks (denoted δ d ) represent the situations where the IUT cannot interact anymore, e.g., its execution is terminated or it is deadlocked. In practice, the observation and the distinction of these two kinds of quiescence require the following hypothesis on the test architecture. First, we suppose the existence of a timer indicating, when not expired, that the IUT may still produce an output. Second, we suppose to be able to observe whether or not the IUT is ready to receive an input. This latter hypothesis boils down to the observation of this Boolean information on the IUT. Then, if the timer is expired and the IUT is still able to receive an input, this means that the IUT is in outputlock. If the timer is expired and the IUT is not ready to receive an input, this means that the IUT is in deadlock or has finished its execution. Thus, we introduce those two events in the output alphabet of the IUT. We have now the following additional alphabets:

Σ IU T !,δ def = Σ IU T ! ∪ {δ o , δ d }, Σ IU T δ def = Σ IU T !,δ ∪ Σ IU T ?
. We also have to distinguish the set of traces of the IUT from the set of potential interactions with the IUT. This latest is based on the observable behavior of the IUT and potential choices of the tester. The set of executions of the IUT is now Exec(P Σ IU T ) ⊆ (Σ IU T δ ) ∞ . However, the set of possible interactions of the tester with the IUT is

Inter (P Σ IU T ) def = (Σ IU T + δ o ) * • (δ d + ),
i.e., the interactions of the tester with IUT are s.t. the tester can observe IUT's outputlocks and may be ended by the observation of an outputlock, a deadlock, or program termination. When considering quiescence, characterizing testable properties now consists in comparing the set of interactions with the set of sequences described by the r-property. The intuitive ideas are the followings:

-The tester can observe finished executions of the IUT with δ d . In this case, the IUT has run a finite execution. In some sense, the played sequence determines negatively or positively the r-property depending on whether or not it satisfied the r-property. -The tester can decide to terminate its interaction with the program when observing an outputlock. When the tester played a sequence s.t. the underlying r-property is not satisfied and observes an outputlock, the played sequence negatively determines the r-property. Indeed, with no further action of the tester, the IUT is blocked in a state in which the underlying r-property is not satisfied.

Equivalently, in a more intuitive way, quiescence is forbidden in currently bad states and allowed in currently good states. The notion of negative determinacy is now modified in the context of quiescence as follows. Definition 14 (Determinacy with quiescence). An r-property Π defined over Σ is said to be negatively determined upon quiescence by σ ∈ Inter (P

Σ IU T \ {!grant,!deny} !grant Σ IU T ?maintain !grant Σ IU T Σ IU T \ {?logout,?auth-req} ?logout Σ IU T \ {?maintain,?logout,!grant} Σ IU T \ {!grant} (c) Canonical tester for A Π op
Inter (P Σ IUT ) ⊆ Π Testability Condition on the property Safety (Af (ψ), A(ψ)) ψ = ∅ Guarantee (Ef (ψ), E(ψ)) {σ ∈ ψ | pref (σ) ⊆ ψ}} = ∅ Obligation k i=1 (Si(ψi) ∪ Gi(ψ i )) k i=1 ψi ∩ {σ ∈ ψ i | pref (σ) ⊆ ψ i = ∅ k i=1 (Si(ψi) ∩ Gi(ψ i )) k i=1 ψi ∪ {σ ∈ ψ i | pref (σ) ⊆ ψ i } = ∅ Response (Rf (ψ), R(ψ)) ψ = ∅ Persistence (Pf (ψ), P (ψ)) ψ = ∅
Σ IU T ) (denoted -determined-q(σ, Π)) if -determined (σ ↓ Π , Π) ∨ (|σ| > 1 ∧ σ |σ|-1 ∈ {δ d , δ o } ∧ ¬Π(σ ↓ Π ))
where σ ↓ Π is the projection of σ on the vocabulary of Π, i.e., with δ o and δ d erased. The definition of positive determinacy is modified in the same way.

For the proposed approach, the usefulness of quiescence lies in the fact that the current test sequence does not have any continuation. Consequently, testability conditions may be weakened. Indeed, when one has determined that the current interaction with the IUT is over, it is not necessary to evaluate the satisfaction of the rproperty anymore. In some sense, it amounts to consider that the evaluation produced by the last event before observing quiescence "terminates" the execution sequence (and there is no continuation). For instance, if the rproperty is not satisfied after the last interaction, then the r-property is negatively determined by it.

Revisiting previous results for the inclusion relation

With quiescence, the purpose of the tester is now to "drive" the IUT in a state in which the underlying rproperty is not satisfied, and then potentially observe quiescence, i.e., find a sequence that negatively determines the property upon quiescence. Informally, the testability condition relies now on the existence of a sequence s.t. the r-property is not satisfied. Testability results, upon the observation of quiescence and in order to produce fail verdicts when the tested r-property is not satisfied, are updated using the notion of negative determinacy with quiescence as shown in Table 3. From these testability conditions, and using the definition of negative determinacy with quiescence, we can deduce the sequences that should be played in order to obtain a fail verdict. Two kinds of sequences may lead to a fail verdict:

the first ones, when projected on the vocabulary of the property, negatively determine it (as previously); the second ones are such that the prefixes of these sequences containing all events but the last one do not satisfy the property and the last event is either an outputlock or a deadlock.

It is then rather easy to give a characterization of these sequences in the language view. For instance:

for safety r-properties: {σ ∈ Inter | σ ↓ Π ∈ ψ}, for guarantee r-properties:

{σ ∈ Inter | σ ↓ Π ∈ ψ ∧ pref (σ ↓ Π ) ∪ cont(σ ↓ Π ) ⊆ ψ} ∪{σ • (δ o + δ d ) ∈ Inter | σ ↓ Π ∈ ψ ∧ pref (σ ↓ Π ) ⊆ ψ},
for response and persistence r-properties:

{σ ∈ Inter | σ ↓ Π ∈ ψ ∧ cont(σ ↓ Π ) ⊆ ψ} ∪ {σ • (δ o + δ d ) ∈ Inter | σ ↓ Π ∈ ψ}.
where Inter (P Σ IU T ) is denoted Inter for the sake of readability. These sequences are characterized in an easier way on the canonical tester. Now it is possible to adapt the construction of the canonical tester so as to take quiescence into consideration:

Definition 15 (Canonical Tester with quiescence). The definition of the canonical tester construction proposed in Definition 13 is updated as follows:

-Two new states q fail and q wpass are added to Q T such that Γ T (q fail ) = fail and Γ T (q wpass ) = weak pass, -The following transitions are added to -→ T :

-

∀q ∈ B A Π c : q δo -→ T q fail ∧ q δ d -→ T q fail , -∀q ∈ G A Π c : q δo -→ T q ∧ q δ d -→ T q wpass , -∀e ∈ Σ IU T : q fail e -→ T q fail ∧ q wpass e -→ T q wpass .
In a currently bad state, the observation of quiescence produces a fail verdict since the underlying property is negatively determined upon quiescence. In other words, the tester can legitimately stop the interaction and let the IUT in a state in which the underlying property is not satisfied. In a currently good state, the observation of a deadlock (or program termination) produces a weak pass verdict since the underlying property is positively determined upon quiescence: the current interaction sequence is satisfying the underlying property and there will be no possible continuation of this interaction. However, in a currently good state, when observing an outputlock, the canonical tester stays in the same state. Indeed, stopping the tester would be a decision of the tester and not one of the implementation. Illustrations of the construction of the canonical tester for basic classes with quiescence are given in Fig. 13, where the original (resp. modified) transitions from the Streett automaton are in plain (resp. dotted) lines.

Example 11 (Testability with quiescence). We illustrate the usefulness of quiescence by showing how using quiescence makes some properties testable, although they were not testable initially.

Consider the IUT depicted in Fig. 14a with observable actions Σ IU T ? = {?a} and Σ IU T ! = {!b}. This IUT waits for an ?a, produces a !b, and then non deterministically terminates or waits for an ?a, and repeats the behavior consisting in receiving an ?a and producing a !b. The executions and possible interactions with the tester are given in Fig. 15 ("?" and "!" are not represented and x & stands for x + ). Now let us consider the r-property Π 4 defined by the Streett automaton A Π4 depicted in Fig. 14b. Its vocabulary is {?a, !b}, and it has one recurrent state: R = {1}. The underlying r-property states that every input ?a

q wpass P weakpass P unknown P fail δ o δ d q fail R weakpass R fail R unknown δ d , δ o q fail q wpass R unknown R unknown R weakpass R fail δ o , δ d δ o δ d q fail
q wpass P weakpass P fail

P unknown P unknown δ o , δ d δ o δ d

Safety

Guarantee Response Persistence

q wpass q fail !b, !δ o ?a !δ d !b ?a !δ d , !δ o Σ IU T Σ IU T (c) Canonical tester for Π 4 14.
Illustrating the usefulness of quiescence

Exec(P Σ IU T ) = δo & • a & + a • b • (δ d + δo & ) • (a • δo & • ((a • b) & ) * * • a & ) & Inter (P Σ IU T ) = δo & • (a • b) & • (δ d + δo & ) • (a • δo & • ((a • b) & ) * * • δo & ) & & Fig. 15.
Execution and interaction sequences of the IUT of Fig. 14a should be acknowledged by an output !b. This property is not testable under the conditions expressed in Sect. 6, see Example 5. However, this r-property is testable with quiescence. One can observe that Inter (P Σ IU T ) ⊆ Π 4 because of the existence of ?a•!b•?a•!δ o in Inter (P Σ IU T ). Indeed, we have:

-determined-q(?a•!b•?a•!δ o , Π 4 ) since the last event of ?a•!b•?a•!δ o ) is δ o and ¬Π 4 (?a•!b•?a).
The synthesized canonical tester, obtained following Definition 15, is depicted in Fig. 14c.

Example 12 (Canonical Testers with quiescence for the operating system). The canonical tester for the global specification, obtained following Definition 15, is depicted in Fig. 16a. As we can see, using quiescence allows us to test additional behaviors of the operating system. Moreover, following the same reasoning used for Π 4 , using quiescence makes the r-property Π op 5 testable. The corresponding canonical tester is depicted in Fig. 16b.

Related work and discussion

In this section we overview related work or work that may be leveraged by the results proposed in this paper. Then, we propose a discussion on the results afforded by this paper.

Conformance testing

The goal of conformance testing is to check that the behavior of a real software or hardware implementation is correct w.r.t. its specification. Correctness is checked through the observable actions of the implementation (its internal behavior is unknown). In formal conformance testing, one general correctness relation is the so-called ioco relation [START_REF] Tretmans | A formal approach to conformance testing[END_REF], stating that the implementation produces outputs as prescribed in the specification. In the context of ioco, there are several kinds of outputs: the implementation's outputs or quiescence. Quiescence models several sorts of observable inactivity of the system and is practically observed by timers. Roughly speaking, a possible approach to classical conformance testing (see e.g., [START_REF] Jard | TGV: theory, principles and algorithms[END_REF]) proceeds as follows. Starting from the IOLTS specification S = (Q S , q S init , Σ, -→ S ) of the IUT, one has first to build ∆(S), the suspended IOLTS corresponding to S, obtained by adding a new observable output action δ and making IUT's inactivity explicit. This automaton is then determinized into S = Det(∆(S)), thus representing the observable behavior of the IUT.

Classical conformance testing falls in the scope of our framework and can be easily expressed. Indeed, for a specification S, the conformance of an IUT P Σ to S amounts to asserting the ⊆ relation between Exec(P Σ ) and an r-property built from S. We start from the IOLTS S expressed over Σ = Σ S ? ∪ Σ S ! and then build ∆(S) q fail q wpass ?logout,!deny,!grant ?auth-req !deny,?logout !grant !grant,!deny,?auth-req ?logout

Σ IU T !deny !δ d !δ d !δ d !δ d !δ o !δ o !δ o !δ d , !δ o !δ d , !δ o Σ IU T Σ IU T Σ IU T Σ IU T
!δ d !δ d , !δ o !δ d , !δ o !δ o Σ IU T Σ IU T
(b) Canonical tester for Π op 5 Fig. 16. Canonical testers with quiescence for the operating system and its determinized suspension IOLTS S = Det(∆(S)). Then, we consider the r-property Π defined by the Streett safety automaton

A Π = (Q A Π , q A Π init , -→ A Π , {(∅, P )}) s.t. -Q A Π = Q S ∪ {sink }, with sink / ∈ Q S , --→ A Π =-→ S ∪ {(q, e, sink ) | q ∈ Q S ∧ e ∈ Σ S ! ∪ {δ} ∧ ¬∃q ∈ Q S : q e -→ S q }, -P = Q S .
Finally, we can build the IOLTS corresponding to the canonical tester following Definition 13. When emitting fail verdicts this canonical tester exactly detects violations of the conformance relation.

Testing oriented by properties for generating test purposes

One of the limits of conformance testing [START_REF] Tretmans | A formal approach to conformance testing[END_REF][START_REF] Tretmans | Test generation with inputs, outputs, and quiescence[END_REF] lies in the size of the generated test suite which can be infinite or impracticable. Some testing approaches oriented by properties were proposed to face off this limitation by focusing on critical properties. In this case, properties are used complementary to the specification in order to generate test purposes which will be then used to conduct and select test cases. The goal of test purposes is to select a subset of test cases and their behaviors. Thus, a test purpose allows to evaluate specific features of the IUT. Once the test purposes are generated, a selection of test cases is possible using classical techniques defined on transition systems [START_REF] Jard | TGV: theory, principles and algorithms[END_REF][START_REF] De Vries | Towards formal test purposes[END_REF]. For instance, in [START_REF] Fernandez | Property oriented test case generation[END_REF], Fernandez et al. present an approach allowing to generate test cases using LTL formula as test purposes. For a (non exhaustive) presentation of some general approaches, the reader is referred to [START_REF] Patricia | Towards property oriented testing[END_REF].

Since these approaches are aimed to generate test purposes from properties, the testability of properties is deservedly left aside. One is interested in the satisfaction of a test case execution w.r.t. the considered property.

Combining testing and formal verification

In [START_REF] Constant | Integrating Formal Verification and Conformance Testing for Reactive Systems[END_REF], the complementarity between verification techniques and conformance testing is studied. Notably, the authors showed that it is possible to detect (using testing) violations of safety (resp. satisfaction of co-safety) properties on the implementation and the specification. As co-safety properties in the Safety-Liveness classification are guarantee properties in the Safety-Progress classification, the framework proposed in [START_REF] Constant | Integrating Formal Verification and Conformance Testing for Reactive Systems[END_REF] addresses only a subset of the properties stated as testable in this paper. The work proposed in [START_REF] Constant | Integrating Formal Verification and Conformance Testing for Reactive Systems[END_REF] can then be leveraged by the work proposed in this paper.

Requirement-Based testing

In requirement-based testing, the purpose is to generate a test suite from a set of informal requirements. For instance, in [START_REF] Rajan | Model Validation using Automatically Generated Requirements-Based Tests[END_REF][START_REF] Pecheur | A Formal Analysis of Requirements-based Testing[END_REF], test cases are generated from LTL formula using a model-checker. Those approaches were interested in defining a syntactic test coverage for the tested requirements. Test case generation is driven by some test coverage criterion and no notion of testability is considered.

Property testing without a behavioral specification

Some previous approaches tackle the problem of testing properties on systems without behavioral specification. These approaches used the notion of tiles which are elementary test modules testing specific parts of an implementation and which can be combined to test more complex behaviors. A description of a tile-based approach was provided in [START_REF] Darmaillacq | Test generation for network security rules[END_REF] and formalized using a process algebra dedicated to testing [START_REF] Falcone | A test calculus framework applied to network security policies[END_REF]. Later [START_REF] Falcone | A Compositional Testing Framework Driven by Partial Specifications[END_REF], Falcone et al. have shown that this approach can be generalized to other formalisms (LTL and extended regular expressions) and that the test can be executed in a decentralized fashion. In [START_REF] Darmaillacq | Test Generation and Execution for Security Rules in Temporal Logic[END_REF], Darmaillacq et al. provided a case study dedicated to testing network security policies.

These approaches focused on deriving concrete test cases, given a property. No testability notion is associated to the considered properties. Moreover, in these approaches, the goal of a test execution is to determine the satisfaction of one execution w.r.t. the property without considering the whole set of execution sequences of the IUT.

Using the Safety-Progress classification in validation techniques

The Safety-Progress classification of properties is rarely used in validation techniques. We used (e.g., [START_REF] Falcone | Runtime Verification of Safety-Progress Pro-perties[END_REF]) the Safety-Progress classification to characterize the sets of properties that can be verified and enforced at system runtime. In some sense, this previous endeavor similarly addressed the expressiveness question for runtime verification and runtime enforcement. In the light of the results afforded by [START_REF] Falcone | Runtime Verification of Safety-Progress Pro-perties[END_REF] and this paper, we can remark that these three runtime-based validation techniques have different "expressiveness", i.e., the kind of properties that can be handled by these techniques are rather different.

In [START_REF] Cerná | Relating the hierarchy of temporal properties to model checking[END_REF], Cerná and Pelánek classified linear temporal properties according to the complexity of their verification. The motivation was to study the emptiness problem used in model-checking, according to the various classes. For this purpose, the authors introduced two additional views to the hierarchy. The first one is an extension of the original automata view in which temporal properties are characterized according to new acceptance conditions (Büchi, co-Büchi, weak, and terminal automata). The second one is an extension of the original logical view in which the authors organized temporal logic formula into a hierarchy according to alternation depth of temporal operators Until and Release.

Discussion

Several approaches fall in the scope of the generic one proposed in this paper. For instance, our results apply and extend the approach where verification is combined to testing as proposed in [START_REF] Constant | Integrating Formal Verification and Conformance Testing for Reactive Systems[END_REF]. Furthermore, this approach leverages the use of test purposes [START_REF] Koch | Autolink: A tool for automatic test generation from SDL specifications[END_REF][START_REF] Jard | TGV: theory, principles and algorithms[END_REF] in testing to guide test selection. Indeed, the characterization of testable properties gives assets on the kind of test purposes that can be used in testing. Moreover, the properties considered in this paper are framed into the Safety-Progress classification of properties [START_REF] Manna | A Hierarchy of Temporal Properties[END_REF][START_REF] Chang | Characterization of Temporal Property Classes[END_REF] which is equivalently a hierarchy of regular properties. Thus the results proposed by this paper concern previous depicted approaches in which the properties at stake can be formalized by a regular language. Furthermore, as we have seen in Sect. 9.1, classical conformance testing falls in the scope of the framework proposed by this paper.

10 Implementation: Java-PT In this section we present the prototype tool Java-PT: Properties and their Testability with Java, an implementation of the previously described testing framework. It is mainly purposed to address testability issues w.r.t. an r-property under consideration. In particular, it allows to answer the following questions: The tool is developed in the Java programming language and uses XML13 , XSLT 14 , XStream15 as underlying supporting technologies. An overview of the architecture of Java-PT is given in Fig. 17. In the remainder of this section, we shall describe its functioning principle and its architecture.

The first step for a user before using the tool is to design an r-property that is purposed to be processed by the tool. The property is defined by a Streett automaton (see Sect. 10.

for examples).

A model for automata-based objects. The tool Automaton Models of Java-PT consists of a hierarchy of classes modelling several entities (alphabet, states, and their transitions) related to the kinds of automata we consider (Streett and DFA). Those classes are used at several levels in Java-PT.

We also have implemented a component that provides means to make objects persistent in XML, i.e., being able to save and load automata from their description in a XML file. This utility consists in configuring and customizing the XStream library to realize serialization and deserialization. Some utilities. The module Utilities is used by the module Testability of Properties core when processing properties. It contains the implementation of a set of useful operations on automata such as the computation of reachable states and the computation of the class of the automaton.

The main module: Testability of Properties core. This modules leverages the modules Automaton Models and Utilities. It consists mainly in implementing the previous testability conditions.

Examples

In this section, we present some typical use cases of Java-PT. Examples presented in this paper (and other examples) can be found in the distribution of Java-PT, together with a complete user manual.

Let us come back to the r-properties Π 1 and Π 2 of Example 3. As seen in Sect. 6, these r-properties are testable w.r.t. the relation Exec(P Σ ) ⊆ Π. Those rproperties are defined by their Streett automata described by the XML files in Fig. 18. Processing these properties with Java-PT is represented in Fig. 19, where:

option -in P.xml provides an input property Π to be processed (in the file P.xml); option -dc computes the class of this property (according to the Safety-Progress classification); option -it R asks if this property is testable according to relation R (where R is encoded as an integer, e.g., 1 means Exec(P Σ ) ⊆ Π).

Conclusion and perspectives

Conclusion.

In this paper, we study the classes of testable properties. We use a testability notion depending on a relation between the set of execution sequences that can be produced by the underlying implementation and the considered r-property. Leveraging the notions of positive and negative determinacy of properties, according to the relation of interest, we identify the testable fragments for each Safety-Progress class. Moreover we have seen that the framework of r-properties in the Safety-Progress classification provides a canonical tester able to produce a verdict depending on some finite interaction between the tester and the IUT. Furthermore, we also propose some conditions under which it makes sense for a tester to state weak verdicts. Besides, we address test generation for the general testing framework leveraged by properties. Finally, we have implemented the results of this paper in an available prototype tool.

Perspectives. A first research direction is to investigate the set of testable properties for more expressive formalisms. Indeed, the results afforded in the automata view of the Safety-Progress classification deal with regular properties. Classifying testable properties for more expressive specification formalisms (e.g., related to contextfree properties) would be of interest. This would require to transpose the testability conditions expressed in the automata view to a more expressive recognition mechanism. Then decidability conditions of the state reachability problem need to be taken into account.

<StreettAutomaton> <Alphabet> <Event id="a"/> <Event id="b"/> <Event id="c"/> </Alphabet> <States class="tree-set"> <no-comparator/> <State id="2"> <Transition event="a" nextState="sink"/> <Transition event="b" nextState="2"/> <Transition event="c" nextState="sink"/> </State> <State id="1" initial="true"> <Transition event="a" nextState="1"/> <Transition event="b" nextState="2"/> <Transition event="c" nextState="sink"/> </State> <State id="sink"> <Transition event="a" nextState="sink"/> <Transition event="b" nextState="sink"/> <Transition event="c" nextState="sink"/> </State> </States> <Description>Automaton defining Pi1</Description> <AcceptingCondition> <Pair P="1,2" R=""/> </AcceptingCondition> </StreettAutomaton> <StreettAutomaton> <Alphabet> <Event id="a"/> <Event id="b"/> </Alphabet> <States class="tree-set"> <no-comparator/> <State id="2"> <Transition event="a" nextState="5"/> <Transition event="b" nextState="3"/> </State> <State id="1" initial="true"> <Transition event="a" nextState="2"/> <Transition event="b" nextState="5"/> </State> <State id="5"> <Transition event="a" nextState="5"/> <Transition event="b" nextState="5"/> </State> <State id="3"> <Transition event="a" nextState="3"/> <Transition event="b" nextState="3"/> </State> </States> <Description>Automaton defining Pi2</Description> <AcceptingCondition> <Pair P="" R="3"/> </AcceptingCondition> </StreettAutomaton> An additional perspective is to combine the proposed approach using weak verdicts with a notion of test coverage. Indeed, in order to bring some confidence in the fact that e.g., the implementation satisfies the property, it involves to execute the test several times to make it relevant. The various approaches [START_REF] Rajan | Model Validation using Automatically Generated Requirements-Based Tests[END_REF][START_REF] Pecheur | A Formal Analysis of Requirements-based Testing[END_REF] for defining test coverage for property-oriented testing could be used to reinforce a set of weak verdicts.

Another theoretical perspective would be to relax the hypothesis on alphabets made in this paper. We supposed that execution sequences of the IUT are expressed in the same alphabet as the one used to describe the property; thus avoiding the practical question of the interpretation of the IUT's sequences on the property's sequences. While this hypothesis is reasonable to study the testability of properties, in practice there might be a discrepancy between the alphabet of the property and the alphabet of actions used by the tester to interact with the IUT. This kind of situation arises for instance when testing network security policies: the policy is written at a level of abstraction different from the level of the test architecture (that may consider implementation details). It thus seems interesting to combine our results with the results in [START_REF] Falcone | A Compositional Testing Framework Driven by Partial Specifications[END_REF][START_REF] Darmaillacq | Test generation for network security rules[END_REF] where the alphabet discrepancy issue is specifically addressed. Finally, it is our feeling that several previous testing frameworks using properties shall be revisited in the light of the results provided by this paper. For instance, in the security domain, testing frameworks dedicated to access-control policies [START_REF] Marchand | Automatic testing of access control for security properties[END_REF] use rules that can be forma-lized as safety or co-safety properties. Thus, it might be interesting to investigate whether other kinds of more evolved access-control rules, currently not tested, can be formalized as e.g., testable obligation or response properties. Consequently, those new rules could be validated using the revisited testing frameworks for access-control.

A Operators in the language-theoretic view of the Safety-Progress classification [START_REF] Falcone | What can you verify and enforce at runtime? Software Tools for Technology Transfer[END_REF] The language-theoretic view of the Safety-Progress classification is based on the construction of infinitary properties and finitary properties from finitary ones. It relies on the use of four operators A, E, R, P (building infinitary properties) and four operators A f , E f , R f , P f (building finitary properties) applying to finitary properties. In the original classification of Manna and Pnueli, the operators A, E, R, P, A f , E f were introduced. In this paper, we add the operators R f and P f and give a formal definition of all operators. In these definitions ψ is a finitary property over Σ.

Definition 16 (Operators

A, E, R, P ). -A(ψ) = {σ ∈ Σ ω | ∀σ ∈ Σ * , σ ≺ σ ⇒ ψ(σ )}. -E(ψ) = {σ ∈ Σ ω | ∃σ ∈ Σ * , σ ≺ σ ∧ ψ(σ )}. -R(ψ) = {σ ∈ Σ ω | ∀σ ∈ Σ * , σ ≺ σ ⇒ ∃σ ∈ Σ * , σ ≺ σ ≺ σ ∧ ψ(σ )}. -P (ψ) = {σ ∈ Σ ω | ∃σ ∈ Σ * , ∀σ ∈ Σ * , σ ≺ σ ≺ σ ⇒ ψ(σ )}.
A(ψ) consists of all infinite words σ s.t. all prefixes of σ belong to ψ. E(ψ) consists of all infinite words σ s.t. some prefixes of σ belong to ψ. R(ψ) consists of all infinite words σ s.t. infinitely many prefixes of σ belong to ψ. P (ψ) consists of all infinite words σ s.t. all but finitely many prefixes of σ belong to ψ.

The operators A f , E f , R f , P f build finitary properties from finitary ones. A f (ψ) consists of all finite words σ s.t. all prefixes of σ belong to ψ. One can observe that A f (ψ) is the largest prefix-closed subset of ψ. E f (ψ) consists of all finite words σ s.t. some prefixes of σ belong to ψ. One can observe that E f (ψ) = ψ • Σ * . R f (ψ) consists of all finite words σ s.t. ψ(σ) and there exists an infinite number of continuations σ of σ also belonging to ψ. P f (ψ) consists of all finite words σ belonging to ψ s.t. there exists a continuation σ of σ s.t. σ persistently has continuations σ staying in ψ (i.e., σ • σ belongs to ψ).

B Proofs

Closure of safety and guarantee r-properties. We first state the closure of safety and guarantee r-properties as a straightforward consequence of their definitions. Their closure will be used in the subsequent proofs.

Lemma 2 (Closure of safety and guarantee r-properties). Considering an r-property Π = (φ, ϕ) defined over an alphabet Σ built from a finitary property ψ, the following facts hold:

1. Π is a safety r-property if and only if all prefixes of a sequence belonging to Π also belong to Π, i.e., Π is prefix-closed. That is:

∀σ ∈ Σ ∞ , Π(σ) ⇒ ∀σ ∈ Σ * : σ ≺ σ ⇒ Π(σ ).
2. Π is a guarantee r-property if and only if all continuations of a finite sequence belonging to Π also belong to Π, i.e., Π is extension-closed. That is:

∀σ ∈ Σ * : Π(σ) ⇒ ∀σ ∈ Σ ∞ : Π(σ • σ ).
Proof. We prove the two facts successively:

1. We have either φ(σ) or ϕ(σ), i.e.,, all prefixes σ of σ belong to ψ. Necessarily, all prefixes σ of σ also belong to ψ, that is ψ(σ ). By definition, that means σ ∈ A f (ψ), i.e.,, ψ(σ ) and Π(σ ). 2. Π(σ) implies that σ has at least one prefix σ 0 σ belonging to ψ: σ ∈ E f (ψ). Then, any continuation of σ built using any finite or infinite sequence σ has at least the same prefix belonging to ψ. If σ ∈ Σ * , we have σ 0 σ σ •σ and σ •σ ∈ E f (ψ). If σ ∈ Σ ω we have σ 0 σ ≺ σ • σ and σ • σ ∈ E(ψ).

B.1 Proof of Theorem 1

The theorem states that, given a Streett m-automaton A Π = (Q A Π , q A Π init , -→ A Π , {(R 1 , P 1 ), . . . , (R m , P m )}) defining an r-property Π, according to the class of Π, the testability conditions expressed both in the languagetheoretic and automata views are given in Table 1.

Proof. We first prove the testability conditions from the language view for each Safety-Progress class as given in Table 1. We have to prove that when the proposed conditions hold, the underlying property is negatively determined.

(i) For safety r-properties. Let Π be a safety r-property, then there exists ψ ⊆ Σ * s.t. Π can be expressed (A f (ψ), A(ψ)). Let us consider σ ∈ ψ. Then, according to Lemma 2 on the closure of safety r-properties, we can deduce that every finite (resp. infinite) continuation of σ does not belong to A f (ψ) (resp. A(ψ)).

Thus every finite and infinite continuation of σ does not belong to (A f (ψ), A(ψ)): Π is negatively determined by σ. (ii) For guarantee r-properties. Let Π be a guarantee rproperty, then there exists ψ ⊆ Σ * s.t. Π can be expressed (E f (ψ), E(ψ)). Let σ be a sequence belonging to {σ ∈ ψ | pref (σ) ∪ cont(σ) ⊆ ψ}. Then, every prefix and every continuation of σ do not belong to ψ. Consequently, these continuations cannot belong neither to E f (ψ), nor to E(ψ) and (consequently) nor to Π as well: Π is negatively determined by σ. (iii) For obligation r-properties. Let Π be an obligation r-property, then Π can be expressed (for instance) under conjunctive normal form, i.e., there exists k ∈ N \ {0}, s.t.

Π = k i=1 (S i (ψ i ) ∪ G i (ψ i ))
where S i (ψ i ) (resp. G i (ψ i )) is a safety (resp. guarantee) r-property built upon ψ i (resp. ψ i ). Let σ 0 be a finite sequence belonging to

ψ i ∩ {σ ∈ ψ i | pref (σ) ∪ cont(σ) ⊆ ψ i } for some i ∈ [1, k].
Then, according to the proofs of (i) and (ii), each (finite or infinite) continuation σ of σ 0 does not satisfy (S i (ψ i ) ∪ G i (ψ i )). Hence, σ / ∈ k i=1 (S i (ψ i ) ∪ G i (ψ i )), which means ¬Π(σ ). (iv) For response and persistence r-properties. The reasoning is similar to the one used for guarantee rproperties. Let Π be a response (resp. persistence) r-property, then there exists ψ ⊆ Σ * s.t. Π can be expressed (R f (ψ), R(ψ)) (resp. (P f (ψ), P (ψ))). This r-property is testable if the set {σ ∈ ψ | cont(σ) ⊆ ψ} is not empty. The difference with guarantee properties is that an r-property can be negatively determined even if it has some prefixes in ψ.

We now prove these testability conditions from the automata view. Let A Π be the Streett automaton associ-ated to Π, and let σ be a finite sequence of length n s.t. run(σ, A Π ) = q 0 • • • q n .

(i) For safety r-properties. Let Π be a safety r-property.

If ∀i ∈ [0, n] : q i ∈ P then σ / ∈ Π, and, since there is no transition from P to P in A Π , each continuation σ of σ is s.t. each state of run(σ , A Π ) belongs to P . Hence σ is not accepted by A Π . (ii) For guarantee r-properties. Let Π be a guarantee rproperty. Let us assume that q n ∈ R ∧ Reach A Π (q n ) ⊆ R. Since there is no transition from R to R then σ / ∈ A Π . Moreover, each continuation σ of σ is s.t. each state of run(σ , A Π ) belongs to R. Hence σ is not accepted by A Π . (iii) For obligation r-properties. Let Π be an obligation r-property and assume that q n ∈ (P i ∩ {q ∈ R i | Reach A Π (q) ⊆ R i } for some given i ∈ [1, k]. Then, according to the proofs of (i) and (ii) each continuation σ of σ is s.t. each state of run(σ , A Π ) belongs to P i ∩ R i . Thus, σ is not accepted by A Π . (iv) For response r-properties. Let Π be a response rproperty and assume that q n ∈ {q ∈ R | Reach A Π (q) ⊆ R}. Then, σ ∈ Π and each continuation σ of σ is s.t. each state of run(σ , A Π ) belongs to R. Thus, σ is not accepted by A Π . (v) For persistence r-properties. The proof is similar to the one proposed for case (iv).

B.2 Proof of Lemma 1

Given σ ∈ Σ * a Streett automaton A Π defining a rproperty Π, and q ∈ Q A Π s.t. q A Π init σ -→ A Π q, we have to prove:

q ∈ G A Π ⇔ ⊕-determined (σ, Π), q ∈ B A Π ⇔ -determined (σ, Π).

Proof of q ∈ G AΠ ⇔ ⊕-determined (σ, Π). We prove the implication in both ways.

-Let us suppose that q ∈ G AΠ . Using the acceptance criterion for finite sequences, we have that σ is accepted by A Π . Furthermore, as A Π specifies Π, we have Π(σ). Now, let us consider µ ∈ Σ + s.t. |σ|+|µ| = n > n and run(σ •µ, A Π ) = q 0 • • • q n . As q ∈ G AΠ , we deduce ∀k ∈ N : n ≤ k ≤ n ⇒ q k ∈ m i=1 R i ∪ P i and consequently Π(σ • µ). Let us consider µ ∈ Σ ω , one may remark that ∀i ∈ [1, m] : vinf (σ•µ, A Π )∩R i = ∅∨ vinf (σ • µ, A Π ) ⊆ P i , which implies Π(σ • µ). We have Π(σ) ∧ ∀µ ∈ Σ ∞ : Π(σ • µ), i.e., ⊕-determined (σ, Π).

-Conversely, let us suppose that ⊕-determined (σ, Π).

By definition, it means ∀µ ∈ Σ ∞ : Π(σ •µ). According to the acceptance criterion of Streett automata, we deduce ∀k ≥ n, ∀µ ∈ Σ * :

run(σ • µ, A Π ) = q 0 • • • q • • • q k ⇒ q k ∈ m i=1 R i ∪ P i .
That is, Reach A Π (q) ⊆ m i=1 (R i ∪ P i ), i.e., q ∈ G AΠ .

Proof of q ∈ B AΠ ⇔ -determined (σ, Π). The proof can be done following the same principle as the one used to prove q ∈ G AΠ ⇔ ⊕-determined (σ, Π).

C Summary of notations

Fig. 1 .

 1 Fig. 1. A simple operating system

Fig. 4 .

 4 Fig. 4. Streett Automata for (A f (ψ 1 ), A(ψ 1 )), (E f (ψ 2 ), E(ψ 2 )), (R f (ψ 2 ), R(ψ 2 ))

Fig. 5 .

 5 Fig. 5. A Π op : reactivity Streett automaton specifying the behavior of the operating system

Fig. 6 .

 6 Fig. 6. Schematic illustrations of the shapes of Streett automata for basic classes

1

  Fig.6illustrates the syntactic restrictions on Streett automata for each basic class. A squared box represents a group of states. States are grouped according to whether they are recurrent or not (respectively denoted by "R" and "R"), and persistent or not (respectively denoted by "P " and "P "). Arrows represent possible transitions between groups of states 7 . For instance, for safety automata, there are P -states, P -states, and only R-states. For this kind of automata, the P -states can be distinguished according to whether P -states can be reached (the right-hand side group of states) or not (the lefthand side group of states).To refine Fig.2, a graphical representation of the Safety-Progress hierarchy of properties is depicted in Fig.8: for each class of properties, characterizations are recalled in the language-theoretic and automata views, as defined in Definition 5.

Π op 1 : 2 :Σ 4 : 5 :Fig. 7 .

 12457 Fig. 7. Some Streett automata for the operating system

Fig. 8 .

 8 Fig. 8. The SP classification

6. 1 . 2

 12 Testability of Exec(P Σ ) ⊆ Π in the Safety-Progress classification

6. 3

 3 Testability w.r.t. the relation Exec(P Σ ) ∩ Π = ∅ Testability results for this relation can be determined using:

Fig. 9 .

 9 Fig. 9. Schematic illustrations of the canonical tester for basic classes

Theorem 3 (

 3 Soundness and completeness of canonical testers). The canonical tester as defined in Definition 13 is a sound and complete test oracle augmented with weak verdicts as proposed in Definition 11. Proof. It is a direct consequence of Lemma 1. Example 8 (Canonical Testers). Canonical testers for rproperties of Example 3 are represented in Fig. 10. The alphabet partitioning is s.t. Σ IU T ? = {?a} and Σ IU T ! = {!b, !c}. Assignments to unknown are omitted for readability.

Π 3 Fig. 10 .

 310 Fig. 10. Canonical testers built from the r-properties of Example 3

4 Fig. 12 .

 412 Fig. 12. Canonical tester for some r-properties of the operating system

Fig. 13 .

 13 Fig. 13. Schematic illustrations of the canonical tester with quiescence for basic classes

  (a) Canonical tester for the global specification Π op

Fig. 18 .Fig. 19 .

 1819 Fig. 18. Defining Π 1 (left) and Π 2 (right) in XML

Definition 17 (

 17 Operators A f , E f , R f , P f ). -A f (ψ) = {σ ∈ Σ * | ∀σ ∈ Σ * , σ σ ⇒ ψ(σ )}. -E f (ψ) = {σ ∈ Σ * | ∃σ ∈ Σ * , σ σ ∧ ψ(σ )}. -R f (ψ) = {σ ∈ Σ * | ψ(σ) ∧ ∀n ∈ N, ∃σ ∈ Σ * , σ ≺ σ ∧ |σ | ≥ n ∧ ψ(σ )}. -P f (ψ) = {σ ∈ Σ * | ψ(σ) ∧ ∃σ ∈ Σ * , σ σ ∧ ∀n ∈ N, ∃σ ∈ Σ * , |σ | = n ∧ ψ(σ • σ )}.

  Intuitively, this condition compels the existence of a sequence which, if played on the IUT, allows to determine for sure, whether the relation holds or not. Let us note that this definition entails to synthesize a test oracle which allows to determine R Exec(P Σ ), Π from the observation of a sequence σ ∈ Exec f (P Σ ).A test oracle is a Moore automaton parameterized by a test relation as shown in Definition 6. It reads incrementally an execution sequence σ ∈ Exec f (P Σ ) and produces verdicts in {pass, fail , unknown}. Definition 9 (Test Oracle). A test oracle O for an IUT P Σ , a relation R and an r-property Π is a deterministic Moore automaton, i.e., a 5-tuple

). An r-property Π is said to be testable on P Σ w.r.t. the relation R if there exists a sequence σ ∈ Σ * s.t. verdict(σ, R(Exec(P Σ ), Π)) ∈ {pass, fail }.

Table 1 .

 1 Summary of testability results w.r.t. the relation Exec(P Σ ) ⊆ Π (for a fail verdict)

Table 3 .

 3 Testability

w.r.t. Inter (P Σ IU T ) ⊆ Π with quiescence

Table 3

 3 summarizes the notations used throughout the paper. R(Exec(PΣ), Π)) Def.7, p. 10 the verdict that the observation of σ allows to determine(Q O , q O init , Σ, -→O, Γ O ) Def.9, p. 11 test oracle (a Moore automaton: IOLTS with output function) (c) Summary of the notations introduced in Sect. 5 A Π Sect. 7.1, Def. 12, p. 16 the good, currently good, currently bad, and bad states of a Streett automaton AΠ T , q T init , Σ, -→T , Γ T ) Sect. 7.1, Def. 13, p. 16 canonical tester (a Moore automaton) (d) Summary of the notations introduced in Sect. 7 Inter (P Σ IU T ) Sect. 8.1, p. 18 the set of possible interactions of the tester with the IUT -determined-q(σ, Π) Sect. 8.1, Def. 14, p. 20 Π is negatively determined upon quiescence by σ ⊕-determined-q(σ, Π) Sect. 8.1, Def. 14, p. 20 Π is positively determined upon quiescence by σ (e) Summary of the notations introduced in Sect. 8

	Notation		Place Introduced Meaning
	Exec(PΣ) ⊆ Π	Def. 6, p. 10	testability relation stating that all behaviors of the IUT
				are allowed by the r-property
	Exec(PΣ) = Π	Def. 6, p. 10	testability relation: "the behaviors of the IUT
				are those described by the r-property"
	Exec(PΣ) ∩ Π = ∅	Def. 6, p. 10	testability relation: "the behaviors of the IUT
				and those described by the r-property are not disjoint"
	Π ⊆ Exec(PΣ)	Def. 6, p. 10	testability relation: "the IUT implements the r-property"
	verdict(σ, Notation		Place Introduced	Meaning
	G A Π , G A Π c	, B A Π
	Notation		Place Introduced	Meaning

c

, B

Table 3 .

 3 Summary of the notations used in the article

In the Safety-Progress classification guarantee properties are stating that "a good thing should happen in a finite amount of time". The guarantee class corresponds to the co-safety class in the Safety-Liveness classification.

The tester observes a finite execution of the IUT and should state a verdict about all potential continuations of this execution (finite and infinite ones).

Note that in practice properties are sometimes expressed using more abstract operations than the ones occurring at the IUT's execution level. However, the testability issues we address in this paper are still valid in spite of this alphabet discrepancy.

In the remainder of this paper, the term property will stand for regular property.

This will be used later in the paper for test generation from properties (Sect. 7).

Or from a finite set of finite sequences, as a straightforward extension.

In[START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF], this case is associated to the inconclusive verdict. Here we choose to state it as an unknown verdict instead. Indeed, in conformance testing, inconclusive verdicts are produced by a tester when the current test execution will not allow to reach a pass or fail verdict and is often used in association with a test purpose. Furthermore, we believe that the term "unknown" better corresponds to the fact that knowing whether the relation between Exec(P Σ ) and Π holds or not is not yet possible.

Intuitively, the set of sequences exposed in Table1represents the set of sequences allowing, for each class, to negatively determine the r-properties.

In[START_REF] Nahm | Test Case Generation for Temporal Properties[END_REF], for this relation, only guarantee properties are declared as testable.

Extensible Markup Languagehttp://www.w3.org/XML/

The Extensible Stylesheet Language Familyhttp://www.w3. org/Style/XSL/

http://xstream.codehaus.org/