Yliès Falcone

Jean-Claude Fernandez

Laurent Mounier

Jean-Luc Richier
email: jean-luc.richier@imag.fr

{ylies Falcone

A Test Calculus Framework applied to network security policies

We propose a syntax-driven test generation technique to automaticaly derive abstract test cases from a set of requirements expressed in a linear temporal logic. Assuming that an elementary test case (called a "tile") is associated to each basic predicate of the formula, we show how to generate a set of test controlers associated to each logical operator, and able to coordinate the whole test execution. The test cases produced are expressed in a process algebraic style, allowing to take into account the test environment constraints. We illustrate this approach in the context of network security testing, for which more classical model-based techniques are not always suitable.

Introduction

Testing is a very popular validation technique, used in various application domains, and for which several formalizations have been proposed. In particular, a well-defined theory is the one commonly used in the telecommunication area for conformance testing of communication protocols [START_REF]OSI-Open Systems Interconnection, Information Technology -Open Systems Interconnection Conformance Testing Methodology and Framework[END_REF]. This approach, sometimes called "model-based" approach, consists in defining a conformance relation [START_REF] Brinksma | A Formal Approach to Conformance Testing[END_REF][START_REF] Tretmans | Test Generation with Inputs, Outputs, and Quiescence[END_REF] between a specification of the system under test and a model of its actual implementation. The purpose of the test is then to decide if this relation holds or not. A practical interest is that test cases can be automatically produced from this specification. Several tools implement this automatic generation technique, e.g. [START_REF] Jard | TGV: theory, principles and algorithms[END_REF][START_REF] Belinfante | Formal Test Automation : a Simple Experiment[END_REF][START_REF] Schmitt | Autolink -A Tool for Automatic and Semi-Automatic Test Generation from SDL Specifications[END_REF][START_REF] Groz | Automated test generation from SDL specifications[END_REF].

However, this model-based approach requires a rather complete specification of the system under test, defined on a precise interface level. If this requirement can be fulfilled for specific pieces of software (e.g., a communication protocol), it may be difficult to achieve for large systems, or when the system requirements cannot be encoded as a conformance relation defined on a single interface level. A typical example of such situation is testing a network security policy, where expected properties may rely on the whole network behavior (not on a single component or protocol), and can be tested only by accessing several interface levels.

In a previous work [START_REF] Darmaillacq | Test Generation for Network Security Rules[END_REF], we have proposed an alternative approach when the system requirements are expressed as a set of (temporal) logic formulae. For each formula φ, an abstract test case t φ is produced following a syntax-driven technique: assuming that an elementary test case t i (called hereafter a "tile") has been associated to each literal p i of formula φ, the whole test case t i is obtained by combining the tiles using test operators corresponding to the logical operators appearing in formula φ. This provides a structural correspondence between formulae and tests and it is easy to prove that the test obtained are sound with respect to the semantics of the formulae (in other words we give a "test based" semantics of the logic which is compatible with the initial one). The originality of this approach is then that a part of the system specification is encoded into the tiles, that can be provided by the system designer, or a by a test expert, which is assumed to be easier to obtain that a global specification. We illustrated this approach in the context of security testing.

This paper extends this previous work from the test execution point of view. In [START_REF] Darmaillacq | Test Generation for Network Security Rules[END_REF], abstract test cases were directly expressed by labelled transition systems, independently of the test architecture. We propose here to better take into account the test execution and to express the test cases in a higher level formalism. In particular we show how to produce well structured test cases consisting of a set of test drivers (one test driver for each elementary tile), coordinated by a set of test controllers (corresponding to the logical operators appearing in the formula). Thus, independent parts of the formula can be tested in parallel (either to speed up the test execution, or due to test environment constraints), each local verdicts being combined in a consistent way by the test controllers. Formally, test cases are expressed in a classical process algebra (called a "test calculus"), using basic control operators (parallel composition and interruption) and data types to handle test parameters and verdicts.

This paper is organized as follows: section 2 introduces our "test calculus" process algebra, and section 3 defines the notions of test execution and test verdicts. We propose in section 4 a simple temporal logic allowing to express network security requirements, and we show how to produce test cases from this logic in section 5. Finally, section 6 provides some examples in the context of network security policies.

Test process algebra

To model processes, we define a rather classic term algebra with typed variables, inspired from CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] and Lotos. We suppose a set of predefined actions Act, a set of types T , and a set of variables Var. Actions are either modifications of variables or communications through channels which are also typed. In the following, we do not address the problem of verifying that communications and assignments are well-typed. We denote by expr τ (resp. x τ ) any expression (resp. variable) of type τ . Thus, when we write x τ := expr τ , we consider that this assignment is well typed.

A test is described as a term of our process algebra. We distinguish between elementary test cases, which are elements of a basic process algebra and compound test cases. We give the syntax and an operational semantics of this test process algebra.

Basic processes

Our basic process algebra allows to describe sequences of atomic actions, communication and iteration. A term of this algebra is called a tile, which are the elementary test components and we note TILE the set of all tiles.

The syntax of tiles and actions is given by the following grammar: There are two kinds of actions (γ ∈ Act). The first ones are the internal actions (modification of variables). The second ones are the communication actions. Two kinds of communications exist: ?c(x τ ) denotes value reception on a channel c which is stored in variable x τ ; !c(expr τ ) denotes the emission of a value expr τ on a channel c. Communication is done by "rendez-vous".

Composing processes

Processes are compositions of tiles. Choices we made about composition operators came from needs appearing in our case studies in network security policies [START_REF] Darmaillacq | Test Generation for Network Security Rules[END_REF]. Composing tests in sequence is quite natural; however, for independent actions, and in order to speed-up test executions, one might want to parallelize some tests executions, for example, if one wants to scan several computers on a network. The parallel composition is also used to model the execution and communication between the test processes and the rest of the system. We assume a set C of channels used by tiles to communicate. We distinguish internal channels (set C in ) and external channels (set C out ), and we have C = C in ∪ C out .

In case of several processes executing in parallel, one might want to interrupt them. We choose to add an operator providing an exception mechanism: it permits to replace a process by an other one on the reception of a communication signal.

So, we define a set of operators, { L , I }, respectively the parallel (with communication through a channel list L ⊆ C), and exception (with an action list I) compositions.

The grammar for term processes (TERM) is:

t ::= e | t L t | t I t
The parallel operator L (so as the choice operator +) is associative and commutative. It expresses either the interleaving of independant action or the emission !c(expr τ ) of the value of an expression expr τ on a channel c. When the value is received by a process ?c(x τ ), the communication is denoted at the syntactic level by c(expr τ /x τ ). The independent and parallel execution ∅ is noted .

The Join-Exception operator I is used to interrupt a process and replace it with an other when a synchronization/global/communication action belonging to its synchronization list I occurs. Intuitively, considering two processes t, t and a communication action α, t {α} t means that if α is possible, t is replaced by t , else t continues normally.

Semantics

α ∈ Act (•) α • t α t t[recX • t/X] α t α ∈ Act (rec) recX • t α t α ∈ Act t2 α t 2 (+) t1 + t2 α t 2 α / ∈ {[b]!c(exprτ ), [b]?c(xτ )|c ∈ L, b ∈ Bexp} t1 α t 1 ( ¬L) t1 L t2 α t 1 L t2 c ∈ Cin ∧ c ∈ L t1 [b]!c(exprτ ) t 1 t2 [b]?c(xτ ) t 2 ( C in ) t1 L t2 [b]c(exprτ /xτ ) t 1 L t 2 c ∈ Cout ∧ c ∈ L t1 [b]!c(exprτ ) t 1 (! Cout ) t1 L t2 [b]!c(exprτ ) t 1 L t2 c ∈ Cout ∧ c ∈ L t1 [b]?c(xτ ) t 1 (? Cout ) t1 L t2 [b]?c(exprτ /xτ ) t 1 L t2 α ∈ I t2 α t 2 ( I α ) t1 I t2 α t 2 α / ∈ I t1 α t 1 ( I ¬α ) t1 I t2 α t 1 I t2
Fig. 1. Rules for term rewriting

A runtime environment ρ maps the set of variables to the set of values. We note E the set of all environments. Actions modify environments in a classical way; we note ρ γ → ρ the modification of environment ρ into ρ by action γ. For example, ρ

xτ :=expτ -→ ρ[ρ(exp τ )/x τ ],
where ρ[ρ(exp τ )/x τ ] is the environment ρ in which variable x τ is associated the value ρ(exp τ ). In the following, environments are extended to any typed expression. A labelled transition system (LTS, for short) is a quadruplet (Q, A, T, q 0 ) where Q is a set of states, A a set of labels, T the transition relation (T ⊆ Q × A × Q) and q 0 the initial state (q 0 ∈ Q). We will use the following definitions and notations: (p, a, q) ∈ T is noted p a -→ T q (or simply p a -→ q). An execution sequence λ is a composition of transitions:

q 0 a1 -→ q 1 a2 -→ q 2 • • • an -→ q n .
We denote by σ λ (resp. α λ ) the sequence of states (resp. observable actions) associated with λ. The sequence of actions α λ is called a trace. We note by Σ S , the set of finite execution sequences starting from the initial state q 0 of S. For any sequence λ of length n, λ i or λ(i) denotes the i-th element and

λ [i•••n] denotes the suffix λ i • • • λ n .
The semantics of a process is based on a LTS where states are "configurations", pairs (t, ρ), t being a term of the process algebra, ρ an environment, and transitions are given by definition 2. Configurations are used to represent process evolutions. We note C term def = TERM × E the set of configurations.

Definition 1 (Term-transition). A term rewriting transition

is an element of TERM × Act × TERM. We say that the term t is rewritten in t by action α. We note: t α t . This semantics is similar with the CCS one [START_REF] Milner | A Calculus of Communicating Systems[END_REF].

Term-transitions are defined in Figure 1 (using the fact that is commutative).

Definition 2 (Transitions). A transition is an element of

C term × Act × C term .
We say that the term t in the environment ρ is rewritten in t modifying the environment ρ in ρ .

We have four transition rules, one for an assignment, and three for communication exchange. They are defined in Figure 2.

ρ(b) = true ρ(exprτ) = v t [b]xτ :=exprτ t (:=) (t, ρ) xτ :=v -→ (t , ρ[v/xτ ]) ρ(exprτ ) = v t [b]!c(exprτ ) t ρ(b) = true (!) (t, ρ) !c(v) -→ (t , ρ ) v ∈ Dom(τ ) t [b]?c(xτ ) t ρ(b) = true (?) (t, ρ) ?c(v) -→ (t, ρ[v/xτ ]) ρ(exprτ ) = v t [b]c(exprτ /xτ ) t ρ(b) = true (c(exprτ /xτ )) (t, ρ) c(v) -→ (t, ρ[v/xτ ])
Fig. 2. Rules for environment modification

Test execution and test verdicts

As seen in the previous section, the semantics of a test case represented by a T ERM process t is expressed by a LTS S t = (Q t , A t , T t , q t 0 ). We assume here that the behaviour of the System Under Test (SUT) is also modelled by a LTS I = (Q I , A I , T I , q I 0 ). A test execution is then a sequence of interactions between t and the SUT to deliver a verdict indicating whether the test succeeded or not. We first explain how verdicts are computed in our context, and then we give a formal definition of a test execution.

Tiles verdicts

We assume in the following that any elementary tile t i owns at least one variable used to store its local verdict, namely a value of enumerated type V erdict = {pass, f ail, inc}. This variable is supposed to be set to one of these values when tile execution terminates. The intuitive meaning we associate to each of these values is similar to the one used in conformance testing:

• pass means that the test execution of t i did not reveal any violation of the requirement expressed by t i ; • f ail means that the test execution of t i did reveal a violation of the requirement expressed by t i ; • inc means that the test execution of t i did not allow to conclude about the validity of the requirement expressed by t i .

We now have to address the issue of combing the different verdicts obtained by each tile execution of a whole test case.

Verdict management

The solution we adopt is to include in the test special processes (called test controlers) for managing tile verdicts. When tiles end their execution, i.e. have computed a verdict, they emit it toward a designated test controler which captures it. Depending on verdicts received, the controller emits a final verdictand may halt the executions of some tests if they are not needed anymore. The "main" controler then owns a variable v g to store the final verdict.

Test controllers can easily be written in our process algebra with communication operations as shown on the following example. The whole test case is then expressed as a term of our process algebra (with parallel composition and interuptions between processes).

An example of test controller Let us consider a test controller waiting to receive two pass verdicts in order to decide a global pass verdict (in other cases, it emits the last verdict received). Let c v, be the channel on which verdicts are waited. The environment of this controller contains three variables, v for the verdicts received, v g for the global verdict, and N to count numbers of verdicts remaining. An LTS representation is shown in Figure 3 and a corresponding algebraic expression is:

def = recX ?c vi(vi) • ([vi = pass] N --• X + [vi ∈ {inc, f ail}] vg := vi • !c vg(vg) • !Stop() • nil + [N = 0] vg := pass • !c vg(vg) • !Stop() • nil ?c v(v) [v = pass] N -- [N = 0] vg := pass !c vg (vg ) [v ∈ {inc, f ail}] vg := v !Stop()
Fig. 3. Verdict controller combining pass verdicts.

Test execution

An execution of a test t (modelled by an LTS S t ) on a SUT (modelled by a LTS I), noted Exec(t, I), is simply expressed as a set of common execution sequences of S t and I, defined by a composition operator ⊗.

Let

λ I = q I 0 a1 -→ q I 1 a2 -→ q I 2 • • • an -→ q I n • • • ∈ Σ I and λ St = q 0,t a1 -→ q t 1 a2 -→ q t 2 • • • an -→ q t n ∈ Σ St , then λ St ⊗ λ I = (q 0,t , q I 0 ) a1 -→ (q t 1 , q I 1 ) • • • an -→ (q t n , q I n ) ∈ Exec(t, I). Let Σ pass St (resp. Σ fail St , Σ inconc

St

) be the sets of states of S t where variable v g is set to pass (resp. f ail, inc):

Σ pass St = {(r, ρ) | ρ(v g ) = pass} Σ fail St = {(r, ρ) | ρ(v g ) = f ail} Σ inc St = {(r, ρ) | ρ(v g ) = inc}

Security rules formalization

In a previous work, we carried out a case study to analyse the network security policy in a university environment. This case study gave us a set of security requirements that could be expressed using a simple temporal logic. We give here the syntax and semantics of this logic.

Syntax

A security policy rule is expressed by a logical formula (ϕ), built upon literals. Each literal can be either a condition literal (p c ∈ P c ), or an event literal (p e ∈ P e ). A condition literal is a (static) predicate on the network configuration (e.g., extRelay(h) holds iff machine h is configured as an external relay), and an event literal corresponds to the occurrence of a transition in the network behavior (e.g., enterN etwork(m) holds if message m is received by the network). A conjunction of condition literals is simply called a condition (C), whereas a conjunction of a single event literal and a condition is called a (guarded) event (E). The abstract syntax of a formula is given in Table 1. The intuitive meaning of these formulae is the following:

-An O-Rule expresses a conditional obligation: when a particular condition holds, then another condition should also hold (logical implication). -An O T -Rule expresses a triggered obligation: when a given event happens, then another condition should hold (or some event should occurs) before expiration of a given amount of time. -An F -Rule expresses an interdiction: when a given condition holds, or when a given event happens, then a given event is always prohibited.

ϕ ::= C ⇒ O C (O-Rule ) | E ⇒ OT C | E ⇒ OT E (OT -Rule) | C ⇒ F C | C ⇒ F E (F-Rule) E ::= pe[C] | pe (Event) C ::= V n i=1 pc i (Condition)
Table 1. Syntax of logic formulae

Semantics

Formulas are interpreted over LTS. Intuitively, a LTS S satisfies a formula ϕ iff all its execution sequences λ do, where condition literals are interpreted over states, event literals are interpreted over labels. We first introduce two interpretation functions for condition and event literals: f c : P c → 2 Q , associates to p c the set of states on which p c holds; f e : P e → 2 A , associates to p e the set of labels on which p e holds.

The satisfaction relation of a formula ϕ on an execution sequence λ (λ |= ϕ) is then (inductively) defined as follows:

-λ |= C for C = p 1 c ∧ • • • ∧ p n c iff ∀i. σ λ (1) ∈ f (p i c ) -λ |= p e iff α λ (1) ∈ g(p e ) -λ |= p e [C] iff (α λ (1) ∈ g(p e ) ∧ λ(2) |= C) -λ |= ϕ 1 ⇒ O ϕ 2 iff ((λ |= ϕ 1 ) ⇒ (λ |= ϕ 2 )) -λ |= ϕ 1 ⇒ O T ϕ 2 iff ((λ |= ϕ 1 ) ⇒ (∃j ∈ [1, |λ|]. λ(j) |= ϕ 2 )) -λ |= ϕ 1 ⇒ F ϕ 2 iff ((λ |= ϕ 1 ) ⇒ (∀j ∈ [1, |λ|]. λ(j) |= ϕ 2 )) Finally, S |= ϕ iff ∀λ ∈ Σ S . λ |= ϕ.

Test generation

We define a structural generation function GenT est to convert a rule into the desired combination of elementary tiles with controllers. It associates controllers in such a way that the final verdict is pass iff the rule is satisfied by the SUT. Each controller emits its verdict on a channel, and may uses variables. In the following, new variables and channels will be silently created whenever necessary.

GenT est generates parallel and architecturally independent subtests. Formula semantics is ensured by the controller verdict combinations. Suitable scheduling of subtests is supplied by the controllers through channels used to start and stop subtests (given below by T est function).

Test generation function GenT est

Transformation of tiles Given a tile t p (computing its verdict in the variable ver) associated to an elementary predicate p, the Test function transforms it. Intuitively, T est(t p , L), where L is a channel list, is t p modified in order to be controlled through the channel list L. More formally: GenT est definition The rule general form is: P l ⇒ M P r where P l , P r ∈ {E, C} are predicates and M ∈ {O, O T , F } a modality. The GenT est function is defined on the rule structure, giving an expression to be instantiated according to the different modalities. We suppose that the final verdict is emitted on the main channel, and t ci , t pe are the tiles respectively associated to elementary predicates c i , p e .

GenT est(P

Verdict controllers

Several verdict controllers are used in the GenT est definition. Controllers have different purposes. They are first used to manage the execution of subtests corresponding to the components of the rule. For example, for a O T formula, we have to wait for the left-side subtest before starting the right-side subtest. Controllers are also used to "implement" the formula semantics by combining verdicts from subtests.

Controllers definitions are parameterized with channel parameters. We give here an informal description of the controllers, with a graph definition for the more important ones; other controllers are similar (definitions given in appendix). Formula level controllers They emit their verdict on the channel main.

1. O (channel list, channel list). This controller is used to manage the execution of tiles corresponding to the left and right part of a static implication.

The controller starts the two tests corresponding to the two sides of the implication. Then it waits for the reception of a verdict (verdicts can arrive in any order). According to the semantics of implication and the first verdict received, it decides either to wait for the second verdict or to emit a verdict immediately. The controller takes two channel lists as parameters for managing the execution and verdict of each side of the implication. The associated environment contains three variables. A LTS representation of

O ({c start l , c stop l , c v l , c loop l }, {c start r , c stop r , c v r , c loop r }) is shown in Figure 5.
2. OT (channel list, channel list). This controller is used to manage the execution of tiles corresponding to the sides of an implication with a triggered obligation. The controller starts the test corresponding to the left side of the implication. If this test is inconclusive or fails, a inc verdict is decided. Otherwise, the timer and the second test are started. If the test emits pass, the final verdict is pass. As long as the timer is not expired, (that is, the boolean variable t out is false), if the second test ends with f ail or inc, the test is started again. When the the timer expires, a stop signal (!c stop r ) is sent to the right side test. In that case, the final verdict is inc if an inc verdict occured, f ail otherwise. A LTS representation of OT ({c start l , c stop l , c loop l , c ver l }, {c start r , c stop r , c loop r , c ver r }) is shown in Figure 6. 3. F (channel list, channel list). This controller is similar to the O controller. It waits for a fail verdict for the right-side subtest in order to conclude on a pass verdict. A LTS definition of this controller is given in appendix A.2 in Figure 7.

Predicate level controllers

1. E (channel list, channel list, channel list). This controller is used to manage executions and verdicts around an event. The controller starts the execution of the event, and then, depending on the verdict received, it starts the subtests associated to the condition predicates in E. This conditions have to be tested after the event. A LTS definition of this controller is given in appendix A.3 in Figure 8. 2. ∧ (channel lists, integer). Informally this controller starts different test and waits for verdicts. Like the other controllers it controls subtests with a channel. If all tests succeed, the controller emits a pass verdict. If some tests do not respond pass the controller emits the last verdict received and stops the other potentially executing subtests. This controller is a generalization of the one presented in 3.1. A LTS definition of this controller is given in appendix A.4 in Figure 9.

Soundness proposition

We now express that an abstract test case produced by function GenT est is always sound, i.e. it delivers a fail verdict when executed on a network behavior I only if formula φ does not hold on I. To do this, we follow a very similar approach than in [START_REF] Darmaillacq | Test Generation for Network Security Rules[END_REF]. Two hypotheses are required in order to prove this soundness property:

H1. First, for any formula ϕ, we assume that each elementary test case t i provided for the (event or condition) literals p i appearing in ϕ is strongly sound in the following sense: Execution of t i on SUT I always terminate, and ∀λ ∈ Exec(t i , I)•VExec(λ) = Pass ⇒ λ |= p i ∧(VExec(λ) = Fail ⇒ λ |= p i ). H2. Second, we assume that the whole execution of a (provided or generated) test case t associated to a condition C is stable with respect to condition literals: the valuation of these literal does not change during the test execution. This simply means that the network configuration is supposed to remain stable when a condition is tested. Formally:

∀p i ∈ P c . ∀λ ∈ Σ I • λ St ⊗ λ ∈ Exec(t, I) ⇒ (σ λ ⊆ f c (p i ) ∨ σ λ ∩ f c (p i ) = ∅)
where σ λ denotes here tacitly a set of states instead of a sequence.

We now formulate the soundness property: Proposition: Let ϕ a formula, I an LTS and t = GenTest(ϕ). Then:

λ ∈ Exec(t, I) ∧ VExec(λ) = f ail =⇒ I |= ϕ.

Application

In this section we apply the GenT est function with two rule patterns taken from the case study presented in [START_REF] Darmaillacq | Test Generation for Network Security Rules[END_REF].

O-Rule

Consider the requirement "External relays shall be in the DMZ", this could be reasonably understood as "If a host is an external relay, it has to be in the DMZ". A possible modelisation is:

extRelay(h) ⇒ O (inDM Z(h))
We suppose that somehow we have tiles models for extRelay(h) and inDM Z(h). The GenT est function can be applied on the formula:

GenT est(extRelay(h) ⇒ O (inDM Z(h))) = " GenT estP (extRelay(h), L l ) GenT estP (inDM Z(h), Lr) " L O (L l , Lr) = " GenT estC(extRelay(h), L l ) GenT estC(inDM Z(h), Lr) " L O (L l , Lr) = " T est(extRelay(h), L l ) T est(inDM Z(h), Lr) " L O (L l , Lr) where L = L l ∪ Lr L l = {c start l , c stop l , c v l , c loop l } Lr = {c startr, c stopr, c vr, c loopr}
The definitions of t extRelay(h) and t inDMZ(h) (writing their verdict in their verdict variable (ver)) in our algebra are: The global test is associated a suitable environment by renaming the two verdict variables of t extRelay(h) and t inDMZ(h) . The new environment contains the following variables: ver 1 for t extRelay(h) , ver 2 for t inDMZ(h) , ver l , ver r for O . t extRelay(h) , and t inDMZ(h) communicate with the controller through channels in L.

t extRelay(h) def = !connect(he,

O T -Rule

Security policies may also express availability requirements. Consider "When there is a request to open an account, user privileges and resources must be activated within one hour". We formalize this requirement as: Supposing that there exists a tile for each predicate and that all tiles are independent. One could generate a test from appropriate derivation: ´ L le ∪L lc E (L l , L le , L lc ) " " `T est(op acc(c), Lre) GenT estC(alloc disk(c), Lrc)

´ Lre∪Lrc E (Lr, Lre, Lrc) "

L O 1H (L l , Lr) = " `T est(req acc(c), L le ) T estC(ex acc(c), L lc )
´ L le ∪L lc E (L l , L le , L lc ) " " `T est(op acc(c), Lre) T estC(alloc disk(c), Lrc)

´ Lre∪Lrc E (Lr, Lre, Lrc) "

L O 1H (L l , Lr) with: L = L l ∪ Lr, Ls = {c starts, c stops, c loops, c vers}s, s ∈ {l, r, le, lc, re, rc}

Conclusion

We have proposed a test generation technique for testing the validity of a temporal logical formula on a system under test. The originality of this approach is to produce the tests by combinations of elementary test cases (called tiles), associated to each atomic predicates of the formula. These tiles are supposed to be provided by the system designer or a test expert, and, assuming they are correct, it can be proved that the whole test case obtained is sound. The practical interest of this approach is that it can be applied even if a formal specification of the system under test is not available, or if the test execution needs to mix several interface levels. A concrete example of such a situation is network security testing, where the security policy is usually expressed as a set of logical requirements, encompassing many network elements (communication protocols, firewalls, antivirus softwares, etc.) and those behavior would be hard to describe on a single formal specification. The abstract test cases we obtain are expressed in a process algebraic style, and they are structured into test drivers (the tiles), and test controllers (encoding the logical operators). This approach makes them close to executable test cases, and easy to map on a concrete (and distributed) test architecture. Independent parts of the tests can then be executed concurrently. This work could be continued in several directions. First, the logic we proposed here could be extended. So far, the kind of formulae we considered was guided by a concrete application, but, staying in the context of network security, other deontic/temporal modalities could be foreseen, like"interdiction within a delay", or "permission". We also believe that this approach would be flexible enough to be used in other application domains, with other kinds of logical formulae (for instance with nested temporal modalities, which were not considered here). A second improvement would be to produce a clear diagnostic when a test execution fails. So far, test controllers only propagate "fail" verdicts, but it could be useful to better indicate to the user why a test execution failed (which subformula was unsuccessfully tested, and what is the incorrect execution sequence we obtained). Finally, we are currently implementing this test generation technique, and we expect that practical experimentations will help us to extend it towards the generation of concrete test cases, that could be directly executable. The automaton shown in Figure 7 presents the F (L l , L r ) controller,with:

A Complete definitions of controllers

L l = {c start l , c stop l , c loop l , c v l }, L r = {c start r , c stop r , c loop r , c v r })

A.3 The E controller

The automaton shown in Figure 8

B Execution trace of a O-rule generated test

We show a possible execution of this process, the choice considered make extRelay finishing first with f ail. Then, the controller computes an inc verdict, and send it to the user through the channel main. We list here only the term rewritings, and show the evolution of the environment ρ only when it is modified. We start from the test generated from GenT est(extRelay(h) ⇒ O inDM Z(h)). In the following, I l = {?c stop l }, I r = {?c stop r }.

e

  ::= α • e | e + e | nil | recX e | X α ::= [b]γ γ ::= x τ := expr τ | !c(expr τ ) | ?c(x τ ) b ::= true | false | b ∨ b | b ∧ b | ¬b | expr τ = expr τ where e ∈ T ILE is a tile, b a boolean expression, c a channel name, γ an action, • is the prefixing operator (• : Act × T ILE → T ILE), + the choice operator, and recX : T ILE → T ILE allows recursive tile definition with X a term variable. When the condition b is true, we abbreviate [true]γ by γ. The special tile nil does nothing.

For λ ∈

 ∈ Exec(t, I), we define the verdict function: VExec(λ) = pass (resp. fail , inconc) iff there is λ St ∈ Σ pass St (resp. Σ fail St , Σ inconc St ) and λ I ∈ Σ I such that λ St ⊗ λ I = λ.

TFig. 4 .

 4 Fig. 4. Extension of tile tp in a testing form

  l ⇒ M P r ) def = (GenT estP (P l , L l ) GenT estP (Pr, Lr)) L M(Ll, Lr) with L = L l ∪ Lr, L l = {c start l , c stop l , c loop l , c ver l }, Lr = {c startr, c stopr, c loopr, c verr} GenT est P (E, {c start, c stop, c loop, c ver}) def = if E = pe[C], `T est(tp e , Le) GenT estC(C, Lc) ´ L E ({c start, c stop, c loop, c ver}, Le, Lc) with L def = Le ∪ Lc Le = {c starte, c stope, c loope, c vere}, Lc = {c startc, c stopc, c loopc, c verc} else /* E = pe */ T est(tp e , {c start, c stop, c loop, c ver}) GenT est P (C, L) def = GenT estC(C, L) GenT est C (∧ n i=1 c i , {c start, c stop, c loop, c ver}) def = if n = 1, T est(tc 1 , {c start, c stop, c loop, c ver}) else /* n > 1 */ n i=1 T est(tc i , Li) L ∧({c start, c stop, c loop, c ver}, (Li)i=1...n, n) with L = ∪ n i=1 Li; ∀i ∈ {1 . . . n}, Li = {c start, c stop, c loop, c veri}

!Fig. 5 .

 5 Fig. 5. An instantiated LTS representation of the O controller.

Fig. 6 .

 6 Fig. 6. An instantiated LTS representation of the O T controller

  h)• `(?ok•!transf er(he, h, m) • [?ok•!tranf er(h, hi, m) • ver := pass+?ko • ver := f ail]) + (?ko • ver := f ail) •nilt inDM Z(h) def = !tracert(hd, h)• ?end • ver := pass + ˆ?resp(hx) • `(?resp(hx )•?end • ver := inc) + (?end • ver := f ail) ´•nil So, GenT est(extRelay(h) ⇒ O inDM Z(h)) = ((?c start l •!connect(he, h) • . . .) I l ?c stop l • nil) ((?c startr•!tracert(hd, h) • . . .) Ir ?c stopr • nil) L " !c start l •!c startr • (?c v l (v l ) • . . . +?c vr(vr) • . . .)"with I l = {?stop l }, Ir = {?stopr}

  request open account(c)[¬ex account(c)] ⇒ O1H(open account(c)[allocate disk(c)])

  GenT est(req acc(c)[¬ex acc(c)] ⇒ O1H (op acc(c)[alloc(c)])) def = `GenT estP (req acc(c)[¬ex acc(c)], L l ) GenT estP (op acc(c)[alloc(c)], Lr)´L O 1H (L l , Lr) = "`T est(req acc(c), L le ) GenT estC(ex acc(c), L lc )

A. 1

 1 The O controller O def = !c start l • !c start r • ((?c ver r (v r ) • t r ) + (?c ver l (v l ) • t l )) tr def = ([vr ∈ {inc, f ail}]?c ver l (v l ) • tr1) + ([vr = pass]?c ver l (v l )) t l def = (([v l ∈ {inc, f ail}]vg := inc) + ([v l = pass]?c verr(vr) • vg := vr)) • end tr1 def = ([v l = pass]vg := vr + [v l ∈ {inc, f ail}]vg := inc) • end tr2 def = ([v l = pass]vg := pass + [v l ∈ {inc, f ail}]vg := inc) • end end def = !main(vg) A.2 The F controller

!c startFig. 7 .

 7 Fig. 7. An instanciated automaton representation of the F controller.

Fig. 8 .

 8 Fig. 8. An instanciated automaton representation of the E controller.

`Fig. 9 .

 9 Fig. 9. An instanciated automaton representation of the ∧ controller.