Christophe Chareton

Julien Brunel

David Chemouil

Evaluating the Assignment of Behavioral Goals to Coalitions of Agents

We present a formal framework for solving what we call the "assignment problem": given a set of behavioral goals for a system and a set of agents described by their capabilities to make the system evolve, the problem is to find a "good" assignment of goals to (coalitions of) agents. To do so, we define Kore, a core modelling framework as well as its semantics in terms of a strategy logic called USL. In Kore, agents are defined by their capabilities, which are pre-and post-conditions on the system variables, and goals are defined in terms of temporal logic formulas. Then, an assignment associates each goal with the coalition of agents that is responsible for its satisfaction. Our problem consists in defining and checking the correctness of this assignment. We define different criteria for modelling and formalizing this notion of correctness. They reduce to the satisfaction of USL formulas in a structure derived from the capabilities of agents. Thus, we end up with a procedure for deciding the correctness of the assignment. We illustrate our approach using a toy example featuring exchanges of resources between a provider and two clients.

Introduction

The question of assigning behavioral goals to coalitions of agents (i.e. sets of active entities), the capabilities of whom are known, is a fundamental and recurring problem in various areas of software and systems engineering. We call it the assignment problem. In this paper, we propose a formalization of this problem and then describe various criteria to assess an assignment formally.

First, let us illustrate various situations where this problem arises; this will not only demonstrate the ubiquity of this problem but also enable us to delineate the most salient aspects that ought to be addressed in the formalization.

In the field of Requirements Engineering (RE), for instance, several modeling languages have been proposed that each partly feature the concepts just mentioned. Thus, Kaos [Let02,LVL02b,vL09,vL03], a so-called goal-oriented modeling language, features behavioral goals that may be formalized using Linear Temporal Logic (LTL). This allows us to assert and check the correctness of both refinement between goals and of realization of goals by operations. On the other hand, agent-oriented modeling languages, such as Tropos [BPG + 04] and i * [Yu09, Yu96], also focus on the agents that will realize these goals. A formal extension of i * , featuring commitments and protocols [CDGM10b, CDGM10a, CS09, MS06], aims at checking the capabilities of agents to ensure the satisfaction of the goals. There, goals are described using propositional logic and agents are described along with their capabilities to ensure the satisfaction of propositional formulas. Thus, the need for a treatment of the assignment problem has been identified in RE but, to the best of our knowledge, no proposition has been made until now to address it for behavioral goals, in a formalized framework.

In Systems-of-Systems Engineering (SoSE) [Mai98], several independent systems, made up of subsystems (agents in our parlance) interact altogether to achieve a global mission. Consider one of these systems and its set of agents A. Then, to investigate whether the agents in A are able to ensure a given goal in the global system, one must take into account the side effects of the actions performed by the other agents (from other systems) pursuing different goals.

Finally, in Component-Based Software Engineering (CBSE) [Szy02], individual components (agents, for us) may be assembled into composite subsystems in order to fulfill requirements specifications. The capabilities of these agents are given as contracts [BJPW99]. Then knowing whether the resulting architecture indeed satisfies its specification is of major importance. Besides, identifying unsatisfied specifications can provide guidance to the engineer for adding new components. Identifying unexpected side effects (good or bad) between components is also very important.

These various examples lead us to propose the following informal characterization of the assignment problem:

Definition 1 (Assignment Problem, Informally). Given a set of interacting agents, the capabilities of whom are known, given a set of goals, and given an assignment function mapping each goal to a coalition (i.e. a set) of agents, is every goal assigned to a coalition of agents who are able to ensure its satisfaction (including by benefiting from actions of other coalitions)?

The objective of this paper is to formalize this definition and to provide a means to solve the assignment problem. In particular, notice that in this definition, what interaction is is left ambiguous. One of our contributions is precisely to propose multiple acceptations, each of them inducing a particular case of the problem. We call these cases correctness criteria for an assignment. We model the assignment problem and these criteria, and we describe a formal process to check their satisfaction for any instance.

Our approach was originally developed for agent-and goal-oriented RE [CBC11]. In this field, to the best of our knowledge, this provides the first unified formal framework addressing the satisfaction of behavioral goals by operation specifications and the capabilities of agents to perform these operations as required.

Checking the capabilities of agents to ensure goals also enables one to distinguish, given a set of available agents and a set of goals, those goals that the available agents cannot ensure. Then these goals can support the engineer in identifying new agents that should be introduced to fulfill all goals.

Our approach also makes it possible to characterize other sorts of interaction phenomena. Here, we stress the following:

-First, given two coalitions of agents and a goal for each coalition, we highlight dependencies between coalitions w.r.t. the satisfaction of their respective goals.

-Second, in an SoS for instance, we can check whether, while pursuing their own goals, agents in a system S 1 necessarily entail, as a side effect on the global system, that agents in a system S 2 can also ensure their own goals.

The remainder of this article is organized as follows: in Sect. 2 we introduce a minimal modeling framework, called Kore, to allow a proper representation of the situations that we wish to address. In practice, this framework can be seen as a subset of modeling languages such as Kaos or SysML. In the same section, we also introduce a minimal example which will be used in the following sections to illustrate our approach. In Sect. 3, we give a description of the assignment problem in the framework introduced by Sect. 2. To do so, we analyze various modalities of interactions between agents and we devise corresponding correctness criteria for the assignment. This way, the assignment problem is reduced to the problem of satisfaction of the evaluation criteria by an instance of Kore. Then, this problem is itself reduced to a model-checking problem for a multi-agent logic called USL in Sect. 4. Related work is discussed in Sect. 5.

A Modeling Framework for the Assignment Problem

As sketched before, a Kore model is described using a set of goals to be realized, a description of the context given by a number of context properties, a set of agents (considered with their capabilities to act on the system) and an assignment of the goals to (coalitions of) agents. Goals and context properties are temporal properties, so we briefly introduce in Sect. 2.1 the logic that we use to formalize them.

Let us first introduce a running example that will be used throughout this paper to illustrate our approach. In this example, we consider a resource, provided by a provider. Then two clients A and B have different needs w.r.t. this resource. As we will proceed through this article, we will envision three variations of this example.

Example 1 (CP 1 ). In the first version (CP 1 ), the provider can provide up to 15 units of the resource per time unit. It can also decide to which clients the resources are affected. Concretely, at each time unit it provides the clients up to 15 new units as a whole, distributed in variables new A for client A and new B for client B. Each client is able to receive up to 15 units of the resource at a time.

LTL Kore

In our setting, goals are behavioral: therefore we formalize them as well as context properties in a version of Linear Temporal Logic (LTL,[MP95]). Following [Let02,LVL02b,vL09,vL03], we describe an action (of an agent) as the modification of the values of variables describing the state of the sytem. Therefore, in our version of LTL(called LTL Kore ), atomic propositions are comparisons of integer variables and constants.

Definition 2 (Cond). Let X be a set of variables, the set of propositions Cond over X (written Cond (X)) is given by the following grammar:

ϕ ::= x ∼ n | x -y ∼ n | x + y ∼ n | ϕ ∧ ϕ | ϕ ∨ ϕ |¬ϕ
where x, y ∈ X, n is a constant in Z, and ∼ ∈ {<, >, =, , }.

Definition 3 (LTL Kore ). Let X be a set of variables, the logic LTL Kore (X) is the usual Linear Temporal Logic where atoms are taken from Cond(X). It is generated by the following grammar:

ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | Xϕ | ϕUϕ where p ∈ Cond(X).
Because LTL is standard knowledge in formal approaches and due to space constraints, we do not detail the formal semantics of LTL and refer the interested reader to [MP95]. Basically,an LTL Kore (X) formula is interpreted over discrete traces of assignments (instants) for variables in X. A formula Xϕ is true in one of these traces, at a given instant, iff ϕ is true in the same trace at the next instant. A formula ϕ is true in a trace iff ϕ is true at every instant of this trace.

Example 2 (CP 1 (cont.)). Version CP 1 of the client-provider example makes use of the following variables for every c ∈ {A, B} :

a variable res c denotes the amount of resources available for client c at any time t 1. This amount is the sum of:

• the part remaining from the resource in res c at time t -1, denoted old c

• the resources added by provider in res c at transition from time t -1 to t: new c at any time t 2, obt c denotes the amount of resources obtained by c from the amount in store res c at time t -1.

We also write X CP for the set of variables c∈{A,B} {res c , old c , new c , obt c }. Now that LTL Kore has been introduced, let us delve into the concepts necessary to consider the assignment problem as we informally defined it in Sect. 1.

Goals

In Kore, goals are statement describing the behavior expected from the system. They are formalized in LTL Kore .

Example 3 (CP 1 (cont.)). In CP 1 , every client wishes to get a certain amount of the resource: A (resp. B) wants to get at least 6 (resp. 12) units of the resource per unit of time t 2. Their respective goals g A and g B are formalized as follows3 :

[[g A ]] XX( (obt A 6)) [[g B ]] XX( (obt B 12))

Context Properties

Context properties are statements describing the system as it is (as opposed, for instance, to expected properties). In this paper:

-They may be used to specify the set of states of the system, in which case we call them static.

-They may also concern the initial state of the system. In this case, they are called initial properties. They can be formalized using Cond only.

Example 4 (CP 1 (cont.)). In CP 1 we consider the following context properties:

-Static properties:

Res c For any client c, the set of resources in res c is the union of old c and new c . Formally, at any time t 1, the resources available are the sum of the previous ones (remaining from the value of res c at time t -1) and the new ones, gotten from provider:

[[Res c ]] (res c = old c + new c )
Obt c At any time t 1, when a client c takes some resources from the set res c , then at time t + 1, the set old c is the set of resources remaining from res c at time t: at any time t 1 the amount of resources in old c is the amount in res c minus the amount obtained by c at transition from time t -1 to t:

[[Obt c,k ]] (res c = k → X(old c = k -obt c ))
Posi x All the variables in the example stand for the cardinality of some set of resources. Therefore they always have a non-negative value. For each x ∈ X CP :

[[Posi x ]]
x 0 -Initial property Init x : in the initial state of the system, there is none of the resource anywhere. Thus, every variable is initialized to 0. For each x ∈ X CP :

[[Init x ]] x = 0 2.

Agents and Capabilities

Agents are the active entities of the system, likely to ensure or prevent the satisfaction of goals. They are described along with their capabilities. To define the latter, we need to consider a restriction of Cond to a fragment which characterizes finite intervals (windows) only:

Definition 4 (Window conditions). Let X be a set of variables, the language of window conditions, written Cond win (X), is generated by the following grammar:

ϕ ::= a x ∧ x b | ϕ ∧ ϕ | ϕ ∨ ϕ (with x ∈ X, a b and a, b ∈ Z).
Definition 5 (Capability). A capability Cap for an agent a is a pair of a pre-condition Cap.enabCond in Cond(X) and of a window Cap.window, in Cond win (X).

The meaning of a capability is as follows: in each state where the enabCond holds, the corresponding agent can give to the variables appearing in window any values satisfying this window. Indeed, our modeling considers that an agent able to act upon variables is not necessarily able to give them any value at any time. The ∧ connective in Def. 4, is in particular used to link bounds on different variables (see Ex. 5 below). The enabling condition defines the conditions under which an agent can use her capability and change the values of some variables, and the window bounds the set of values she can give to these variables. However, in the example we develop in this article, each window is reduced to a singleton.

Example 5 (Capabilities for all variations of client-provider). The capabilities for the agents in client-provider are given hereafter: Caps. {provide} k+ 15 for provider:

Caps. {get c } 0<k 15 for client c ∈ {A, B}: enabCond :

window

: new A = k ∧ new B = enabCond : res c k window : obt c = k 2.5 Assignment
An assignment is simply a function from goals to coalitions (where every coalition is a set of agents). This can model different kinds of situations; for instance:

-Each agent may be pursuing her own goals (distributed intentionality [Yu09]). In this case the assignment models the relation between a goal and the agent(s) aiming for it. -Or there may be a controller or an engineer, able to constrain and schedule every agent in the model, and who is responsible for the realization of the whole set of goals. In this case the assignment is an affectation, by this controller, of the available resources (the agents) to the satisfaction of the goals.

Example 6 (CP 1 (cont.)). Here we follow the second item, then provider is committed to the realization of both goals, so the assignment A 1 is defined by: A 1 (g A ) = {provider, A} and A 1 (g B ) = {provider, B}.

Evaluation Criteria for Assignment

Now that the different elements of Kore are defined, let us come back to the assignment problem and seek precise criteria modeling the notion of correctness for an assignment. We first give informal definitions for these criteria. Their formalization, which requires first the introduction of the USL framework, is given in Sect. 4.

Local correctness

The first version of the assignment problem we consider is the question whether each goal is assigned to a coalition able to ensure it, whatever the other agents do. We call this criterion the local correctness of the system under consideration. For the client-provider example, this is the question whether {provider, A} is able to ensure the satisfaction of g A (whatever B does) and {provider, B} is able to ensure the satisfaction of g B (whatever A does). We write LC A (G) for the satisfaction of the local correctness of a set of goals G under an assignment A.

Global correctness

The criterion of local correctness is easy to understand and to check. Nevertheless it is not sufficient when, as is the case of CP 1 , one agent is part of several coalitions being assigned different goals. Indeed, provider is able to take part separately in both coalitions {provider, A} and {provider, B}. But the local correctness does not say whether provider is able to take part in both coalitions at the same time. What provider has to do with the first coalition might be contradictory with what she has to do with the second coalition. To overcome this issue, we introduce a second correctness criterion, called the global correctness. Global correctness is satisfied if there is a general behaviour b of all agents s.t. for each goal g, knowing that the coalition of agents assigned to g behaves according to b is enough to ensure g, whatever the other agents do. The notion of such a general behaviour is to be defined as a multi-strategy profile in a CGS, in Sect. 4. If the assignment A of a set of goals G is globally correct, then we write GC A (G).

Collaboration

The global correctness criterion is sufficient to ensure that each goal is assigned to a capable coalition. Nevertheless, it may require more than what is necessary. Indeed, it requires that each coalition is able to ensure its goal in a completely autonomous way (whatever the agents not in this coalition do). In certain cases, it may be necessary to soften this criterion and to admit that some given coalitions depend on others to ensure their goals. To illustrate this point, let us slightly modify our example and consider its second version, CP 2 .

Example 7 (CP 2 ). It brings the following changes from CP 1 :

provider can produce up to 20 units at a time in the new assignment A 2 , provider is assigned a new goal g provider , to produce at least 16 units of the resource per time unit. Furthermore, g A and g B are respectively assigned to {A} and {B}.

In this second version, provider is able, at the same time, to ensure the satisfaction of its goal and to help A and B. By producing, for example, at least 7 units in new A and 13 units in new B , it ensures g provider and the global correction of the model reduced to {g A , g B }. In this case we say that the coalition that is assigned to g provider globally collaborates to the satisfaction of {g A , g B }, and we write Coll A 2 (g provider , {g A , g B }).

Note that a relation of local collaboration could also be defined a similar way.

Contribution

In the three criteria introduced above, we adopted the point of view of an engineer controlling every agent in the system. Thus, we considered our model as a closed system and only asked the possibility for a unique decision-maker to specify the agents so that all goals are ensured. In the case of open systems, the engineer of one system does not control the other systems, which interact with it. Then, a relevant question from the point of view of this engineer is whether the agents from the other interacting systems, by ensuring their goals, necessarily have favorable side effect on its model. This is what we call contribution. Let us consider a last version of our example, CP 3 .

Example 8 (CP 3 ). In this version, A has priority over B: when the provider provides resources in new A at time t, A can get some of them, the remainder is sent to new B and then at time t + 1, B can take some. In order to encode this, we introduce a new variable even marking the evenness of the current time unit (it is equal to 0 at even times and equal to 1 at odd times). A can act during transitions from even to odd time units (let us call them even transitions), and provider and B can act during odd transitions. Again, the provider is able to produce up to 20 units of the resource per odd transition, its goal g provider is changed into providing at least 18 units of the resource per time unit and g A and g B are both assigned to {A, B} in the assignment A 3 . (Fig. 1 gives an overview of the goals and the assignments in the three versions of our example.)

In this version, whatever provider does, if by doing so it ensures the satisfaction of g provider then it provides at least 18 units of the resource per time unit, enabling A and B to ensure the satisfaction of g A and g B . We say that g provider globally contributes to g A and g B and we write Contr A 3 (g provider , {g A , g B }).

Again, one can also define, similarly, a relation of local contribution, that we do not detail here.

CP 1 [[g A ]] XX( (obt A 6)) [[g B ]] XX( (obt A 12)) A 1 (g A ) = {provider, A} A 1 (g B ) = {provider, b} CP 2 [[g provider ]] X( (new A + new B 16)) [[g A ]] cf. CP 1 [[g B ]] cf. CP 1 A 2 (g provider ) = {provider} A 2 (g A ) = {A} A 2 (g B ) = {B} CP 3 [[g provider ]] X( (new A 18)) [[g A ]] cf. CP 1 [[g B ]] cf. CP 1 A 3 (g provider ) = {provider} A 3 (g A ) = {A, B} A 3 (g B ) = {A, B}

Formal Analysis

In this section we introduce the formal framework that we use to check the correctness criteria. Basically, given a specification K conforming to the Kore framework, checking a criterion consists in knowing whether goals in K are assigned to coalitions of agents able to ensure them.

Our approach consists of reducing such a question to a model-checking problem: does a model G (in the logical sense) satisfy a formula ϕ ? where: (1) the model of the possible behaviors of the system is derived from the description of agents and context properties; and (2) the formula expresses that some coalition(s) is (are) able to ensure some goal(s).

To achieve this, a logic that allows to reason about the ability of agents to ensure temporal properties is required. This is the aim of temporal multi-agent logics, such as ATL [AHK02], Chatterjee, Henzinger, and Piterman's Strategy Logic (SL) [CHP10] or USL (Updatable Strategy Logic) [CBC13, CBC15], which is strictly more expressive than the former two, and which we originally proposed to address such issues.

One of the main specific features of USL is that it enables us to express situations where agents may be part of several different interacting coalitions. So, agents in USL can compose their behavior according to the different goals assigned to these coalitions. For this reason, we rely on USL in the following.

In Sect. 4.1, we briefly present USL. Then in Sect. 4.2, we present the reduction of our correctness criteria to instances of the model-checking problem for USL.

A temporal multi-agent logic for the formalization of Kore: USL

Let us first introduce the semantic concepts that are used in USL. Due to space constraints, we refer the reader to [CBC15] for a complete exposition of USL.

Semantic concepts Formulas of USL are interpreted in concurrent game structures (CGS), introduced in [AHK02] and then subsequently used with slight modifications in numerous works [BDCLLM09, DLLM10, MMV10, MMPV14]4 . Intuitively, a CGS is an extension of labelled transition systems dedicated to modelling multi-agent systems. In these systems, transitions are determined by the actions that agents perform. More precisely, at each state of any execution, each agent plays an action so that a transition is determined. Definition 6. A CGS is a tuple G = Ag, St, s 0 , At, v, Act, tr where :

-Ag is a non-empty finite set of agents, -St is an non-empty enumerable set of states, s 0 ∈ St is the initial state, -At is a non-empty finite set of atomic propositions v: St → P(At) is a valuation function, to each state s it associates the set of atomic propositions that are true in s, -Act is an non-empty enumerable set of actions, -Let Dec = Act Ag be the set of decisions, i.e. the set of total functions from the agents to the actions. Then tr : St × Dec → St is the transition function: it decides the successor of a state, given this state and the set of actions played by the agents.

The semantics of USL in CGSs is given by plays in a game, that are infinite sequences (s 0 , δ 0 ) • (s 1 , δ 1 ) . . . where for each k ∈ N:

-s k is a state and δ k is a decision -tr(s k , δ k ) = s k+1
In such a game, every agent plays w.r.t. a multi-strategy. A multi-strategy is a function from St * to P(Act): given the current history of the game, it gives a set of possible actions for any agent following it. The datum of one multi-strategy per agent in the game is called a multi-strategy profile.

During the evaluation of an USL formula in a CGS, the data concerning the different multi-strategies played by the agents are stored in a context κ. In a context, an agent may be bound to several multi-strategies, which is a particularity of USL in the field of multi-agent logics. As we will see below, USL also makes use of multi-strategy variables. Then, a context also contains information about the instantiations of multistrategy variables to multi-strategies. We also use the notion of multi-strategy profile for a coalition of agents, which consists of one multi-strategy per agent in the coalition.

Given a context κ binding agents and variables to multi-strategies in a CGS, and given a state s of this CGS, we can define the notion of outcomes of s and κ. It is the set of executions that are possible in the CGS from s if each agent plays only actions that are allowed by all the multi-strategies she is bound to in κ.

Syntax and semantics of USL Let us now present the syntax of USL and an intuition of its semantics. We start by defining USL pseudo-formulas. We distinguish between state pseudo-formulas (interpreted on states, whose operators deal with multistrategies quantification and binding of multi-strategies to agents) and path pseudoformulas (which express temporal properties).

Definition 7 (Pseudo-formulas of USL). Let Ag be a set of agents, At a set of propositions, and X a set of multi-strategy variables. Then, the set of USL (Ag, At, X) pseudoformulas is generated by the following grammar (with p ∈ At, x ∈ X and A ⊆ Ag):

-State pseudo-formulas: ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | x ϕ | (A x)ψ | (A x)ψ -Path pseudo-formulas: ψ ::= ϕ | ¬ψ | ψ ∧ ψ | X ψ | ψUψ
Then, well formed formulas are pseudo-formulas where every quantified multistrategy variable is fresh w.r.t. the scope in which it is introduced. Formally: Definition 8 ((Well formed) formulas). A pseudo-formula ϕ is a (well formed) formula iff for any sub-formula x ϕ of ϕ and for any sub-formula y ϕ of ϕ , x and y are distinct variables.

Here we do not detail the definition for the relation of semantic satisfaction for USL (| = USL ). We just give an intuition for the main operators:

-The operator x is an existential quantifier over multi-strategies: a formula x ϕ is true in a state s of a CGS G, under context κ, iff there is a multi-strategy σ s.t. the formula ϕ is true in s and G under the context κ enriched by the fact that x is instantiated by σ. -The operator (A x) is a binding of agents in A to the multi-strategy instantiating

x in the current context: a formula (A x)ψ is true in a state s of a CGS G, under context κ, iff the formula ψ is true in any execution in the outcomes of s and κ[A⊕x],

where κ[A ⊕ x] is the context κ enriched with the fact that agents in A are now bound to the multi-strategy instantiating x in κ (in addition to the multi-strategies they were already bound to in κ, if there are some). In USL, this set of outcomes may be empty (if there are agents bound to multi-strategies in empty intersection in the context). In such a case, the current execution stops.

-(A

x) unbinds agents in A from the multi-strategy instantiating x in the current context: it is interpreted in a similar way as (A

x), except that the binding of agents in A to x is deleted from the current context (instead of being added).

-The semantics of temporal operators follows the classical definition of their interpretation in possibly finite executions [EFH + 03]. In the following, given a possibly finite execution λ and an integer i, we write λ i for the sequence obtained from λ by deleting its i first elements:

• A formula X ψ is true in λ iff λ contains at least two states and ψ is true in λ 1 .

• A formula ψ 1 Uψ 2 is true in λ iff there is i ∈ N s.t. λ contains at least i + 1 states, ψ 2 is true in λ i and for all 0 j < i, ψ 1 is true in λ j .

Reduction of the assignment problem to the model-checking of USL

Using USL, we can reduce the satisfaction problem for the assignment correctness criteria from Sect. 3 to instances of model-checking. First, notice that from the description of agent capabilities in an instance K of Kore, and from the set of context properties for K, one can derive a CGS G K . For the sake of simplicity, we do not detail this translation here. Basically:

-Agents of G K are those of K, the set of states in G K is the set of possible instantiations for the variables in K which respect the static context properties, the initial state of G K is chosen non-deterministically within those satisfying the initial context properties, the set of atomic propositions is the set of propositions in Cond that are used in K for the description of goals or for the description of agents capabilities, the valuation function is given by the natural evaluation of Cond formulas in variables instantiations, the transition function encodes the capacities of agents to change the value of variables, according to the description of their capabilities in K.

Then, thanks to USL formulas, we can express that coalitions of agents ensure the satisfaction of the different correctness criteria for K. The formalization of the criteria are given in Def. 9. It makes use of the following notations:

--→ x denotes a vector of multi-strategy variables (one can see it as a multi-strategy profile variable). Then, for any coalition of agents A = {a 1 , . . . , a n }, the notation (A, -→ x ) abbreviates the sequence (a 1 , x a 1 ), . . . (a n , x a n )

for a variable x, x is the universal quantifier over x. It is the dual operator of x . In other words, for any USL formula ϕ, x ϕ ¬ x ¬ϕ.

Definition 9 (Formalisation of the correctness criteria in USL). Let K be an instance of Kore with assignment A. Let G be a set of goals in K and let g be a goal in K s.t.

g G. Then:

[[LC A (G)]] g∈G - → x g (A(g) - → x g )[[g]] [[GC A (G)]] - → x g∈G (A(g) - → x g )[[g]] [[Coll A (g, G)]] - → x g (A(g) - → x g ) [[g]] ∧ [[GC A (G)]] [[Contr A (g, G)]] ( y g (A(g) - → x g )[[g]]) ∧ - → x g (A(g) - → x g )[[g]] → (A(g) - → x g )[[GC A (G)]]
Thus, for any correctness criterion C from Sect. 3, and for any instance K of Kore, the satisfaction of C by K is formalized by the relation

G K | = USL [[C]].
Let us discuss on the formulas in Def. 9.

-The assignment is locally correct iff for each goal g, there is a multi-strategy profile s.t., by playing it, the agents to which g is assigned can ensure its satisfaction. Hence, we check the satisfaction of this criterion by considering one (possibly different) multi-strategy profile per considered goal.

B . So, --→ x g A (A, provider --→ x g A )[[g A ]] ∧ --→ x g B (B, provider --→ x g B )[[g B ]] is true: G CP 1 | = USL [[LC A 1 ({g A , g B })]].
-For the global correctness, we consider one single multi-strategy profile, which imposes on each agent to act in a coherent way. The assignment is globally correct iff there is a multi-strategy profile -→ x s.t. for each goal g, if the agents in the coalition A(g) play according to -→ x (in the definition, we note -→ x g the part of -→ x that concerns the agents in Ag), then they ensure the satisfaction of g. We can easily see that [[GC A 1 (G)]] is not true in G CP 1 . Indeed, provider cannot play a multi-strategy that satisfies both g A and g B at the same time. (According to its capabilities, provider cannot deliver more than 15 units of the resource at a time). -To ensure that a goal g globally collaborates to a set of goals G, we need a multistrategy profile -→ x s.t., if followed by the agents in A(g), -→ x ensures at the same time that:

• g is satisfied • the evolution of the model is constrained in such a way that the assignment A becomes globally correct for the set of goals G. According to this definition, the example g prov globally collaborates to g A and g B in CP 2 (see Sect. 3.3). Indeed, since it may produce up to 20 units of the resource per time unit, provider can play a multi-strategy that will allow both A and B to ensure their respective goal. Furthermore, recall that A 2 (g A ) is reduced to {A} and A 2 (g B ) is reduced to {B} and observe that CP 2 is not globally correct: to be able to ensure their goals, A and B depend on the multi-strategy played by provider.

-The contribution relation is an universally quantified variant of the collaboration : a goal g globally contributes to a set of goals G iff

• the agents in A(g) are able to ensure g,

• for any multi-strategy profile -→ x g that makes A(g) ensure g, -→ x g also makes A(g) constrain the evolution of the system in a way that G becomes globally correct. In CP 2 , by playing, for example, the multi-strategy consisting in setting new A to 5 and new B to 11, provider ensures its goal of producing at least 16 units per time unit, but it prevents A and B to ensure both goals g A and g B . On the other hand, in CP 3 , the satisfaction of g provider (providing at least 18 units of the resource) by the provider allows A an B to ensure their goals, provided the new assignment of both g A and g B to {A, B}.

So [[Contr A 3 (g prov , {g A , g B })]] is true in G CP 3 .
Theorem 1. The possible entailment relations between our correctness criteria for the assignment are given in the following figure, where arrows 1, 2 and 3 represent a strict entailment relation, and the crossed out arrow 4 means that there is no entailment between GC A (G) and Contr A (g, G\{g}), in either direction. Each arrow should be read by universally quantifyfing the assignment A, the set of goals G and any goal g ∈ G.

For example:

-Entailment For any instance K of Kore with assignment A and for any subset G of goals in K, for any g ∈ G, if

G K | = USL [[GC A (G)]] then G K | = USL [[Coll A (g, G\{g})]].
-Strictness It is not true that for any instance K of Kore with assignment A and for any subset G of goals in K, for any g ∈ G, if

G K | = USL [[Coll A (g, G\{g})]] then G K | = USL [[GC A (G)]]. LC A (G) GC A (G) Coll A (g, G\{g}) Contr A (g, G\{g}) 1 2 3 / 4
Proof (sketch). Each item in this proof sketch refers to the arrow in figure above that has the corresponding label.

1. Entailment : straightforward. Strictness: as seen in Sect. 4.2, CP 1 provides a counterexample. 2. Entailment: suppose there is a general multi-strategy profile -→ x s.t., by playing it, every coalition ensures its goal. Then, by playing along -→ x , the agents in g ensure at the same time the satisfaction of g and the global correction of the model reduced to G \ {g}. Strictness: as seen in Sect. 4.2, CP 2 is a counterexample for the converse. 3. Entailment : straightforward. Strictness: goal g provider in CP 2 provides a counterexample: by playing multi-strategies allwaysNew A = 5 and allwaysNew B = 11, provider ensures g provider but prevents the satisfaction of g A and g B by the other agents. 4. Left to right: CP 3 satisfies Contr A 3 (g provider , GC({g A , g B })) but, to be able to ensure their goals, A and B depend on the satisfaction of g provider by provider, so GC A 3 ({g A , g B }) is not true. Right to left: consider a minimal example where provider is able to provide 5 units of the resource per time unit, and is assigned both goals g -to provide 2 units, and g + to provide 4 units. This model is globally correct but g -does not contribute to {g + }.

This work was initially developed in the context of Requirements Engineering [CBC11] and took inspiration from the state-of-the-art in this domain, in particular from Kaos [vL09,LVL02b,Let02]. In this method, goals are gradually refined until reaching socalled requirements. Then, agents are assigned the responsibility of realizing the latter by relying on operations (our agents are directly assigned goals to simplify the presentation). In some developments of Kaos, a notion of controllable and monitorable conditions [LVL02a, vL04] is used as a criterion of satisfiability of realization: an agent can perform an operation if it monitors the variables in its pre-conditions and controls the ones in its post-conditions. So, in Kaos and contrary to Kore, (1) capabilities are not conditioned by the state of the system; and (2) agents interactions are not analyzed.

Another important RE approach is Tropos [CDGM10a, CDGM10b, MS06, CS09]. In this line of work, a notion of role is introduced which gathers a set of specifications to be satisfied by the system. The two notions of agents and roles are then confronted. The adequacy between them is examined using propositional logic: roles are described through commitments and agents may ensure these depending on their capabilities. Considerations on time and interactions between agents are only led using natural language. Thus the method makes the verification of questions of the sort: "can agent a ensure transition tr?" possible. But the possible interactions between agents, as modifications of the common environment, are not considered formally. Kore precisely aims at unifying the multi-agent and behavioral aspects.

On the logical side, ATL and ATL* [AHK02] consider the absolute ability of coalitions to ensure propositions whatever other agents do. But there is no contextualization w.r.t. the strategies followed by different agents. More recently, this contextualization was considered for ATL* [BDCLLM09]. This proposition only uses implicit quantification over strategies for coalitions, preventing from considering different strategy quantifications for a given coalition. This problem was also tackled in SL [MMV10] where quantification over strategies is made using explicit variables. Our logic USL was first developed in [CBC13, CBC15]. Its syntax is inspired by that of SL, but it contains in addition treatment for the composition of several multi-strategies for a given agent.

Conclusion and Future Work

In this article, we proposed a framework to model the assignment of behavioral goals to agents, described with capabilities. Then, we addressed the evaluation of such an assignment, informally referred to as the assignment problem. We proceed in two steps:

-Rather than defining one criterion that would provide a unique "yes or no" answer, we think it is more relevant to define several correctness criteria, each involving a different level of interaction between agents. We compared these criteria through a logically defined entailment relation between them. -We provide a formalization of the different criteria using a temporal multi-agent logic, USL, and we reduce the verification of these criteria to the model-checking problem of this logic.

As a future work, the relevance of new correctness criteria for the assignment could be investigated. A direction would be to develop a formal language dedicated to the specification of criteria, using the satisfaction of goals by the coalitions they are assigned to as atoms, and the relations between these goals as operators. Thanks to such a language, we could extend and refine the criteria that can be checked in Kore.

Another direction is to study dependence relations between the multi-strategies that are played by the different coalitions. In the contribution relation for example, a coalition A 1 is able to find a favorable multi-strategy profile, whatever another coalition A 2 does (because of the nesting of multi-strategy quantifiers). In other words, A 1 knows the whole multi-strategy profile chosen by A 2 when choosing its own multi-strategy profile, which is a very strong assumption. However, it is possible in USL to characterize several forms of independence of A 1 's multi-strategy profile with respect to A 2 's multi-strategy profile, so that this question could be integrated in the definition of new correctness criteria.

In [CBC15], we proved that the model-checking problem for USL is decidable, but does not support any elementary bound. Nevertheless, we have a strong conjecture stating that the restriction of USL to memoryless multi-strategies is decidable in PSPACE. Thus, restricting to memoryless multi-strategies appears as an important condition for a tractable use of our proposition. Then, research should be led in order to further characterize the class of systems for which a memoryless semantics is adequate.

Finally, it can happen that some goals are not fully achievable by the agents they are assigned to. Especially, so called soft goals don't have any clear cut satisfaction criterion. Then, considering and searching the best multi-strategies with regards to these goals would rise further analyses. Different notions of optima are indeed expressible in USL and could be used for defining different notions of optimal multi-strategies.

Fig. 1 :

 1 Fig. 1: Goals and assignments in the client-provider example

  Let us consider for instance CP 1 from Examples 3 and 5. We see that provider can play the multi-strategy al-waysNew A 6 (consisting in restricting to the choices of values for new A and new B s.t. new A 6 at any time of the execution) and, if provider does so, A can play alwaysObt A 6 so that g A is ensured. Similarly, by playing respectively alwaysNew B 12 and alwaysObt A 12, provider and B can ensure g

We use double brackets[[•]] to denote the formalization of an informal property.

As USL builds upon SL, our definition for CGS is the one from [MMV10, MMPV14].


Julien Brunel

David Chemouil

Safety and Security Assessment of Behavioral Properties Using Alloy

Keywords: Logic, Formal Methods, Alloy, Safety and Security

In this paper, we propose a formal approach to supporting safety and security engineering, in the spirit of Model-Based Safety Assessment, using the Alloy language. We first implement a system modeling framework, called Coy, allowing to model system architectures and their behavior with respect to component failures. Then we illustrate the use of Coy by defining a fire detection system example and analyzing some safety and security requirements. An interesting aspect of this approach lies in the "declarative" style provided by Alloy, which allows the lean specification of both the model and its properties.

Introduction

In the context of critical systems engineering, formal approaches have been used for a long time with great successes. In particular, in order to support safety analyses, an approach called Model-Based Safety Assessment (MBSA) [START_REF] Bozzano | Esacs: an integrated methodology for design and safety analysis of complex systems[END_REF] has been proposed. The language AltaRica [START_REF] Arnold | The altarica formalism for describing concurrent systems[END_REF] and associated tools is one the main techniques used in MBSA. It allows to model system architectures as a set of communicating automata (one automaton per function or system, depending on the level of abstraction retained for the system under study) and then to study the impact of failure or erroneous events. Then, for instance, fault trees may be generated, the impact of events can be simulated or some property can be assessed exhaustively using a model-checker. Besides, some security properties can also be addressed with the same kind of approach as the language is in fact agnostic with respect to the nature of feared events.

Following earlier work, we propose here to address the question of safety and security assessment using the Alloy language and the Alloy Analyzer free-software tool. Alloy [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF] is a formal modeling language amenable to automatic analyses. Alloy has recently been used in the context of security assessment, for instance to model JVM security constraints [START_REF] Reynolds | Lightweight modeling of java virtual machine security constraints[END_REF], access control policies [START_REF] Toahchoodee | Using alloy to analyse a spatio-temporal access control model supporting delegation[END_REF], or attacks in cryptographic protocols [START_REF] Lin | Modeling partial attacks with alloy[END_REF]. Besides, we proposed in earlier works a study of the safety and security assessment of an avionic system supporting an approach procedure [START_REF] Brunel | Formal modelling and safety analysis of an avionic functional architecture with alloy[END_REF][START_REF] Brunel | A viewpoint-based approach for formal safety & security assessment of system architectures[END_REF][START_REF] Brunel | Formal safety and security assessment of an avionic architecture with alloy[END_REF].

Our motivation for relying on Alloy instead of, say, AltaRica is to take benefit from the model-based aspect of Alloy and its expressiveness for the specification of the properties to check. Indeed, Alloy allows to define metamodels easily, which allows for instance to devise domain-specific metamodels. Here, as will be seen, we develop in Alloy a modeling framework called Coy which can be partly seen as the embedding of the general concepts of AltaRica into Alloy (ignoring concepts we do not need). Furthermore, with Alloy, the specification of the properties we check is expressed in relational first-order logic, with many features adapted to model-based reasoning.

With respect to our previous propositions around using Alloy for MBS&SA, we devise here a richer architectural framework and, more importantly, we formalize a notion of behavior so as to be able to check properties of the considered system along time.

Thus, this paper is organized as follows: in Sect. 2, we give a very brief account of Alloy. Then, in Sect. 3, we describe the Coy modeling framework that we implemented in Alloy to model system architectures and their behavior. We show how Alloy is well adapted to designing domain-specific metamodels and to getting some flexibility in the modeling of time and behavior. In Sect. 4, we illustrate our approach on a fire detection example that we model in Alloy following the Coy metamodel. In particular, we show how using Alloy allows to express "in one shot" properties ranging over a set of elements selected by navigating in the model structure.

Alloy in a Nutshell

Alloy is a formal modeling language that is well adapted to the following (non-exhaustive) list of activities: abstract modeling of a problem or of a system; production of a metamodel (model corresponding to a viewpoint); analysis of a model using well-formedness or formal semantic rules; automatic generation of an instance conforming to a model, possibly according to supplementary constraints; finding interesting instances of a model. Models designed in Alloy can deal with static aspects only, or integrate also dynamic aspects, so as to check behavioral properties.

We now give a brief glance at the main concepts of the language using a simple example.The most important type of declaration is that of a signature which introduces a structural concept. It may be seen as a class or entity in modeling parlance. A signature is interpreted as a set of possible instances; and it can also come with fields that may be seen, as a first approximation, as class attributes or associations.

sig Data { consumedBy : some System } sig System {} sig Criticality { concernedData : one Data, concernedSystem : one System } Here, we defined 3 concepts : Data, System and Criticality. Alloy advocates not to delve into unnecessary details and only give information on things we want to understand or analyze. Thus, here, a system is just defined to be a set of "things", but we do not say anything about the exact nature of its elements.

The keywords some or one give details on the multiplicity of the relation, as 1..* and 1 in UML. Here the field declarations mean that: every datum is consumed by at least one (some) system; every criticality concerns exactly one (one) data and one system. Other possible multiplicities are: lone which means at most one (0..1); and set which means any number (0..*).

Then, we can add constraints on possible instances of our model. For instance, we would like to state that every system consumes at least one datum. This can be done by writing additional facts (facts are axioms, so as few facts as possible should be stated in order to avoid over-specification): fact { // every system consumes at least one datum all s : System | some consumedBy.s // for any system which consumes a given datum, the said datum and system // should belong to a same unique criticality

all d : Data | all s : System | one c : Criticality | c.concernedData = d and c.concernedSystem = s }
The . operator yields the join of two relations, matching the last column from the first one to the first column of the second one. Thus one may write d.consumedBy to get the systems consuming a data d, but also consumedBy.s to get the data consumed by the system s.

The formal foundation of Alloy is relational first order-logic, that is first-order logic extended with relational terms (including the transitive closure of a binary relation). Besides allowing navigation in models, this logic suffices to encode various models of time (e.g. to go from a linear to a tree view of time, or to give either an interleaving or a true-concurrency semantics).

Finally, although the language does not preclude unbounded verification in principle, in practice the Alloy Analyzer works only on finite models, reducing a given problem to a SAT instance the analysis of which is delegated to an off-the-shelf SAT solver. Then Alloy may be used to carry out some explorations (the command run builds instances that satisfy a given statement) or to check whether a given assertion is satisfied by all instances of the model (command check). Therefore, as analysis is sound but carried out on finite instances only, the Alloy Analyzer is able to find counter-examples up to a certain bound but it cannot prove the validity of an assertion. This is not a problem in our case because (1) the system architecture we consider is fixed in advance so its number of instances may not vary and (2) only time (i.e. the size of the time model) may be unbounded but, in our analyses, we do not aim at proving the absence of errors but rather that a bounded number of events does not lead to a feared situation (which induces that bounded time is sufficient).

The Coy Modeling Framework

We now present the Coy modeling framework, implemented as a metamodel in Alloy (i.e. a model where each signature is abstract and only instantiated in a second model corresponding to the system under study). We take inspiration in model-based safety assessment but our formalization is not specific to this sole family of properties.

As will be seen hereafter, Coy models essentially represent hierarchical structures of transition systems communicating instantaneously through data ports.

The overall structure of the framework is presented graphically in Fig. 1. Extension links are figured using black dashed arrows. As the metamodel contains n-ary relations with n > 2, the figure shows these after projection on parts of their domain (this is indicated using square brackets, as in conns[Port] for instance). Furthermore, the metamodel contains a Time signature: its purpose is that every signature field with Time as its last column can be conceptually seen as mutable field, i.e. its value may change (discretely) over time. Notice that the metamodel in Fig. 1 is projected over Time, hence it is not shown in the diagram.

Composite Structure

Let us now delve into more details in the metamodel (in what follows, for the sake of readability, we do not show all Alloy facts enforcing the well-formedness of instance models or just classical properties). The basic architectural element is a node. Nodes are arranged hierarchically as a tree, so we use the classical Composite design pattern and devise a notion of AbstractNode which is inherited by signatures CompositeNode and LeafNode, the former pointing back to abstract nodes.

Every node comes with a set IPort of input ports and a set OPort of output ports. These sets are disjoint and every port belongs to a single node. Every port carries a value at every instant (possible values may differ for distinct ports).

Connections (between ports) are constrained so that they cannot cross a parent node boundary or many levels of composition. In other words, nodes are arranged as trees and connections can only happen between siblings or between a parent and a child. Furthermore, connected ports always carry the same value.

abstract

Behavior

As Coy is mainly aimed at describing systems where atomic nodes are endowed with behavior, we now introduce a notion of state (for leaf nodes) and of events that may happen. One approach to deal with such models could be to rely on classical modelcheckers, such as Spin [START_REF] Holzmann | The model checker spin[END_REF] or NuSMV [START_REF] Cimatti | Nusmv: A new symbolic model verifier[END_REF], the modeling languages of which are wellsuited to describing transition systems. While this is of course a possibility, our aim with using Alloy is:

to be able to easily adapt the Coy metamodel depending on the domain of study (e.g. to add a notion of connectors as in many architecture-description languages); as explained earlier, to change the model of time if need be (e.g. to go from a linear to a tree view of time, or to give either an interleaving or a true-concurrency semantics); and above all to allow the use of logic for specification, which brings two interesting aspects:

1. it provides a single language to specify both models and expected properties; 2. the logic allows for the expression of rather abstract properties (e.g. relying on under-specification) or to navigate through elements of a model to specify a given property in only one formula.

Thus, every leaf node is in one given state at any time (the set of possible states may vary for two different nodes). Besides, such nodes may undergo events. An event is an instance of an event type that happens at a certain instant and concerns a given node: this distinction between events and event types then allows to consider events of a certain type only, for instance to characterize their effects.

Notice also we impose the end-user to give, for any leaf node, the set of its possible states and the set of event types that concern it: this is a bit redundant from the theoretical point of view but it provides a sort of additional safety check akin to a poor man's typing that we deem important from a methodological point of view.

abstract

Fire detection example

In this section, we provide an illustration of Coy with a fire detection system in facility such as, for example, an airport or a port.

Presentation of the system

The system consists of the following components: a smoke detector and a heat detector, which are part of the automatic fire alarm system; a manual fire alarm pull station; the local firemen, inside the facility; and the city firemen, in the nearest city.

The automatic fire alarm system, which is activated by either of the two detectors, directly calls the city firemen. The manual pull station, triggered by a human present on site, calls both the local and the city firemen.

We also represent two possible failures for each of the components: (1) the loss of a component: once a component is lost, it does not send any information, (2) an erroneous failure of a component: after this kind of failure, a component sends a corrupted data (in the case of a fire detector, for instance, it can be a false alarm or a false negative). Lastly, we represent three security threats: (1) intentional wrong activation of the pull station, (2) the deactivation of the smoke detector and (3) of the heat detector.

Notice that the loss of a component and the deactivation of the smoke detector (or of the heat detector) have the same effect on a component (the availability is not ensured) although they do not have the same nature (the former is a failure, the latter is a security threat). The same applies to an erroneous failure and the intentional wrong activation of the pull station, which both affect the integrity of the information. Nevertheless, it is important to distinguish between these failure and threat events in order to allow a pure safety analysis, a pure security analysis, and a combined analysis.

Coy model

The Coy model of this system imports the Coy metamodel, declares signatures instances and relates them. Components of the system are modeled as Coy nodes. Fig 2 illustrates a particular instance of the fire detection model at a given instant. As can be seen, at this instant, all nodes are in the state OK and all ports yield a correct data (modeled by OKVal). The occurrence of an event of type failLoss (see the declaration of event types below) can be observed on the node pullStation.

Regarding the possible failures and threats mentioned above, we use the following event types, node states and possible values for the node ports. The model also comprises axioms stating what happens to nodes depending on observed events. An interesting point here is that this description is declarative and does not depend on the effective nodes and ports. Concerning an event of type failLoss:

the event can only occur on a node which is not in the state Lost, after the occurrence of the event, the node moves to the state Lost.

Here, we chose to model events of type threatBlock in the same way (the node also moves to the state Lost). So, they have the same effect (but they do not occur on the same components). In further analysis, if we want to distinguish between the effects of both kinds of events, we just have to use a specific node state and a specific port value corresponding to the occurrence of threatBlock.

The behavior of events of type failErr and threatPull are specified in a similar way. The following assertions express the robustness of some parts of the system to possible failures/threats. We took benefit from the possibility to reason about a set cardinality in Alloy. Here, we count the number of events (corresponding to failures/threats) that occurred before the system enters a bad situation. For instance, the following assertion expresses that in order to make both local and city firemen unable to act properly, either the threat threatPull has occurred, or there has been at least two distinct failures/threats. Remark that it would have been also possible to reason independently about the number of failures and about the number of threats. In order to assertions, Alloy Analyzer searches for counter-examples up to a certain bound (i.e. the counter-examples are such that their signatures have a cardinality less than the bound). The bound can be given by the user or chosen by the tool. In general, this bounded verification is thus incomplete: the tool may not find counterexamples whereas there are some. But in our case, the cardinality of all the signatures (nodes, ports, etc.) is fixed by the model itself. Therefore, the verification performed by Alloy Analyzer is complete.

The last four assertions have been validated by Alloy Analyzer (it does not find any counter-example).

The following assertion expresses that in order to make both local and city firemen unable to act, there has to be at least three failures/threats in the architecture. This last assertion is not satisfied by the model. Alloy Analyzer exhibits a counterexample where the pull station and the city firemen are lost after two events (Fig. 2 shows the first time step of this counter-example, Fig 3 shows the next time steps).

Conclusion and Future Work

In this article, we presented a framework, called Coy, to model and assess safety and security properties of behavioral models. We have chosen to embed it in Alloy so that we can benefit from its model-based features and its expressiveness for the specification of the properties to check. A Coy model essentially describes transition systems communicating through data ports (note that other means of communication, such as synchronization of transitions, are also possible). We illustrated Coy through an example of a fire detection system, and showed it is suited to the specification of failures and threats propagation along the system. We were able to check properties over this system, and to generate counter examples for the violated properties.

In this work, the security aspects are not developed (we have just considered three threats that have the same kind of effects as failures). However, recent works have showed the relevance of Alloy to assess more advanced security properties [START_REF] Lin | Modeling partial attacks with alloy[END_REF][START_REF] Reynolds | Lightweight modeling of java virtual machine security constraints[END_REF][START_REF] Brunel | Formal safety and security assessment of an avionic architecture with alloy[END_REF]. Moreover, it was shown that using AltaRica, one can specify the effect of richer security threats over a system architecture [START_REF] Bieber | From safety models to security models: Preliminary lessons learnt[END_REF] and check related security properties. This is in favor of using Coy to model and assess security of more complex systems architectures, where both concerns are rich and interact with each other.

Fig. 1 :

 1 Fig. 1: Graphical depiction of the Coy metamodel (projected over Time)

  one sig failLoss, failErr, threatBlock, threatPull extends EventType {} one sig OK, Lost, Err extends State {} one sig OKVal, LostVal, ErrVal extends Value {} Then, we can declare the components and ports, as instances of the corresponding Coy concepts. For instance, here is the declaration of the fire pull station. one sig pullStation extends LeafNode {} { input = none and output = oPullStation possibleStates = OK +Lost +Err and possibleEventTypes = failLoss +threatPull }

Fig. 2 :

 2 Fig. 2: detection model example (see also Fig. 3 for following time steps); leaf nodes are beige rectangles, output ports are red trapeziums, input ports are green trapeziums and connections between ports are blue arrows.

check noSingleFailureThreatLeadsToFiremenNotOK for 10

 10 assert noDoubleFailureThreatLeadsToFiremenNotOK { all t : Time | OKVal not in (localFiremen +CityFiremen).output.val.t

( a )Fig. 3 :

 a3 Fig. 3: Counter-example for assertion noDoubleFailureLeadsToFiremenNotOK (follow-up from Fig. 2)

  sig Port { // a port carries one value at every instant val : Value one →Time } abstract sig IPort, OPort extends Port {} abstract sig AbstractNode { // input and output ports input : set IPort, output : set OPort } abstract sig CompositeNode extends AbstractNode { // a composite node contains at least one sub-node subs : some AbstractNode, // port connections with siblings and between sub-nodes and this node conns : subs.@output →subs.@input +input →subs.@input +subs.@output →output, } { // connected ports always carry the same value all t : Time, po, pi : Port | po→pi in conns implies po.val.t = pi.val.t // +other structural properties ... } abstract sig LeafNode extends AbstractNode { ... }

  sig LeafNode extends AbstractNode { possibleStates : some State, state : possibleStates one →Time, possibleEventTypes : set EventType, } abstract sig EventType {} abstract sig Event { // event occurrence instant : one Time, node : one LeafNode, type : one EventType } { type in node.possibleEventTypes } Finally, as Alloy does not feature a native notion of time, we encode it by characterizing finite traces of instants. The fact accounting for this says how states change depending on events, at every instant.

fact traces { // if a node state changed, there was an event concerning this node all t : Time, t' : t.next, n : LeafNode { n.state.t =n.state.t' implies some e : Event { e.instant = t e.node = n } } }

  Time | OKVal not in (localFiremen +CityFiremen).output.val.t implies some e : Event | e.type = threatPull and lt[e.instant, t]

	assert noSingleFailureThreatLeadsToFiremenNotOK {
	all t :

The propagation of values is also described by an Alloy fact. For example, here is the description of the value propagation for leaf nodes with one input:

Properties verification

Now we can express the safety and security properties that we want to check as Alloy assertions. We have mainly expressed properties related to the consequence of some failures/threats or to the robustness of the system to a given number of failures/threats. For instance, the following assertion states that whenever the smoke detector is lost (and all other nodes are OK) then the firemen can still act. The following assertion expresses that whenever the pull station is attacked, (and all other nodes are OK) then at least one firemen department is able to act. Notice that the first-order quantifiers and the object-oriented syntax allows to navigate easily through the model and is convenient to state safety properties.

The following assertion expresses that whenever the smoke detector is erroneous and the pull station is attacked threatPull, then both local and city firemen are unable to act.