Lucian Bentea

Peter Csaba Ölveczky

A Probabilistic Strategy Language for Probabilistic Rewrite Theories and its Application to Cloud Computing

Several formal models combine probabilistic and nondeterministic features. To allow their probabilistic simulation and statistical model checking by means of pseudo-random number sampling, all sources of nondeterminism must first be quantified. However, current tools offer limited flexibility for the user to define how the nondeterminism should be quantified. In this paper, we propose an expressive probabilistic strategy language that allows the user to define complex strategies for quantifying the nondeterminism in probabilistic rewrite theories. We have implemented PSMaude, a tool that extends Maude with a probabilistic simulator and a statistical model checker for our language. We illustrate the convenience of being able to define different probabilistic strategies on top of a system by a cloud computing example, where different load balancing policies can be specified by different probabilistic strategies.

We then use PSMaude to analyze the QoS provided by different policies.

Introduction

Many formal analysis tools support the modeling of systems that exhibit both probabilistic and nondeterministic behaviors. To allow their probabilistic simulation and statistical model checking using pseudo-random number sampling, the nondeterminism must be quantified to obtain a fully probabilistic model. However, there is typically limited support for user-definable adversaries to quantify the nondeterminism in reasonably expressive models; such adversaries are either added by the tool or must be encoded directly into the system model.

In this paper we propose an expressive probabilistic strategy language for probabilistic rewrite theories [START_REF] Kumar | Probabilistic rewrite theories: Unifying models, logics and tools[END_REF][START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF] that allows users to define complex adversaries for a model, and therefore allows us to separate the definition of the system model from that of the adversary needed to quantify the nondeterminism in the system model.

Rewriting logic is a simple and expressive logic for concurrent systems in which the data types are defined by an algebraic equational specification and where the local transition patterns are defined by conditional labeled rewrite rules of the form l : t -→ t if cond , where l is a label and t and t are terms representing state fragments. Maude [START_REF] Clavel | All About Maude[END_REF] is a high-performance simulation, reacha-bility, and LTL model checking tool for rewriting logic that has been successfully applied to many large applications (see, e.g., [START_REF] Meseguer | A rewriting logic sampler[END_REF][START_REF] Martí-Oliet | Rewriting logic: roadmap and bibliography[END_REF] for an overview).

Rewriting logic has been extended to probabilistic rewrite theories [START_REF] Kumar | Probabilistic rewrite theories: Unifying models, logics and tools[END_REF][START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF], where probabilities are introduced by new variables in the righthand side t of a rewrite rule. These variables are instantiated according to a probability distribution associated with the rewrite rule. Probabilistic rewrite theories, together with the VeStA statistical model checker [START_REF] Sen | VeStA: A statistical model-checker and analyzer for probabilistic systems[END_REF], have been applied to analyze sensor network algorithms [START_REF] Katelman | Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking[END_REF] and defense mechanisms against denial of service attacks [START_REF] Alturki | Probabilistic modeling and analysis of DoS protection for the ASV protocol[END_REF][START_REF] Eckhardt | Stable availability under denial of service attacks through formal patterns[END_REF]. However, since the probabilistic rewrite theories were highly nondeterministic, adversaries had to be encoded into the model before any analysis could take place.

Probabilistic model checking suffers from state space explosion which renders it unfeasible for automated analysis of the complex concurrent systems targeted by rewriting logic. Statistical model checking [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF][START_REF] Younes | Probabilistic verification of discrete event systems using acceptance sampling[END_REF][START_REF] Sen | On statistical model checking of stochastic systems[END_REF] trades absolute confidence in the correctness of the model checking for computational efficiency, and essentially consists of simulating a number of different system behaviors until a certain confidence level is reached. This not only makes statistical analysis feasible, but also makes such model checking amenable to parallelization, which is exploited in the parallel version PVeStA [START_REF] Alturki | PVeStA: A parallel statistical model checking and quantitative analysis tool[END_REF] of the statistical model checker VeStA. PVeStA has recently been used to analyze an adaptive system specified as a hierarchical probabilistic rewrite theory [START_REF] Bruni | Modelling and analyzing adaptive self-assembly strategies with Maude[END_REF].

To support the analysis of probabilistic rewrite theories where our strategy language has been used to quantify all nondeterminism, we have formalized and integrated into (Full) Maude both probabilistic simulation and statistical model checking. Our strategy language and its implementation, the PSMaude tool [START_REF] Bentea | The PSMaude tool home page[END_REF], enable a Maude-based safety/QoS modeling and analysis methodology in which:

1. A non-probabilistic rewrite theory defines all possible behaviors in a simple "uncluttered" way; this model can then be directly subjected to important safety analyses to guarantee the absence of bad behaviors. 2. Different QoS policies and/or probabilistic environments can then be defined as probabilistic strategies on top of the basic verified model for QoS reasoning by probabilistic simulation and statistical model checking.

We exemplify in Section 4 the usefulness of this methodology and of the possibility to define different complex probabilistic strategies on top of the same model with a cloud computing example, where a (non-probabilistic) rewrite theory defines all the possible ways in which requested resources can be allocated on servers in the cloud, as well as all possible environment behaviors. We can then use standard techniques to prove safety properties of this model. However, one could imagine a number of different policies for assigning resources to service providers and users, such as, e.g.,

-Service providers might request virtual machines uniformly across different regions (for fault-tolerance and omnipresence), or with higher probability at certain locations, or with higher probability at more stable servers.

-Service users may be assigned virtual machines either closer to their locations, on physical servers with low workload, or on reliable servers, with high probability.

Each load balancing policy can be naturally specified as a probabilistic strategy on top of the (non-probabilistic) model of the cloud infrastructure that has been proved to be "safe." We then use PSMaude to perform simulation and statistical model checking to analyze the QoS effect of the different load balancing policies.

Preliminaries

Rewriting Logic and Maude. A rewrite theory [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF]

A-equivalent if A (∀ ) C( ) = C ( ). Given [u] A ∈ Can Σ,E/A , its R/A-matches are triples ([C] A , r, [θ] A ) where C is a context, r ∈ R is a rewrite rule, [θ] A ∈ CanGSubst E/A ( x) is such that E ∪ A θ(cond ), and [u] A = [C( ← θ(t))] A .
We denote by M([u] A ) the set of all such triples, and define the set of rules that are enabled for a term [u] A , the set of valid contexts for [u] A and a rule r, and the set of valid substitutions for [u] A , a rule r, and a context [C] A , in the expected way:

enabled([u] A ) = {r ∈ R | ∃[C] A , ∃[θ] A : ([C] A , r, [θ] A ) ∈ M([u] A )} C([u] A , r) = {[C] A ∈ Can Σ,E/A ( ) | ∃[θ] A : ([C] A , r, [θ] A ) ∈ M([u] A )} S([u] A , r, [C] A ) = {[θ] A ∈ CanGSubst E/A ( x) | ([C] A , r, [θ] A ) ∈ M([u] A )}
Maude [START_REF] Clavel | All About Maude[END_REF] is a high-performance simulation, reachability analysis, and LTL model checking tool for rewrite theories. We use Maude syntax, so that conditional rules are written crl [l]: t => t if cond . In object-oriented Maude specifications [START_REF] Clavel | All About Maude[END_REF], the system state is a term of sort Configuration denoting a multiset of objects and messages, with multiset union denoted by juxtaposition.

A class declaration class C | att 1 : s 1 , . . . , att n : s n declares a class C with attributes att 1 , . . . , att n of sorts s 1 , . . . , s n , respectively. A subclass inherits the attributes and rules of its superclass(es). Objects are represented as terms < o : C | att 1 : val 1 , . . . , att n : val n >, where o is the object's identifier of sort Oid, C is the object's class, and where val 1 , . . . , val n are the values of the object's attributes att 1 , . . . , att n . For example, the rule defines a family of transitions in which a message m, with parameters O and w, is read and consumed by an object O of class C. The transitions change the attribute a1 of O and send a new message m'(O', x). "Irrelevant" attributes (such as a3 and the righthand side occurrence of a2) need not be mentioned.

Markov Chains. Given Ω = ∅, a σ-algebra over Ω is a collection F ⊆ P(Ω) such that Ω \ F ∈ F for all F ∈ F, and i∈I F i ∈ F for all collections {F i } i∈I ⊆ F indexed by a countable set I. Given a σ-algebra F over Ω, a function P : F → [0, 1] is a probability measure if P(Ω) = 1 and P (∪ i∈I F i ) = i∈I P(F i ), for all collections {F i } i∈I ⊆ F of pairwise disjoint sets. We denote by PMeas(Ω, F) the set of all probability measures on F over Ω. A probability mass function (pmf) is a function p : Ω → [0, 1] with ω∈Ω p(ω) = 1. A family of pmf's can be used to define the behavior of a (memoryless) probabilistic system. In particular, a discrete time Markov chain (DTMC) is given by a countable set of states S, and a transition probability matrix T : S × S → [0, 1], where T (s) : S → [0, 1] is a pmf for all states s ∈ S, i.e., T (s, s ) is the probability for the DTMC to make a transition from state s to state s . Probabilistic Rewrite Theories. In probabilistic rewrite theories (PRTs) [START_REF] Kumar | Probabilistic rewrite theories: Unifying models, logics and tools[END_REF] the righthand side t of a rule l : t -→ t if cond may contain variables y that do not occur in t, and that are instantiated according to a probability measure taken from a family of probability measures-one for each instance of the variables in t-associated with the rule. Formally, a PRT R π is a pair (R, π), where R is a rewrite theory, and π maps each rule r of R, with vars(t) = x and vars(t ) \ vars(t) = y, to a mapping π r : cond ( x) → PMeas CanGSubst E/A ( y), F r , where cond

( x) = { [θ] A ∈ CanGSubst E/A ( x) | E ∪ A θ(cond ) },
and F r is a σ-algebra over CanGSubst E/A ( y). That is, for each substitution [θ] A of the variables in t that satisfies cond , we get a probability measure π r ([θ] A ) for instantiating the variables y. The rule r together with π r is called a probabilistic rewrite rule, and is written l : t -→ t if cond with probability π r . We refer to the specification of the "blackboard game" in Section 3 for an example of the syntax used to specify probabilistic rewrite rules and the probability measure π r . An E/A-canonical one-step rewrite of R π [START_REF] Kumar | Probabilistic rewrite theories: Unifying models, logics and tools[END_REF][START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF] is a labeled tran-

sition [u] A ([C] A , r, [θ] A ,[ρ] A ) -----------→ [v] A with m ∆ = ([C] A , r, [θ] A ) a R/A-match for [u] A , [ρ] A ∈ CanGSubst E/AS ( y), and [v] A = [C( ← (θ ∪ ρ)(t ))] A .
To quantify the nondeterminism in the choice of m, the notion of adversary is introduced in [START_REF] Kumar | Probabilistic rewrite theories: Unifying models, logics and tools[END_REF][START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF] that samples m from a pmf that depends on the computation history.

A memoryless adversary3 is a family of pmf's {σ

[u] A : M([u] A ) → [0, 1]} [u] A , where σ [u] A (m) is the probability of picking the R/A-match m. A consequence of a result in [18] is that executing R π under {σ [u] A } [u] A is described by a DTMC.
PCTL. The probabilistic computation tree logic (PCTL) [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] extends CTL with an operator P to express properties of DTMCs. We use a subset of PCTL, without time-bounded and steady-state operators. If AP is a set of atomic propositions, φ is a state formula, and ψ is a path formula, PCTL formulas over AP are defined by:

φ ::= true | a | ¬φ | φ ∧ φ | P p (ψ) ψ ::= φ U φ | Xφ where a ∈ AP , ∈ { <, ≤, >, ≥ }, and p ∈ [0, 1]
. PCTL satisfaction is defined over DTMCs, e.g., the meaning of M, s |= P <0.05 (true U φ) is that φ eventually becomes true in less than 5% of all the runs of the DTMC M from state s.

Statistical Model Checking and VeStA. Traditional model checking suffers from state space explosion problem, whereas statistical model checking [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF][START_REF] Younes | Probabilistic verification of discrete event systems using acceptance sampling[END_REF][START_REF] Sen | On statistical model checking of stochastic systems[END_REF] trades complete confidence for efficiency, allowing the analysis of large-scale probabilistic systems. This technique is based on simulating the model, and on performing statistical hypothesis testing to control the generation of execution traces. The simulation is stopped when a given level of confidence is reached for answering the model checking problem. The VeStA tool [START_REF] Sen | VeStA: A statistical model-checker and analyzer for probabilistic systems[END_REF] supports statistical model checking and quantitative analysis of executable specifications in which all nondeterminism is quantified probabilistically. In VeStA, system properties are given in PCTL (or its continuous-time extension CSL), while quantitative analysis queries are given in the QuaTEx logic [START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF] and ask for the average values of quantities associated with the model-VeStA simulates the model and provides estimates for these averages.

A Language for Specifying Memoryless Adversaries

The source of nondeterminism in a probabilistic rewrite theory is picking an R/A-match from a set of possible ones in each state. This section introduces a probabilistic strategy language that can be used to quantify this nondeterminism, i.e., for specifying memoryless adversaries of PRTs.

The probability distribution associated with picking a certain R/A-match ([C] A , r, [θ] A ) can be specified using the individual (conditional) distributions for picking the rule r, the context [C] A , and the substitution [θ] A , which is more convenient than specifying their joint distribution. That is, by probability theory, any memoryless adversary {σ

[u] A } [u] A of a PRT R π can be decomposed as: σ [u] A ([C] A , r, [θ] A ) = P {pick rule r | state is [u] A } • P {pick context [C] A | state is [u] A , rule is r} • P {pick substitution [θ] A | state is [u] A , rule is r, context is [C] A }
We denote the factors in this product by

A [u] A (r), A r [u] A ([C] A ), and A r,[C] A [u] A ([θ] A )
, respectively. They give the probabilities of picking rule r in state [u] A , of using context [C] A to match [u] A with the lefthand side of r, and of using substitution

[θ] A to match [u] A with the lefthand side of r in context [C] A , respectively. We call {A [u] A : enabled([u] A ) → [0, 1]} [u] A , {A r [u] A : C([u] A , r) → [0, 1]} [u] A ,r , and {A r,[C] A [u] A ([θ] A ) : S([u] A , r, [C] A ) → [0, 1]} [u] A ,r,[C] A ,
resp., the underlying rule, context, and substitution adversaries of the memoryless adversary {σ

[u] A } [u] A .
It is cumbersome to define absolute probabilities for each choice (so that they add up to 1 in each state). If we have rules r 1 , r 2 , and r 3 , and want r 1 to be applied with 3 times as high probability as r 2 (when both are enabled), which should be twice as likely as taking rule r 3 , then, for a state [u] A where all rules are enabled, the probabilities would be {r 1 → 6/9, r 2 → 2/9, r 3 → 1/9}, and for a state [u ] A where r 2 is not enabled, the distribution would be {r 1 → 6/7, r 3 → 1/7}, etc. This can soon become inconvenient. In our language one therefore instead defines relative weights for each rule, context, and substitution. That is, for any state [u] A in our example, the "weights" of the rules r 1 , r 2 and r 3 could be 6, 2, and 1, respectively. Relative weights are therefore needed since the set of possible R/A-matches in a state, whose nondeterministic choice we want to quantify, is only available during the model execution. We therefore build the concrete probability distributions on-the-fly in each state during execution, which we sample to obtain the next state.

Language. The language we propose allows specifying memoryless rule, context, and substitution adversaries, using strategy expressions of the following forms: We refer to [START_REF] Bentea | A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing[END_REF] for the detailed syntax and semantics of our language, i.e., how each strategy expression defines an adversary. Our implementation also provides an executable rewriting logic semantics of our language.

PSMaude. Our tool PSMaude [START_REF] Bentea | The PSMaude tool home page[END_REF] extends Maude by adding support for specifying probabilistic rules with fixed-size probability distributions and our strategy language, a probabilistic rewrite command and a statistical PCTL model checker that can analyze a given PRT controlled by given probabilistic strategies. Given a probabilistic module SYSTEM-SPEC that specifies a PRT, probabilistic strategies can be written in modules of the form:

(psmod PSTRAT is protecting SYSTEM-SPEC .
---import system specification state StateSort .

---sort for system states psdrule A strategy definition, introduced with psd, associates strategies for rules, contexts, and substitutions with a strategy identifier StratID, that can be used in a probabilistic strategy rewrite command (prew [n] s using StratID .), which executes n one-step (probabilistic) rewrites from the state s using the strategy StratID. The unbounded version (uprew s using StratID .) rewrites until a deadlock occurs. The strategies for rules, contexts, and substitutions are introduced with psdrule, psdcontext, and psdsubst, respectively; they can be conditional, with keywords cpsdrule, cpsdcontext, and cpsdsubst, respectively. There may be several definitions for the same strategy identifier, but they should refer to disjoint cases of the arguments.

[owise]-annotated strategy expressions can be used to specify how the nondeterminism is resolved when no other strategy definition is applicable. It can thus be easily ensured that a probabilistic strategy resolves all nondeterminism in a given system specification.

Our statistical model checking command (smc s |= ϕ using StratID .) allows for further analysis of a specification with given strategies, where ϕ is a PCTL formula, and satisfaction of atomic propositions is defined in a state predicate module:

(spmod SYSTEM-PRED is protecting SYSTEM-SPEC . ---import system specification smcstate StateSort .

---sort for system states psp ϕ 1 . . . ϕn : Sort1 ... SortK .

---parametric state predicates var S :

StateSort . csat S |= ϕ 1 (s 1 , . . ., s K ) if f (S, (s 1 , . . ., s K )) . ---define their semantics ... endspm)
For instance, the parametric state predicate ϕ 1 (s 1 , . . . , s K ) holds in a state S if and only if the condition f (S, s 1 , . . . , s K ) in the above csat declaration is true, where the operator f is defined by means of (possibly conditional) equations.

The command (set type1 error b1 .) sets the bound on type I errors (the algorithm returns "false" when the property holds), and (set type2 error b2 .) sets the bound on type II errors (vice versa). By lowering these bounds, a higher confidence on the model checking result is achieved, but more execution samples are generated.

Example. In each step in a probabilistic version of the blackboard game [START_REF] Martí-Oliet | Towards a strategy language for Maude[END_REF], in which some numbers are on a blackboard, two arbitrary numbers x and y are replaced by (x 2 + y) quo 2 with probability 3/4, and by (x 3 + y) quo 2 with probability 1/4, where quo denotes integer division. The goal of the game is to obtain the highest possible number at the end. This game is formalized in the following probabilistic module, that also defines an initial state: Since the multiset union __ is associative and commutative (declared with the keywords assoc and comm), the choice of the numbers x and y from the blackboard is nondeterministic. The choice of the substitution, { M → x, N → y } or { M → y, N → x }, is then also nondeterministic. We define the following probabilistic strategy BlackboardStrat to quantify this nondeterminism: The rule strategy RuleStrat assigns weight 1 to the only rule play. The context strategy CtxStrat, selecting in which context the rule play applies, assigns for each pair of numbers x and y on the blackboard, the relative weight 1/(x • y) to the context that implies that the numbers x and y are replaced by the rule play; i.e., it gives a higher weight to contexts corresponding to picking small numbers to replace. The substitution strategy SubStrat selects the rule match {M → x, N → y} with 9 times as high probability as {M → y, N → x} when x ≤ y.

We now explain the strategy BlackboardStrat in more detail. For a state [u] ACU = [2 3 5 7 11 13 17] ACU , CtxStrat assigns weights to each valid context as follows, where ACU refers to the structural axioms for multiset union (Associativity, Commutativity, and Unit (identity)). It first matches the state [u] ACU with the state pattern X Y B (where B can be empty), which gives several matches θ 1 , . . . , θ N . Then all valid contexts are generated, which in this example have the form [ t] ACU , with identifying the fragment of [u] ACU that matches the lefthand side of rule play, and t is the rest of the state. Next, the weight of each valid context is computed. Each context [ t] ACU is unified with the context pattern [] B, giving a unique match {B → t}. Of all the matches θ 1 , . . . , θ N obtained above, only those with B → t are kept. The weight associated to [ t] ACU is then computed by instantiating the weight pattern 1 / (X * Y) with either one of these last substitutions. (For well-definedness, θ i (1 / (X * Y)) and θ j (1 / (X * Y)) should be the same, for all θ i and θ j with θ i (B) = θ j (B).) For example, for the context [C] ACU = [ 3 7 11 [START_REF] Eckhardt | Stable availability under denial of service attacks through formal patterns[END_REF] The substitution strategy SubStrat solves the same matching and unification problems as above, but further refines the set of matches to those that satisfy the condition X <= Y. For the context [C] ACU above the only such match is θ 1 . The weight distribution pattern associated with SubStrat is then instantiated by θ 1 to obtain a concrete weight distribution over the matches of the lefthand side of rule play: {M → 2, N → 5} → 9 ; {M → 5, N → 2} → 1. By normalizing the associated weights, a probability distribution is obtained, from which a match is picked, e.g., η = {M → 2, N → 5} with probability 9/10.

Finally, a match for the probabilistic variable K of rule play is sampled from the distribution π r ([η] ACU ).

We run two simulations using unbounded probabilistic rewriting to show possible final states under the above strategy (the outputs are shown as comments):

(uprew initState using BlackboardStrat .) ---276 (uprew initState using BlackboardStrat .) ---4457

We then define a state predicate sumGreaterThan(i), which is true in a state S if the sum of all numbers in S is larger than i: We first set a bound of 0.01 on both error probabilities, and then check that the sum on the blackboard never exceeds 10000 with high probability. This returns a positive result, and the estimated probability for the property to hold: In this section we use cloud computing to illustrate the usefulness of defining different adversaries for the same rewrite theory. The "base" rewrite theory defines all possible behaviors of the cloud and its environment, and each probabilistic strategy corresponds to a particular load balancing policy (and assumptions about the environment). We prove the safety of the "base" model, and use simulation and statistical model checking to analyze the QoS of different load balancing policies.

Cloud Computing Scenario. We model a cloud computing system that delivers services to service users and service providers. A service provider runs web applications on one or more virtual machines (VMs) hosted on physical servers in the cloud. Service users then use these applications via the cloud service. An example of a user is a person who uses an email application of a provider via a cloud infrastructure.

Servers are grouped into data centers, which are grouped into geographical regions. Since running applications in regions closer to the users may prove beneficial, we have included a region selection filter in our cloud architecture in Fig. 1. A load balancer distributes traffic across the data centers in a region. When a user sends an application request, the cloud service forwards it to one of the VMs of the provider that owns the application. When a provider sends a request to launch a VM in a region, the cloud service forwards it to the region's load balancer, which chooses a server to host the new VM. Providers may launch a limited number of VMs, and users have a limited number of requests that the cloud can process simultaneously.

Formalization. We model the cloud system as a hierarchical object-oriented system. Service users, providers, and cloud services are declared as follows: where status and subscr contain status and subscription information data about users and providers, of the forms: noReq(u, k): the number of unresolved requests of user u is k; noVM(p, l): the number of VMs of provider p is l; maxReq(u, k): the maximum number of requests that the cloud service may simultaneously process for user u is k; maxVM(p, l): the maximum number of VMs that provider p can run is l. A region has a location, and a dataCenters attribute with the data center objects in that region. The pservers attribute of a data center object denotes the set of physical server objects in the data center: with owner the ID of the provider that owns the VM; vmReq the object IDs of all users whose requests are running on the VM; vmMaxReq the maximum number of requests that can be resolved on the VM simultaneously; and running says whether the VM is running. We model two types of messages: i) user requests req(u,p) from user u to the application of provider p; ii) provider requests launch(p,r) from provider p to the cloud service, to launch a new VM in region r.

The following rule models how the cloud service handles a service request from user O to the web application of provider O' when O does not exceed her limit (A < B). This request can be forwarded to any VM in the system (since dataCenter, pservers, and vms denote sets of objects). The user's status is updated and the selected VM updates its vmReq attribute by adding the user's object ID O to the set

(O OIDSET) > VM) > PS) > DC) > if A < B /\ size(OIDSET) < D .
The next rule models how the cloud service handles launch requests from a provider O for a new VM in a region R by launching a VM on any server in R.

> VM) > PS) > DC) > if A < B /\ M < N .
Model Checking Safety Properties. To ensure the "safety" of our system we use Maude's search command to verify that the cloud is never processing more requests from a user than allowed. For the search to terminate, we use an initial state with two users that can generate 6 and 7 requests. The following Maude command searches for a "bad" state where some user O' has more requests running (M) than allowed (N): Load Balancing Policies as Probabilistic Strategies. The above model describes all possible treatments of user and provider requests. For better system performance, one could think of different load balancing policies, so that, e.g., users may get with high probability a VM closer to their location, or get VMs on servers with the least workload, etc. Likewise, a provider might want VMs uniformly across the regions, or in regions with least workload, etc. Within a region, better-paying providers could be assigned VMs with high probability on stable servers, or on servers with small workload. These policies are specified by different strategies on top of our verified model.

We have defined three strategies: i) a strategy that does not take locations or geographical regions into account, i.e., the region to which a user request is forwarded is chosen uniformly at random; ii) a strategy that forwards high priority user requests to the region closest to the user with high probability, and furthermore, treats requests from high priority providers with high probability; and iii) a strategy that forwards high priority user requests to a region with small VM load with high probability, and processes requests from high priority providers with high probability. For each of these policies, we define two "subcases": a) distribute requests uniformly within the region, and b) with high probability, distribute requests to VMs/physical servers with small workload for the high-priority providers/users.

We first quantify the nondeterministic choices related to general/environment assumptions about the cloud system, using the following rule strategy: Our load balancing policies are specified by different context strategies for rules processUserReq and processProviderReq. They resolve the nondeterministic choice of which request to process next, and on which VM/server the request is resolved. We only specify the policy ii(b), and refer to [START_REF] Bentea | A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing[END_REF] for the definitions of the other policies. The rule processUserReq selects any user request req(u, p), and assigns any VM to handle the request, in any region. For policy ii(b), the context strategy for rule processUserReq models that user requests with high priorities P are selected with probability proportional to P 2 , that the probability of selecting region R is inversely proportional to the distance distance(LOC, LOC') between the user and R, and that requests are sent to the VMs/servers with small load size(OIDSET) with high probability: The context strategy for rule processProviderReq models that requests from providers with high priorities P are selected with high probability proportional to P 2 , and resolved by allocating VMs on servers with small load M with high probability: The resulting probabilistic strategy is denoted Strat2b.

Simulation. We simulate our system using the strategies Strat2b and Strat3b (specifying policies ii(b) and iii(b) above). To analyze the QoS from a user U 's perspective, we define a QoS measure of a request R as a function of the relative workload of the server S handling the request, and the distance between the user and S:

cost(U, R, S) = k • #tasksRunning(S) capacity(S) + q • distance(U, R)
The total user QoS is the sum of all such single QoS measures in the system. We simulate the cloud system using Strat2b and Strat3b, from an initial state with 2 regions, 4 users, and 2 providers in different locations and with different priorities. Users can generate 3, 5, 8, and 3 requests, respectively, whereas providers can generate 20 requests. Fig. 2 shows the total cumulative cost over 200 probabilistic rewrite steps (the horizontal axis), for the two strategies (using the same random seed). The smaller values correspond to Strat2b, which suggests that Strat2b is a better policy in terms of the total user QoS. We next use statistical model checking to show that, with high confidence, this is the case. Statistical Model Checking. We use the same initial state as for the simulation, and define a parametric state predicate effortGreaterThan as follows: such that effortGreaterThan(N ) is true if the cumulative cost of the cloud exceeds N in the current state. We verify that, with confidence 0.9, under the strategy Strat2b, the effort always stays below 13000 with high probability:

(

Related Work

A number of tools support models that are both probabilistic and nondeterministic, including Markov automata [START_REF] Eisentraut | On probabilistic automata in continuous time[END_REF], generalized stochastic Petri nets [START_REF] Marsan | Modelling with generalized stochastic Petri nets[END_REF], or uniform labeled transition systems [START_REF] Bernardo | Uniform labeled transition systems for nondeterministic, probabilistic, and stochastic processes[END_REF].

In probabilistic automaton-based models one can use synchronous parallel composition to quantify nondeterministic choices by composing the system with a new "scheduler" component. For example, if the model allows us to nondeterministically select action a or action b, we can quantify this nondeterminism by composing the model with a "scheduler" automaton with transitions

{s 0 τ [1/3] ----→ do-a, s 0 τ [2/3] ----→ do-b, do-a a -→ s 0 , do-b b - → s 0 }; the composed
system will then do action a with probability 1/3 and action b with probability 2/3. Such "scheduler" components are supported by tools like Modest [START_REF] Bohnenkamp | MODEST: A compositional modeling formalism for hard and softly timed systems[END_REF] and PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF]. Our approach contrasts with this one by: (i) having a more explicit separation between model and strategy, since in the above approach the strategy is just another "system" component; (ii) supporting a more expressive underlying specification language with unbounded data types, dynamic object/message creation and deletion, and arbitrary complex data types; and (iii) providing a more expressive and convenient way of specifying the strategies themselves. It is also unclear to what extent automaton-based approaches can support hierarchical systems.

In Uppaal-SMC [START_REF] David | Time for statistical model checking of real-time systems[END_REF] the nondeterminism concerning which component should be executed next is implicitly resolved by assigning a stochastic delay to each component; the one with the shortest remaining delay is then scheduled for execution. If multiple transitions are enabled for a component, then one is chosen uniformly at random. In contrast, our language allows the user to specify the probability distributions that quantify the nondeterminism in the model.

Maude itself has a non-probabilistic strategy language [START_REF] Eker | Deduction, strategies, and rewriting[END_REF] to guide the execution of non-probabilistic rewrite theories; i.e., there is no support for quantifying the nondeterminism either in the model or in the strategy. VeStA [START_REF] Sen | VeStA: A statistical model-checker and analyzer for probabilistic systems[END_REF] can analyze fully probabilistic actor PMaude specifications. For flat objectoriented systems nondeterminism is typically removed by letting each action be triggered by a message, and letting probabilistic rules add a stochastic delay to each message [START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF][START_REF] Alturki | Probabilistic modeling and analysis of DoS protection for the ASV protocol[END_REF]. The probability of two messages being scheduled at the same "time" is then zero, and this therefore resolves nondeterminism. This method was recently extended to hierarchical object-oriented systems [START_REF] Eckhardt | Stable availability under denial of service attacks through formal patterns[END_REF][START_REF] Bruni | Modelling and analyzing adaptive self-assembly strategies with Maude[END_REF]. The differences with our work are: (i) whereas we have a clear separation between system model and adversary, the above approach encodes the adversary in the model, and hence clutters it with fictitious clocks and schedulers to obtain a fully probabilistic model; (ii) our implementation supports not only a subset of object-oriented specifications, but the entire class of PRTs with fixed-size probability distributions; and (iii) we add a simulator and statistical model checker to Maude instead of using an external tool.

ELAN [START_REF] Borovanský | An overview of ELAN[END_REF] is a rewriting language where strategies are first class citizens that can appear in rewrite rules, so there is no separation between system model and strategies. The paper [START_REF] Bournez | Probabilistic rewrite strategies. Applications to ELAN[END_REF] adds a "probabilistic choice" operator PC(s 1 : p 1 , . . . , s n : p n ) to ELAN's strategy language, where p i defines the probability of applying strategy s i . This approach is different from ours in the following ways: there is no separation between "system" and "strategy;" the definition of context and substitution adversaries is not supported and therefore not all nondeterminism in a system can be quantified; and there is no support for probabilistic model checking analysis.

Concluding Remarks

In this paper we define what is, to the best of our knowledge, the first language for defining complex probabilistic strategies to quantify the nondeterminism in infinite-state systems with both probabilities and nondeterminism, and that includes the object-oriented systems with dynamic object creation. We propose a modular safety/QoS analysis methodology in which a simple (typically nonprobabilistic) "base" model that defines all possible system behaviors can be easily verified for safety, and where different probabilistic refinements can be specified on top of the verified base model. QoS properties of the refinements can then be analyzed by statistical and exact probabilistic model checking.

We have implemented a probabilistic simulator and statistical PCTL model checker for our strategies for all probabilistic rewrite theories with discrete probability distributions. We show the usefulness of our language and methodology on a cloud computing example, where different probabilistic strategies on top of the verified base model define different load balancing policies for the cloud, and show how our tool PSMaude can be used to compare the QoS provided by dif-ferent policies. This example indicates that we need to integrate timed modeling and analysis into our framework.

We also plan to extend PSMaude to allow the statistical analysis of quantitative temporal expressions specified in the QuaTEx logic [START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF]. This would allow, e.g., the statistical estimation of expected values of particular numerical quantities associated with a probabilistic rewrite theory whose nondeterminism is quantified by a given probabilistic strategy. Another direction for future work is to investigate algorithms for the exact (vs. statistical) probabilistic model checking of probabilistic rewrite theories for which some, but not necessarily all nondeterminism is quantified by a "partial" probabilistic strategy. Finally, since our proposed probabilistic strategy language only allows defining memoryless adversaries, we also aim to extend its syntax and semantics to allow defining history-dependent adversaries.

  rl [l]: m(O, w) < O : C | a1 : x, a2 : O', a3 : z > => < O : C | a1 : x + w, a2 : O', a3 : z > m'(O', x) .

  RuleStratID := RuleStratExpr . ---rule strategy psdcontext ContextStratID := ContextStratExpr . ---context strategy psdsubst SubstStratID := SubstStratExpr . ---substitution strategy psd StratID := < RuleStratID | ContextStratID | SubstStratID > . ---strategy endpsm)

(

  pmod BLACKBOARD is protecting RAT . sort Blackboard . subsort Nat < Blackboard . op empty : -> Blackboard [ctor] . op __ : Blackboard Blackboard -> Blackboard [ctor assoc comm id: empty] . vars M N K : Nat . prl [play] : M N => (K + N) quo 2 with probability K := (M * M -> 3/4 ; M * M * M -> 1/4) . op initState : -> Blackboard . eq initState = 2 3 5 7 11 13 17 . endpm)

(

  psmod BLACKBOARD-PROB-STRAT is protecting BLACKBOARD . state Blackboard . var B : Blackboard . vars X Y : Nat . psdrule RuleStrat := given state: B is: (play) -> 1 . psdcontext CtxStrat := given state: X Y B rule: play is: ([] B) -> (1 / (X * Y)) . psdsubst SubStrat := given state: X Y B rule: play context: [] B is: {M <-X, N <-Y} -> 9 ; {M <-Y, N <-X} -> 1 if X <= Y . psd BlackboardStrat := < RuleStrat | CtxStrat | SubStrat > . endpsm)

17 ]

 17 ACU two such matches θ k with θ k (B) = 3 7 11 13 17 exist: θ 1 = {X → 2, Y → 5, B → 3 7 11 13 17} and θ 2 = {X → 5, Y → 2, B → 3 7 11 13 17}. The weight of the context [C] ACU is then computed as θ 1 (1 / (X * Y)) = 1 / 10. Similarly, the weight of the context [ 2 5 7 11 17] ACU is 1/(3 • 13) = 1/39. After computing the weights of all contexts, they are normalized to obtain a distribution, from which a context is picked.

(

  spmod BLACKBOARD-PRED is protecting BLACKBOARD . protecting NAT . smcstate Blackboard . psp sumGreaterThan : Nat . ---declare a parametric state predicate var B : Blackboard . var N : Nat . csat B |= sumGreaterThan(N) if sum(B) > N . ---define its semantics op sum : Blackboard -> Nat . eq sum(empty) = 0 . eq sum(N B) = N + sum(B) . endspm)

(

  set type1 error 0.01 .) (set type2 error 0.01 .) (smc initState |= P>= 0.9 [G ~sumGreaterThan(10000)] using BlackboardStrat .) Result Bool: true Number of samples used: 11176 Confidence: 99% Estimated probability: 79/87

Fig. 1 .

 1 Fig. 1. A cloud computing architecture.

class

  Region | location : Location, dataCenters : Configuration . class DCenter | pservers : Configuration . class PServer | load : Nat, maxLoad : Nat, nextVMID : Nat, vms : Configuration . with load the number of VMs on the server; maxLoad the server's capacity; nextVMID for generating fresh IDs for new VMs; and vms a set of VM objects of the class: class VMachine | owner : Oid, vmReq : OidMSet, vmMaxReq : Nat, running : Bool .

OIDSET 4 :

 4 crl [processUserReq]: req(O, O') < CSO : CService | status : (noReq(O, A), AS1) , subscr : (maxReq(O, B), AS2) > < R : Region | dataCenters : (< DCO : DCenter | pservers : (< PSO : PServer | vms : (< VMO : VMachine | owner : O', running : true, vmReq : OIDSET , vmMaxReq : D > VM) > PS) > DC) > => < CSO : CService | status : (noReq(O, A + 1), AS1) > < R : Region | dataCenters : (< DCO : DCenter | pservers : (< PSO : PServer | vms : (< VMO : VMachine | vmReq :

  crl [processProviderReq]: launch(O, R) < CSO : CService | status : (noVM(O, A), AS1) , subscr : (maxVM(O, B), AS2) > < R : Region | dataCenters : (< DCO : DCenter | pservers : (< PSO : PServer | load : M , maxLoad : N, nextVMID : NEXTID , vms : VM > PS) > DC) > => < CSO : CService | (status : (noVM(O, (A + 1)), AS1) ) > < R : Region | dataCenters : (< DCO : DCenter | pservers : (< PSO : PServer | load : (M + 1) , nextVMID : (NEXTID + 1), vms : (< vm(PSO, NEXTID) : VMachine | owner : O, running : true, vmReq : noid, vmMaxReq : MAXREQ

(

  search [1] : initState =>* CONFIG < CSO : CService | status : (noReq(O, M), AS1), subscr : (maxReq(O, N), AS2) > such that M > N .) rewrites: 11312174 in 279134ms cpu (283262ms real) (40525 rewrites/second) No solution.

psdcontext

  CtxStrat2b := given state: CF req(O , O') < O : SUser | location : LOC , priority : P > < CSO : CService | ATTRSET > < R : Region | location : LOC' , dataCenters : (< DCO : DCenter | pservers : (< PSO : PServer | ATTRSET', vms : (< VMO : VMachine | vmReq : OIDSET , ATTRSET'' > VM) > PS) > DC) > rule: processUserReq is: (CF < O : SUser | location : LOC , priority : P > []) -> ((P * P ) / ((1 + size(OIDSET )) * (1 + distance(LOC , LOC' )))) .

psdcontext

  CtxStrat2b := given state: CF < CSO : CService | ATTRSET > launch(O , R) < O : SProvider | priority : P > < R : Region | location : LOC', dataCenters : (< DCO : DCenter | pservers : (< PSO : PServer | load : M , ATTRSET > PS) > DC) > rule: processProviderReq is: (CF < O : SProvider | priority : P > []) -> ((P * P ) / (1 + M )) .

(

  prew [200] initState using Strat2b .) (prew [200] initState using Strat3b .)

Fig. 2 .

 2 Fig. 2. Comparison of the total cloud cost with each rewrite step, for the two policies.

  psp effortGreaterThan : Nat . var CF : Configuration . var N : Nat . csat CF |= effortGreaterThan(N) if costCloud(CF) > N .

  ContextWeightDist and SubstWeightDist have similar forms. Condition (abbreviated to Cond in the context adversary syntax above) specifies the condition under which the strategy can be applied, and [owise] specifies that it should be applied if no other strategy can be applied.

psdrule Identifier := given state: StatePattern is: RuleWeightDist [if Condition ] [[owise]] psdcontext Identifier := given state: StatePattern rule: RulePattern is: ContextWeightDist [if Cond ] [[owise]] psdsubst Identifier := given state: StatePattern rule: RulePattern context: ContextPattern is: SubstWeightDist [if Condition ] [[owise]]

with StatePattern a term t( x), RulePattern a rule label or a variable over rule labels, and ContextPattern a term c( y) with ∈ y and y\{ } ⊆ x, or a variable over contexts. The weight expression RuleWeightDist is either uniform, or a list of ";"-separated weight assignments of the form RuleLabel → Weight , where Weight is a term w( x) of sort Rat;

This is a slightly modified version of the definition of adversaries in[START_REF] Kumar | Probabilistic rewrite theories: Unifying models, logics and tools[END_REF][START_REF] Agha | PMaude: Rewrite-based specification language for probabilistic object systems[END_REF].

We do not show the declaration of variables, but follow the Maude convention that variables are in capital letters.

Acknowledgments. We thank José Meseguer and Roy Campbell for discussions on probabilistic strategies, and gratefully acknowledge partial support for this work by AFOSR Grant FA8750-11-2-0084. We also thank the anonymous reviewers for very useful comments on a previous version of the paper.


Jonas Eckhardt

Tobias Mühlbauer

José Meseguer

Martin Wirsing

Statistical Model Checking for Composite Actor Systems

Keywords: actor system, rewriting logic, Maude, composite actor, statistical model checking

In this paper we propose the so-called composite actor model for specifying composed entities such as the Internet. This model extends the actor model of concurrent computation so that it follows the "Reflective Russian Dolls" pattern and supports an arbitrary hierarchical composition of entities. To enable statistical model checking we introduce a new scheduling approach for composite actor models which guarantees the absence of unquantified nondeterminism. The underlying executable specification formalism we use is the rewriting logic-based semantic framework Maude, its probabilistic extension PMaude, and the statistical model checker PVeStA. We formalize a model transformation which-given certain formal requirements-generates a scheduled specification. We prove the correctness of the scheduling approach and the soundness of the transformation by introducing the notions of strong zero-time rule confluence and time-passing bisimulation and by showing that the transformation is a time-passing bisimulation for strongly zero-time rule confluent composite actor specifications.

Introduction

The actor model is a classical model for concurrent computation [START_REF] Hewitt | A universal modular actor formalism for artificial intelligence[END_REF] which witnessed revived interest with the advent of multi-core programming and Cloudscale computing. Several modern programming languages such as Erlang and Scala base their concurrency models on actors [START_REF] Armstrong | Concurrent Programming in Erlang[END_REF][START_REF] Haller | Actors in Scala[END_REF]. An actor is a concurrent object which operates asynchronously and interacts with other actors by sending asynchronous messages [START_REF] Agha | Concurrent programming using actors[END_REF]. Temporal logic properties of actor-based models can be automatically verified either by exact model checking algorithms [START_REF] Eker | The Maude LTL model checker[END_REF] or, in an approximate but more scalable way, by statistical model checking (see e.g., [START_REF] Agha | PMaude: Rewrite-based Specification Language for Probabilistic Object Systems[END_REF]).

These approaches are all based on the original "flat" actor model but many interesting applications such as the Internet and Cloud systems are not flat, as they are composed of various participants and systems and are hierarchically structured into different layers and networks. Such composed entities are often safety-and security-critical, and have strong qualitative and quantitative formal requirements. The above mentioned analysis approaches, however, rely on flat actor models and cannot handle and model check composite models in a direct way.

In this paper, we extend the actor model to a so-called composite actor model that directly addresses hierarchical concurrent systems and present a model transformation which makes statistical model checking usable for composite actor model specifications. The composite actor model follows the so-called "Reflective Russian Dolls" model [START_REF] Meseguer | Semantic Models for Distributed Object Reflection[END_REF] and supports an arbitrary hierarchical composition of entities. As underlying executable specification formalism we use the rewriting logic language Maude and its real-time and probabilistic extensions.

Current statistical model checking methods require that the system is purely probabilistic, i.e., that there is no unquantified nondeterminism in the choice of transitions. This is nontrivial to achieve for distributed systems where many different components may perform local transitions concurrently. There are two complementary ways for guaranteeing the absence of nondeterminism: either by associating continuous probability distributions with message delays and computation time and by relying on the fact, that for continuous distributions the probability of sampling the same real number twice is zero (see e.g., [START_REF] Eker | The Maude LTL model checker[END_REF]), or by introducing a scheduler that provides a deterministic ordering of messages (see e.g., [START_REF] Alturki | Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol[END_REF]). We follow the latter approach and propose a new scheduling method for well-formed composite actor models that guarantees the absence of nondeterminism. We formalize the approach in Maude and study its soundness by proving the correctness of the scheduling approach, termination and confluence of the underlying equational specification, and by showing the absence of unquantified nondeterminism from any scheduled well-formed composite actor specification. We further formalize a model transformation which-given a composite actor specification that adheres to certain formal requirements-generates a scheduled specification. To prove the soundness of the transformation we introduce the notions of strong zero-time rule confluence and time-passing bisimulation and then show that the transformation, which is only a simulation by itself, is indeed a time-passing bisimulation for strongly zero-time rule confluent composite actor specifications. To the best of our knowledge, our solution is the first one making it possible to analyze such systems in a faithful way by statistical model checking. We have applied our method to several complex case studies (see [START_REF] Eckhardt | Stable Availability under Denial of Service Attacks through Formal Patterns[END_REF][START_REF] Wirsing | Design and Analysis of Cloud-Based Architectures with KLAIM and Maude[END_REF][START_REF] Eckhardt | A Formal Analysis of Security Properties in Cloud Computing[END_REF][START_REF] Mühlbauer | Formal Specification and Analysis of Cloud Computing Management[END_REF]); for reasons of space we only illustrate a simple example.

Outline. The paper is structured as follows: In Sect. 2 we explicate shortly the (flat) actor model and the "Reflective Russian Dolls" model, and show how to build the composite actor model in Maude by applying the Russian Dolls approach to the flat actor model. In Sect. 3 we present our model transformation together with the scheduling approach, their formalization in Maude and prove the soundness properties. Sect. 4 then gives a short presentation of our methodology for the statistical model checking analysis of actor model-based specifications. We conclude by discussing related work, summarizing our results, and sketching further work.

The Composite Actor Model

The Actor Model of Computation

Our specifications are based on the actor model of computation [START_REF] Hewitt | A universal modular actor formalism for artificial intelligence[END_REF][START_REF] Hewitt | Laws for communicating parallel processes[END_REF][START_REF] Agha | Actors: a model of concurrent computation in distributed systems[END_REF], a mathematical model of concurrent computation in distributed systems. Similar to the object-oriented programming paradigm, in which the philosophy that everything is an object is adopted, the actor model follows the paradigm that everything is an actor. An actor is a concurrent object that encapsulates a state and can be addressed using a unique name. Actors communicate with each other using asynchronous messages. Upon receiving a message, an actor can change its state and can send messages to other actors. Actors can be used to model and reason about distributed and concurrent systems in a natural way [START_REF] Agha | Actors: a model of concurrent computation in distributed systems[END_REF].

The Reflective Russian Dolls Model

In rare situations, the state of a distributed system can be thought of as a flat configuration which contains objects and messages. Such a flat configuration can be modelled as a flat soup (i.e., a multiset) that consists of actors and messages. However, as a distributed system becomes more complex, hierarchies are introduced to better represent the structure of the system and its communication patterns. A flat model does not reflect boundaries in a hierarchical system which impose conditional communication barriers. In a flat model, every participant can communicate with everybody else. However, some concepts, like a firewall, rely on the existence of physical boundaries that messages from the outside have to cross in order to reach destinations within that boundary.

In [START_REF] Meseguer | Semantic Models for Distributed Object Reflection[END_REF], Meseguer and Talcott present the Reflective Russian Dolls (RRD) model which extends and formalizes previous work on actor reflection and provides a generic formal model of distributed object reflection. The rewriting logicbased model combines logical reflection and hierarchical structuring. In their model, the state of a distributed system is not represented by a flat soup, but rather as a soup of soups, each enclosed within specific boundaries. As with traditional Russian dolls, soups can be nested up to an arbitrary depth.

Figure 1 illustrates the basic idea using a system that is guarded by a firewall. Each of the boxes represents a system. The firewall consists of a subsystem which itself is composed of several components C 1 . . . C n . Message M is addressed to the innermost component C n and as such has to pass the boundary of the firewall. The firewall possibly transforms the message to M (e.g., tags a message with a security clearance). After that, the boundary of the sub-system has to be crossed which, respectively, can also alter the message to M .

Mathematically, this can be modelled by boundary operators of the form

b : s 1 , . . . , s n , Conf iguration → Conf iguration
where s 1 , . . . , s n are additional sorts. These sorts are called the parameters of the boundary operator. Boundary operators encapsulate a configuration together with several parameters, and as with Russian dolls, they can be nested arbitrarily. Using the Russian Dolls model, sophisticated distributed systems, that rely on system boundaries, can be modeled [START_REF] Meseguer | Semantic Models for Distributed Object Reflection[END_REF].

The Composite Actor Model

We extend the original actor model of computation for flat configurations with the RRD model to allow the specification of hierarchically structured composite actor systems. Actors are now allowed to contain a soup, that is a multiset, of actors and messages in their state where each of the actors in the sub-configuration can again contain another soup of actors and messages, and so on. Referring to the aforementioned firewall example, the firewall actor can be represented by the term Thereby the firewall actor has address 0 and contains a sub-configuration in its state denoted by the config attribute. In this sub-configuration there is a subsystem actor with address 0.0 which again contains a sub-configuration which consists of the components (Ci) with adresses 0.0.0, . . . ,0.0.N-1.

The naming of actors follows an hierarchical naming scheme. This naming scheme is comparable to Internet domain names, which are structured in toplevel (e.g., "de"), second-(e.g., "google") and third-level (e.g., "www") domain names. The hierarchical naming scheme for the actor model basically builds a hierarchical name tree, in which children addresses are composed of their parents address and an appended number which uniquely identifies them among their siblings (e.g., a name could be 4.0.8.2). Further information on the naming scheme can be found in [START_REF] Eckhardt | A Formal Analysis of Security Properties in Cloud Computing[END_REF][START_REF] Mühlbauer | Formal Specification and Analysis of Cloud Computing Management[END_REF].

The analysis of real world systems often requires the system model to include a notion of time (e.g., as for quality of service properties in our case studies [START_REF] Alturki | Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol[END_REF][START_REF] Wirsing | Design and Analysis of Cloud-Based Architectures with KLAIM and Maude[END_REF]). Thus, we introduce activation times for messages, i.e., times at which messages are intended to be processed.

We model composite actor models as hierarchically structured soups of messages and actors. In Maude, we represent a soup as a term of sort Config. A configuration is associative and commutative and is constructed by the operators op null : -> Config and op __ : Config Config -> Config [assoc comm id: null]. The sorts for actors and messages are both subsorts of Config. Additionally, we introduce the sort Address, which represents an actor's address, and which is a subsort of Nat. Addresses can be concatenated using the constructor op _._ : Address Address -> Address [assoc]. Messages are terms of sort Msg and are created by the constructor (_,_<-_): Float Address Content -> Msg, which takes the message's "activation" time, the receiver address and the actual contents of the message as arguments. Finally, actors can be created by the constructor op <_:_|_> : Address ActorType AttributeSet -> Actor, which takes the address of the actor, the type of the actor, and an additional set of attributes (a term of sort AttributeSet, which represents an associative, commutative set of terms of sort Attribute) as arguments.

The hierarchical nature of the composite actor model is made explicit by the dedicated attribute config, which contains the inner soup of an actor. The constructor op config:_ : Config -> Attribute [gather(&)] creates this inner soup for an arbitrary term of sort Config. 1Following the idea of the actor model, actors in the composite actor model communicate only via asynchronous message passing. This convention allows the local specification of actors, i.e., the specification of an actor's semantics does not need to contain knowledge about the structure of the composed system and rewrite rules that capture the semantics do not have to include the receiving actor. As such, a specification of an actor only requires local transition rules (message handling) and boundary crossing rules to be specified. Thereby, boundary crossing rules are rules that insert a message into an actor's sub-configuration and rules that move a message from an actor's sub-configuration to the configuration the actor is in. More precisely, composite actor model specifications only contain (possibly probabilistic) rewrite rules of the following type:

C onsume: one actor consumes a message at time t and may emit timed (t1,. . .,tn) messages or spawn new actors in its sub-configuration.

< A : T | config: C, AS> (t, A<-M) => < A : T | config: C', AS'> (t1, A1<-M1) . . . (tn, An<-Mn)
B oundary-Down: one actor consumes a message at time t and inserts it into its subconfiguration. B oundary-Up: one actor consumes a message from its subconfiguration at time t and emits it at its level in the composite actor hierarchy.

< A : T | config: (t, X<-M) C, AS> => < A : T | config: C, AS'> (t', X'<-M')
A, A1,. . .,An, X, X' are thereby terms of sort Address, T of sort ActorType, C, C' of sort Config, t, t1,. . .,tn, t' of sort Float, M, M1,. . .,Mn, M' of sort Content and AS and AS' of sort AttributeSet. Any of these rules may have added probabilistic information [START_REF] Agha | PMaude: Rewrite-based Specification Language for Probabilistic Object Systems[END_REF] or be subjected to a condition.

Local specifications of actors provide modularity which is a key technique to tackle the complexity of large distributed systems. In previous work [START_REF] Eckhardt | Stable Availability under Denial of Service Attacks through Formal Patterns[END_REF] we describe how meta objects, i.e., distributed objects that mediate and control the behavior of one or more distributed objects, can be made highly reusable as formal patterns and how a distributed system can be modelled as a composition of such formal patterns.

Note that even though messages in the composite actor model are timed, the execution of composite actor model specifications in pure Maude would neither take activation times nor the concept of a global time into account. Rather all possible executions regardless of activation times would be executed.

Definition (Well-Timedness). In the following we are only interested in "welltimed" executions where messages are processed according to their activation time and global time is advancing monotonously. More precisely, we call a run u 0 r0 -→ u 1 r1 -→ . . . of a composite actor specification well-timed if for any i, the transition u i ri -→ u i+1 is triggered by the application of rule r i at time t i , and t i ≤ t i+1 where t i is the smallest activation time occurring in u i .

Scheduling Approach for Composite Actor Models

The absence of unquantified nondeterminism is a requirement for statistical model checking using Maude/PMaude and PVeStA [START_REF] Agha | PMaude: Rewrite-based Specification Language for Probabilistic Object Systems[END_REF]. Currently, there are two approaches for assuring this requirement: (i) by associating continuous probability distributions with message delays and computation time [START_REF] Agha | PMaude: Rewrite-based Specification Language for Probabilistic Object Systems[END_REF] and (ii) by introducing a scheduler which guarantees a deterministic execution order of messages in the actor system [START_REF] Alturki | Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol[END_REF]. Both approaches however rely on a flat soup of actors and cannot, in their current state, handle composite actor models. In this work we adapt the scheduling approach (ii) for composite actor models. In order to promote modularity and to make the scheduling approach transparent, we propose a model transformation approach that does not require the specification of an actor to have knowledge about the composition of the system and about the scheduling approach as such. Given a composite actor specification M -that adheres to certain formal requirements-we generate a scheduled composite actor specification SM by a model transformation M → SM such that SM guarantees the absence of unquantified nondeterminism.

Well-Formedness Requirements

To enable statistical model checking we require the following well-formedness conditions on the original composite actor specification. We call a composite actor specification M well-formed if an initial state is defined and the following two formal requirements are fulfilled: (1.) The specification must adhere to the composite actor model, i.e., entities must be specified as actors which communicate only via asynchronous message passing and there are only rewrite rules of type consume, boundary-down, or boundary-up (see Sect. 2.3). (2.) The specification must have no unquantified nondeterminism in the choice of rewrite rules, i.e., for each message there is at most one matching rewrite rule.

Moreover, we assume w.l.o.g. that (3.) any message m = (t, A<-m') is executed at its activation time t (i.e. there exists a matching rule which at time t is applied to m and the actor <A : T | C>). This is not a restriction since e.g. the loss of m can easily be modeled by the rule (t, A<-M)<A : T | C> => <A : T| C>.

If a specification M fulfills these requirements, it is still nondeterministic (e.g. if several messages occur in a configuration there may be a nondeterministic choice to which message a rewrite rule will be applied), but our scheduling approach eliminates all unquantified nondeterminism in the generated scheduled composite actor model specification SM . Note that we introduce requirement (2.) as the scheduling approach introduced by the model transformation only eliminates unquantified nondeterminism in consumption of messages, but does not in the choice of rewrite rules. Together with the scheduling approach, requirement (2.) ensures no unquantified nondeterminism in the whole specification, which is a requirement for statistical model checking with PVeStA.

Model Transformation M → SM

Given a module M that specifies a well-formed composite actor model specification, the transformation M → SM creates a module SM , for which the transformation preserves all sort declarations, all operators, and all equations. Moreover, we introduce new sorts that define an explicit scheduler and new message types to represent scheduled messages as well as two auxiliary sorts of messages where active and scheduled messages are annotated by the address of the sending actor: where terms of sort ScheduleMsg are created by the constructor [_] : Msg -> ScheduleMsg and represent messages that are emitted by rewrite rules and that are to be inserted in the scheduler. The constructors {_,_} : Address Msg -> LocActiveMsg and [_,_] : Address ScheduleMsg -> LocScheduleMsg, generate terms of sort LocActiveMsg and LocScheduleMsg respectively. Both contain either a term of sort Msg (in case of a LocActiveMsg) or ScheduleMsg (in case of a LocScheduleMsg) and a term of sort Address2 .Terms of sort ScheduleListrepresent a list of ScheduleMsg using the constructor op _;_ : ScheduleList ScheduleList -> ScheduleList [assoc id: nil]. A term of sort Scheduler is created by the constructor op {_|_} : Float ScheduleList -> Scheduler, which contains the current time and a list of messages that are to be scheduled.

For each rewrite rule r (which is either of type consume, boundary-down, or boundary-up) in M , a rewrite rule r is added to SM , where each term MSG of sort Msg on the right side of r is transformed to a term [MSG] of sort ScheduleMsg. We also add the specification of our scheduling approach to the new specification (for details see Sect. 3.3).

Moreover, any initial state st of M is transformed to a state st of SM as follows: (i) every message MSG of sort Msg is transformed to a term [MSG] of sort ScheduleMsg and (ii) an empty scheduler {0.0 | nil} is added. Then the result of the model transformation is the canonical form [st ] of st , which is of the form AC {0.0 | SL}, where AC represents the message-free actor hierarchy of st and SL is the message list in the scheduler that now contains all messages of st as scheduled messages.

The Scheduling Approach

On a high level of abstraction, in order to remove all unquantified nondeterminism, our scheduling approach takes control of when a rewrite rule is executed. Our well-formedness requirements specify that only three types of rewrite rules (consume, boundary-down, and boundary-up) are allowed; and that there is no unquantified nondeterminism in the choice of these rules. Each of these rewrite rules requires an active message, i.e., non-scheduled message, to be present either at the hierarchy level of the actor or in its sub-configuration. Thus, a rewrite can occur only if an active message is present in the composite actor hierarchy. Furthermore, since we require that one single message is consumed by exactly one actor, this rewrite can be determined up to probabilistic choices. In order to ensure that only one message at a time is emitted we introduce an operation step and, similar to the special tick rule that is defined in [START_REF] Agha | PMaude: Rewrite-based Specification Language for Probabilistic Object Systems[END_REF], define a one-step computation of a model written in the scheduled composite actor model as a transition of the form u step --→ v → w where (i) u is a canonical term, which represents the global state of a scheduled composite actor system and in which all messages are contained in the scheduler. (ii) v is a canonical term obtained by removing the next addressed scheduled message [A,[(T, A'<-M)]] from the scheduler, and by inserting it, as a nonscheduled addressed message {A,(T, A'<-M)}, into the configuration of the actor at address A. Additionally, the global time in the scheduler is advanced to T. This operation is called step. (iii) w is a canonical term obtained after zero or one rewrites the actor performs to forward (boundary-down or boundary-up) or consume the message.

More precisely, the scheduling approach for the composite actor model consists of the following steps: (1.) If no active message is present at any level of the hierarchy, the next scheduled message is marked as active and inserted in the top-most configuration by the scheduler. (2.) Then, the message is pushed down the hierarchy by equational simplification, until it eventually reaches the configuration where it has been emitted. The resulting term is in canonical form. (3.) Since the specification adheres to the composite actor model, there exists at most one rewrite rule of type consume, boundary-down, or boundary-up which consumes the message and possibly produces several scheduled messages. (4.) Finally, the scheduled messages are pulled up the hierarchy by equational simplification, until it eventually reaches the top-most level where the scheduled messages are inserted into the scheduler which stores the messages in a strict order, i.e., by the scheduled activation time and if equal by Maude's built-in term order. The resulting term is in canonical form.

In the following, we present the Maude specification of the scheduling approach which forms the final part of the model transformation M → SM . To efficiently distinguish composite actor hierarchies that contain messages in any of its sub-configurations and those that do not, we use conditional sort memberships. The sort of term ActorConfig, a subsort of Config, thereby represents a configuration which contains no messages in any of its sub-configurations. In order to be able to make this distiction, we introduce the sort InertActor, which represents a term of sort Actor, that is either flat, i.e., that does not contain any subconfiguration, or whose subconfiguration is of sort ActorConfig. This is expressed by the following (conditional) sort membership axioms: where A is a variable of sort Address, T of sort ActorType, AC of sort ActorConfig, AS of sort AttributeSet, ACT of sort Actor, and C of sort Config.

Having these (conditional) sort membership axioms, we can easily identify configurations that do not contain any active message: terms of sort ActorConfig. These are the configurations that can advance, i.e., the step operation can be called on these configurations. The step operation is defined as

op step : Config -> Config [iter] . eq step(AC {gt | [A1, [(t1 , A <-M1)]]; SL}) = {A1, (t1 , A <-M1)} AC {t1 | SL} .
where AC is a term of sort ActorConfig, gt and t1 of sort Float, A1 and A of sort Address, M1 of sort Msg, and SL of sort ScheduleList. The step equation can only be applied on a term of sort Config which consists of a term of sort ActorConfig and a term of sort Scheduler. It inserts the first message of the scheduler in the configuration and updates the time of the scheduler.

The remaining equations use the following variables: A and A' of sort Address, T of sort ActorType, SM of sort ScheduleMsg, LSM of sort LocScheduleMsg, S of sort Scheduler, SL of sort ScheduleList C of sort Config, AS of sort AttributeSet, AM of sort Msg, and finally gt, t1, and t2 of sort Float.

To put scheduled messages as active messages back into the configuration where they have been emitted, the address of the actor containing the scheduled message needs to be stored together with the scheduled message. The equations create-loc-msg1 and create-loc-msg2 create a LocScheduleMsg from a scheduled message that is either in an actor's sub-configuration or at the top-most level of the hierarchy.

Correctness of the Scheduling Approach

In this section we analyse the correctness of the scheduling approach by proving that the equational specification is terminating and confluent modulo associativity and commutativity and by showing that the introduction of the scheduler eliminates all unquantified nondeterminism. Proposition. The equational specification of the scheduling approach is terminating and confluent modulo associativity and commutativity (AC).

Proof sketch (termination). The equations that need to be discussed are the recursive ones: insert-list, pull-up, and push-down. insert-list terminates since the ScheduleList argument of the insert-list operator in the recursive call gets smaller. pull-up, for a specific scheduled message, terminates, since the distance of the message's location to the toplevel gets smaller with each level of recursion. push-down, for a specific addressed active message, terminates, since the distance between the message's address and the addresses of the actors in the sub-configuration the message is inserted into gets small with each level of recursion.

Proof sketch (confluence modulo AC). As the equational specification of the scheduling approach is terminating, it is sufficient to prove local confluence. For most equations local confluence is achieved by applying the AC property of the configurations. The only exception are the equations that insert a message into the scheduler. For the insertion equations local confluence results from the fact that the message order in the scheduler list is a total ordering. The messages are ordered by activation time and if equal by Maude's built-in term order. Lemma 1. The scheduling approach emits at most one active message at a time (after a call to the step operation).

Proof sketch. The step operator takes an ActorConfig together with a Scheduler as its argument. By construction an ActorConfig does not contain any message and all messages are in the scheduler. step emits one addressed active message into the toplevel. If the message's address is the toplevel the message is then "unwrapped", i.e., converted into an active message; otherwise it is pushed down to the level it addresses and is "unwrapped" there. As only one addressed active message is emitted, the scheduling approach emits at most one active message after a call to the step operation. Theorem 1. Let SM be a scheduled composite actor specification. If SM satisfies the requirements for the scheduling approach for scheduled composite actor models (see Sect. 3.1), then for any one-step computation u step --→ v → w of SM , there is no unquantified nondeterminism possible; however, there may be probabilistic choices in the application of an actor rewrite rule in v.

Proof sketch. We prove the theorem by reductio ad absurdum. Assume there exists unquantified nondeterminism in a one-step computation of SM . As a step operation is possible for u, the configuration in a state u has to be of sort ActorConfig, which means that it contains no active messages. As all the rewrite rules require an active message, no unquantified nondeterminism is possible in u. w is a state after a rewrite triggered by an active message. However, in a scheduled composite actor model specification all rewrite rules may only produce scheduled messages and thus no active messages. Since no active messages are present in the configuration of a state w, no rewrites are possible and thus no unquantified nondeterminism is possible in w. Thus there has to be unquantified nondeterminism in a state v. Because of the well-formedness of the original specification an actor can only react to an active message with rewrite rules that fulfill the unquantified nondeterminism requirement, there have to be at least two active messages in the configuration of a state v to get unquantified nondeterminism. Since the step operation works on terms of sort ActorConfig in which there are no active messages, this means that the scheduling approach has to emit more than one active message. Lemma 2 however states that the scheduling approach emits at most one active message after a call to the step operation. Thus there cannot be two active messages in the configuration of a state u and as a consequence, no unquantified nondeterminism is possible in u. As there is no unquantified nondeterminism possible in u, v, and w, there is no unquantified nondeterminism possible for any one-step computation u step --→ v → w of SM .

Soundness of the Model Transformation

In this section we analyse the soundness of the model transformation. In particular, we show that SM is a simulation of M for any model transformation M → SM where M is well-formed. Correctness needs the additional assumption of strong rule confluence: if M is well-formed and strongly rule confluent, then M and SM are time-passing bisimilar.

First, we introduce some definitions for (timed) probabilistic labelled transition systems and recall the notions of simulation and bisimilation [START_REF] Larsen | Bisimulation through Probabilistic Testing[END_REF].

Definition (Timed Probabilistic Labelled Transition System). A timed probabilistic (tp) labelled transition system A = (A, L, µ, l,t -→) consists of a set of states A, a family of probabilistic distributions µ : A × L → [0, 1] and a labelled transition relation l,t -→⊆ A × A where l ∈ L and t ∈ R ≥0 . We write u l,t -→ v for a transition from u to v where the label l indicates which rule r of the rewriting specification is applied to u, µ(u, l r ) is the probability, and t is the time delay, i.e., the difference of global time between u and v.

In the following, the specifications M and SM form the labelled transition systems M = (Can(M ), L M , µ M , To show the existence of a time-passing bisimulation between M and SM we need some further definitions: Definition (Delay and Zero-Time Transition). We distinguish between delay transitions a l,t -→ a with t > 0, which indicate the passing of time, and zero-time transitions a l,0 -→ a which are executed without taking any time. By A >0 = {a ∈ A| there is no a , l such that a l,0 -→ a } we denote the set of all terms to which no zero-time transition is applicable.

L M ,t ---→ M )
Figure 2 illustrates the resulting term in canonical form after one step, where the term in canonical form is depicted in solid black and in addition, the intermediate messages in gray. The arrows show the corresponding equational simplifications.

Statistical Model Checking Methodology

We propose the following methodology to verify hierarchically structured distributed systems: (1.) Specification of the real-world system as a composite actor system in Maude/ PMaude using the composite actor model as a foundation and fulfilling the formal requirements for the scheduling approach for composite actor models. (2.) Definition of standard probabilistic temporal logic and quantitative temporal logic properties for the system. (3.) (Automated) transformation of the model specified in (1.) to a scheduled composite actor model specification and specification of an initial state which consists of the initial state of the specification of the model defined in (1.) and an instance of the top-level scheduler of the scheduling approach for the composite actor model. (4.) Formal analysis of the properties defined in (2.) over the initial state using the statistical model checker PVeStA. Besides the formal requirements, we further require that the specification does not contain zero-time loops, i.e., a recurring series of messages is produced where each message has the same activation time.

More technically the statistical model checker PVeStA calls the operator run to start the execution of a sample of a composite actor model. The operator is repeatedly called by PVeStA until a specified amount (denoted by the variable LIMIT) of global time has passed. In Maude, the run operator is defined as follows: Several case studies have been conducted to validate this methodology. For example, the approach has been used to detect bugs in the design of a group key distribution service [START_REF] Wirsing | Design and Analysis of Cloud-Based Architectures with KLAIM and Maude[END_REF][START_REF] Eckhardt | A Formal Analysis of Security Properties in Cloud Computing[END_REF], to predict the performance of a distributed brokerbased Publish/Subscribe service [START_REF] Wirsing | Design and Analysis of Cloud-Based Architectures with KLAIM and Maude[END_REF][START_REF] Mühlbauer | Formal Specification and Analysis of Cloud Computing Management[END_REF], and to improve the availability of service of Internet-based service architectures such as Clouds using a denial of service protection mechanism together with dynamic resource provisioning [START_REF] Eckhardt | Stable Availability under Denial of Service Attacks through Formal Patterns[END_REF].

From a more practical point of view, the statistical model checking methodology for hierarchical specifications based on the composite actor model has proven itself effective in our case studies. Compared to LTL model checking, we were able to model check meaningful qualitative as well as quantitative properties of rather large instances of the specifications. E.g., during the work on [START_REF] Eckhardt | Stable Availability under Denial of Service Attacks through Formal Patterns[END_REF], we model checked quantitative properties with a high confidence of 99% on specification instances with up to 500 individual actors. Thereby, the statistical model checking process was running for several hours on a cluster of 32 machines. Model checking just simple qualitative properties with LTL model checking on the same specification instances would have exceeded a graspable timeframe.

Related Work & Concluding Remarks

This work is mainly related to the ideas of actors [START_REF] Hewitt | A universal modular actor formalism for artificial intelligence[END_REF][START_REF] Hewitt | Laws for communicating parallel processes[END_REF][START_REF] Agha | Actors: a model of concurrent computation in distributed systems[END_REF], PMaude [START_REF] Agha | PMaude: Rewrite-based Specification Language for Probabilistic Object Systems[END_REF], the statistical model checker PVeSTA [START_REF] Alturki | PVeStA: A parallel statistical model checking and quantitative analysis tool[END_REF], and the original scheduling approach for flat actor configurations mentioned in [START_REF] Alturki | Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol[END_REF]. Only recently Ölveczky et al. [START_REF] Bentea | Probabilistic real-time rewrite theories and their expressive power[END_REF] proposed a probabilistic strategy language for probabilistic rewrite theories that is implemented in Maude and offers the possibility of statistical model checking with a model checking algorithm implemented as a Maude meta-level functionality. Bruni et al. [START_REF] Bruni | Modelling and Analyzing Adaptive Self-assembly Strategies with Maude[END_REF] have shown that a framework to describe adaptive behavior in multi-layered component hierarchies can naturally be realized in Maude based on the Reflective Russian Dolls Model and quantitatively analyzed using PVeSTA.

In a broader sense this work is related to process calculi such as the Mobile Ambients calculus and its probabilistic extension [START_REF] Cardelli | Mobile ambients[END_REF][START_REF] Kwiatkowska | Probabilistic Mobile Ambients[END_REF]. While process calculi mainly focus on dynamic behavior, our approach also emphasizes the representation of data.

In this paper we have presented the composite actor model and argued that it is well-suited for specifying concurrent Cloud and Internet-based systems which are composed of various participants and subsystems and are hierarchically structured in different layers and networks. Our model extends the actor model of concurrent computation and supports an arbitrary hierarchical composition of entities. As a second main result we have defined a model transformation which extends a composite actor specification by a new scheduling approach that guarantees the absence of nondeterminism and, as a consequence, enables statistical model checking. To show the soundness of our approach we have proven termination and confluence of the (equational part of the) scheduler specification and shown the absence of unquantified nondeterminism in scheduled composite actor specifications. To prove the soundness of the model transformation we introduced the notions of strong zero-time rule confluence and time-passing bisimulation and showed that the transformation is a time-passing bisimulation for strongly zero-time rule confluent composite actor specifications.

Until today we have successfully applied the composite actor approach to three non-trivial Cloud case studies [START_REF] Eckhardt | Stable Availability under Denial of Service Attacks through Formal Patterns[END_REF][START_REF] Wirsing | Design and Analysis of Cloud-Based Architectures with KLAIM and Maude[END_REF][START_REF] Mühlbauer | Formal Specification and Analysis of Cloud Computing Management[END_REF][START_REF] Eckhardt | A Formal Analysis of Security Properties in Cloud Computing[END_REF] by formally specifying and analyzing them using Maude and PVeSTA.

In the future we plan to extend and complement our composite actor modeling approach by a correct-by-construction model-driven program synthesis. As a target system we choose the ØMQ (zeromq) socket library [START_REF]ØMQ: The Intelligent Transport Layer[END_REF] to act as a concurrent framework for Cloud services. Currently, we have partially implemented one of our case studies [START_REF] Eckhardt | Stable Availability under Denial of Service Attacks through Formal Patterns[END_REF] as a ØMQ application based on the Maude model and shown that large parts of the transformation process can be automated.

Fig. 1 .

 1 Fig. 1. Example of a Russian Dolls model of a system with boundaries.

<0:

  Firewall | config: <0.0 :Subsystem | config: <0.0.0 :C1> . . . <0.0.N-1 :C N >>>

<

  A : T | config: C, AS> (t, X<-M) => < A : T | config: C, (t', X'<-M'), AS'>

  mb < A : T | config: AC, AS > : InertActor . cmb ACT : InertActor if flatActor(ACT) . op flatActor : Actor -> Bool . eq flatActor(< A : T | config: C, AS >) = false . eq flatActor(ACT) = true [owise] .

  eq [create-loc-msg1] : <A : T | config: SM C, AS> = [A,SM] <A : T | config: C, AS> . eq [create-loc-msg2] : SM C S = [ toplevel, SM ] C S . Then, terms of sort LocScheduleMsg are pulled up the hierarchy by the pull -up equation and finally inserted in the scheduler by the insert-in-scheduler equation. eq [pull-up] : < A : T | config: LSM C, AS > = LSM < A : T | config: C, AS > . eq [insert-in-scheduler] : LSM S = insert(S, LSM) . Terms of sort LocActiveMsg are pushed down the hierarchy by the equation push-down and are finally inserted in the correct subconfiguration by the equation insert-in-configuration or by the equation insert-toplevel, if the scheduled message has been emitted in the top-most level. eq [push-down] : < A : T | config: C, AS > {A . A', AM} = < A : T | config: C {A . A', AM}, AS > . eq [insert-in-configuration] : < A : T | config: C, AS > {A , AM} = < A : T | config: C AM, AS > . eq [insert-toplevel] : {toplevel, AM} S = AM S .Finally, the operator insert inserts a term of sort LocScheduleMsg into the scheduler. op insert : Scheduler LocScheduleMsg -> Scheduler . op insert : ScheduleList LocScheduleMsg -> ScheduleList . eq insert({gt | SL}, LSM) = {gt | insert(SL,LSM)} . eq [insert-list] : insert([A1,[(t1, A<-M1)]]; SL, [A2,[(t2, A'<-M2)]]) = if (t1 < t2) or ((t1 == t2)) and lt(M1,M2) then [A1,[(t1, A<-M1)]] ; insert(SL,[A2,[(t2, A'<-M2)]]) else [A2,[(t2, A'<-M2)]] ; [A1,[(t1, A<-M1)]] ; SL fi . eq insert(nil, LSM) = LSM .

  of M and SM = (Can(SM ), L SM , µ SM , L SM ,t ----→ SM ) of SM , where L SM = L M is the set of rules in M , µ M is a family of distribution functions, µ SM is a family of distribution functions which coincides with µ M on the image of the model transformation, and Can(M ) and Can(SM ) are the canonical terms of sort config of M and SM, respectively. The labelled transition systems M and SM describe the set of all well-timed one-step rewrites of the probabilistic rewrite theory of M and SM , respectively. Definition (Simulation and Bisimulation). Given timed probabilistic (tp) labelled transition systems A = (A, L A , µ A , l,t -→ A ) and B = (B, L B , µ B , l,t -→ B ) and a bijection of the labels L A ↔ L B , where µ A : A×L A → [0, 1] and µ B : B×L B → [0, 1] are families of probability distributions. Then a simulation of tp-transition systems is a binary relation H ⊆ A × B such that if a l A ,t --→ A a and aHb then there is b such that b l B ,t --→ B b and a Hb , µ A (a, l A ) = µ B (b, l B ), and l A ↔ l B . If both H and H -1 are simulations, then we call H a bisimulation.Remark (Relation between M and SM). We relate the scheduled composite actor specification SM with the composite actor specification M as follows: For any canonical term u of SM in form AC {t | SL} one can construct a term û of M by inserting all messages of SL into the right subconfiguration of AC: for each term [A , [(at1, A1 <-M)]] of sort LocScheduleMsg of SL, the message (at1, A1 <-M) is inserted into the subconfiguration AC at adress A (or into the toplevel configuration of AC if A = toplevel).

Theorem 2 .

 2 Let M be a well-formed composite actor model specification and SM the scheduled composite actor model specification that is the result of the model transformation M → SM . Then SM is a simulation of M. Proof sketch. H : SM → M is a simulation where H = {(u, û)|u = AC {gt | SL} for some AC, gt, SL}.

  op run : Config Float -> Config . eq run(AC {gt | SL}, LIMIT) = if (gt <= LIMIT) then run(step(AC {gt | SL}), LIMIT) else AC {gt | SL} fi .

In general, it is possible to allow an actor to have its inner soup(s) in arbitrarily named attributes. The convention of having a single sub-configuration in a predefined attribute, however, simplifies scheduling approaches for statistical model checking.

Terms of sort LocScheduleMsg are used to store the address of the actor in whose configuration a scheduled message was emitted (or the topmost address if the message was emitted at the top-most level) and the scheduled message itself. Similarly, terms of sort LocActiveMsg are used to store the same address but of a scheduled message that has been made active by the scheduler. These auxiliary messages are used in our scheduling approach.

This work has been partially sponsored by the EU-funded projects FP7-257414 ASCENS and FP7-256980 NESSoS, and AFOSR Grant FA8750-11-2-0084. Tobias Mühlbauer is also partially supported by the Google Europe Fellowship in Structured Data Analysis. We thank Mirco Tribastone for his helpful comments on this paper. We further thank all reviewers for their valuable feedback.

Definition (Complete Zero-Time *-Transition). A zero-time *-transition a ⇒ L a consists of a finite sequence of zero-time transitions; it is complete if it cannot be extended further:

For n ∈ N, L : {1, . . . , n} → L A we call a ⇒ L a a zero-time transition if and only if ∃a 1 , . . . , a n such that a

If π : {1, . . . , n} → {1, . . . , n} is a permutation, we write a ⇒ π(L) a for the zero-time *-transition a ⇒ L a , where L (i) = L(π(i)) for i = 1, . . . , n. Definition (Time-passing Simulation). Given tp-labelled transition systems

Corollary. Every simulation (of tp transition systems) is a time-passing simulation. Definition (Strong Zero-Time Rule Confluence). An actor specification is called strongly zero-time rule confluent if the order of applying any two zero-time actor rules to the same term does not matter:

A specification M is strongly zero-time rule confluent, if for any two zero-time rules r 1 , r 2 with labels l r1 , l r2 and for all canonical terms u, v, w of sort Config: ---→ w and v = w . Many composite actor specifications satisfy the condition of strong zero-time rule confluence; in particular, except for one [START_REF] Eckhardt | Stable Availability under Denial of Service Attacks through Formal Patterns[END_REF], all our published case studies studies [START_REF] Wirsing | Design and Analysis of Cloud-Based Architectures with KLAIM and Maude[END_REF][START_REF] Mühlbauer | Formal Specification and Analysis of Cloud Computing Management[END_REF][START_REF] Eckhardt | A Formal Analysis of Security Properties in Cloud Computing[END_REF] are strongly zero-time rule confluent. Lemma 2. Let M be a well-formed and strongly zero-time rule confluent composite actor specification. For any zero-time *-transition

----→ v n and any rule r which is applicable with label l to a message m in v 0 , the following holds:

(1.) If r is not applied in any of the v i then m occurs in all v i and r stays applicable with label l in all v i , i = 0 . . . n.

Proof. Proof by induction on the length n of the transition. Lemma 3. Let M be well-formed and strongly zero-time rule confluent and SM be the result of the model transformation M → SM . For all canonical terms v 0 of sort Config of M , w 0 of SM with ŵ0 = v 0 , and any zero-time *-transition v 0 ⇒ L v with v ∈ M >0 there exist w ∈ SM >0 and a permutation π such that w 0 ⇒ π(L) w and ŵ = v.

Proof. Proof by induction on the length of the transition using Lemma 2.

Theorem 3. Let M be a well-formed and strongly zero-time rule confluent composite actor model specification and SM be the result of the model transformation M → SM . Then M and SM are time-passing bisimilar.

Proof. Consider the relation H as in Theorem 2 and let H >0 ⊆ SM >0 ×M >0 .

Remark. One can also solve the general case where interdependent messages have the same activation time and the specification is not zero-time rule commutative by assigning random delays to the scheduled activation times of the dependent messages. As in [START_REF] Agha | PMaude: Rewrite-based Specification Language for Probabilistic Object Systems[END_REF], we assume that the probability that a random number is sampled twice is 0. If this process is recursively applied to the dependent messages in the scheduler, a fix point is reached in which there exist no two dependent messages with the same scheduled activation time.

Example: Scheduling Approach for the Composite Actor Model

As an example of how the scheduling approach works, we model a forest of binary trees, where the leaf nodes send messages to each other while the intermediate nodes only forward and delay these messages In both specifications, A and A' are variables of sort Address, t of sort Float, C of sort Config, pref: Address Nat -> Address an operator returning a prefix of a given length, |_| : Address -> Nat an operator returning the length of a given address, and rndA: Nat -> Address an operator returning a random Address of a given length for a binary tree.

The initial configuration consists of two actor trees and the top-level scheduler which contains one message. The following listing shows this configuration, where the original one (M ) is shown on the left, and SM on the right.