Jilles S Dibangoye

Olivier Buffet

Learning to Act in Decentralized Partially Observable MDPs

We address a long-standing open problem of reinforcement learning in decentralized partially observable Markov decision processes. Previous attempts focussed on different forms of generalized policy iteration, which at best led to local optima. In this paper, we restrict attention to plans, which are simpler to store and update than policies. We derive, under certain conditions, the first near-optimal cooperative multi-agent reinforcement learning algorithm. To achieve significant scalability gains, we replace the greedy maximization by mixed-integer linear programming. Experiments show our approach can learn to act near-optimally in many finite domains from the literature.

Introduction

Decentralized partially observable Markov decision processes (Dec-POMDPs) emerged as the standard framework for sequential decision making by a team of collaborative agents [START_REF] Bernstein | The Complexity of Decentralized Control of Markov Decision Processes[END_REF]. A key assumption of Dec-POMDPs is that agents can neither see the actual state of the system nor explicitly communicate their noisy observations with each other due to communication cost, latency or noise, hence providing a partial explanation of the double exponential growth at every control interval of the required memory in optimal algorithms [START_REF] Hansen | Dynamic Programming for Partially Observable Stochastic Games[END_REF][START_REF] Szer | A Heuristic Search Algorithm for Solving Decentralized POMDPs[END_REF][START_REF] Oliehoek | Optimal and Approximate Q-value Functions for Decentralized POMDPs[END_REF][START_REF] Amato | Incremental Policy Generation for Finite-Horizon DEC-POMDPs[END_REF][START_REF] Oliehoek | Incremental Clustering and Expansion for Faster Optimal Planning in Dec-POMDPs[END_REF][START_REF] Dibangoye | Structural Results for Cooperative Decentralized Control Models[END_REF]2016). While planning methods for finite Dec-POMDPs made substantial progress in recent years, the formal treatment of the corresponding reinforcement learning problems received little attention so far. The literature of multi-agent reinforcement learning (MARL) can be divided into two main categories: concurrent and team approaches [START_REF] Tan | Multi-agent Reinforcement Learning: Independent vs. Cooperative Agents[END_REF][START_REF] Panait | Cooperative multi-agent learning: The state of the art[END_REF].

Proceedings of the 35 th International Conference on Machine Learning, Stockholm, Sweden, PMLR 80, 2018. Copyright 2018 by the author(s).

Perhaps the dominant paradigm in MARL is the concurrent approach, which involves multiple simultaneous learners: typically, each agent has its learning process. Self-interested learners, for example, determine their best-response behaviors considering their opponents are part of the environment, often resulting in local optima [START_REF] Brown | Iterative Solutions of Games by Fictitious Play[END_REF][START_REF] Hu | Multiagent Reinforcement Learning: Theoretical Framework and an Algorithm[END_REF][START_REF] Littman | Markov games as a framework for multiagent reinforcement learning[END_REF]. While concurrent learning can apply in Dec-POMDPs, a local optimum may lead to severely suboptimal performances [START_REF] Peshkin | Learning to Cooperate via Policy Search[END_REF][START_REF] Zhang | Coordinated Multi-Agent Reinforcement Learning in Networked Distributed POMDPs[END_REF][START_REF] Kraemer | Multi-agent reinforcement learning as a rehearsal for decentralized planning[END_REF][START_REF] Nguyen | Policy gradient with value function approximation for collective multiagent planning[END_REF]. Also, methods of this family face two conceptual issues that limit their applicability. The primary concern is that of the co-adaptation dilemma, which arises when each attempt to modify an agent behavior can ruin learned behaviors of its teammates. Another major problem is that of the multi-agent credit assignment, that is, how to split the collective reward among independent learners. Alternatively, the team approach involves a single learner acting on behalf of all agents to discover a collective solution [START_REF] Salustowicz | Learning Team Strategies: Soccer Case Studies[END_REF][START_REF] Miconi | When Evolving Populations is Better Than Coevolving Individuals: The Blind Mice Problem[END_REF]. Interestingly, this approach circumvents the difficulties arising from both the co-adaptation and the multi-agent credit assignment. Coordinated agents, for example, simultaneously learn their control choices and the other agent strategies assuming instantaneous and free explicit communications [START_REF] Guestrin | Coordinated Reinforcement Learning[END_REF][START_REF] Kok | Sparse Cooperative Q-learning[END_REF]. While methods of this family inherit from standard single-agent techniques, they need to circumvent two significant drawbacks: the explosion in the state space size; and the centralization of all learning resources in a single place. Recently, team algorithms ranging from Q-learning to policy-search have been introduced for finite Dec-POMDPs, but with no guaranteed global optimality [START_REF] Wu | Monte-Carlo Expectation Maximization for Decentralized POMDPs[END_REF][START_REF] Liu | Stickbreaking policy learning in Dec-POMDPs[END_REF]2016;[START_REF] Kraemer | Multi-agent reinforcement learning as a rehearsal for decentralized planning[END_REF]. So, it seems one can either compute local optima with arbitrary bad performances or calculate optimal solutions but assuming noise-free, instantaneous and explicit communications.

A recent approach to optimally solving Dec-POMDPs suggests recasting them into occupancy-state MDPs (oMDPs) and then applying (PO)MDP solution methods [START_REF] Dibangoye | Optimally Solving Dec-POMDPs As Continuous-state MDPs[END_REF][START_REF] Dibangoye | Optimally solving Dec-POMDPs as Continuous-State MDPs: Theory and Algorithms[END_REF]b;2016). In these oMDPs, the states called occupancy states are distributions over hidden states and joint histories of the original problem, and actions called decision rules are mappings from joint histories to con-trols [START_REF] Nayyar | Optimal Control Strategies in Delayed Sharing Information Structures[END_REF][START_REF] Oliehoek | Sufficient Plan-Time Statistics for Decentralized POMDPs[END_REF][START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF]. This approach achieves scalability gains by exploiting the piece-wise linearity and convexity of the optimal value function. Since this methodology was successfully applied for planning in Dec-POMDPs, it is natural to wonder which benefits it could bring to the corresponding MARL problem. Unfortunately, a straightforward application of standard RL methods to oMDPs will face three severe limitations. First, occupancy states are unknown, and hence must be estimated. Second, they lie in a continuum making tabular RL methods inapplicable. Finally, the greedy maximization is computationally demanding in decentralized stochastic control problems [START_REF] Radner | Team Decision Problems[END_REF][START_REF] Dibangoye | Pointbased incremental pruning heuristic for solving finitehorizon DEC-POMDPs[END_REF][START_REF] Kumar | Constraint-based dynamic programming for decentralized POMDPs with structured interactions[END_REF][START_REF] Oliehoek | Heuristic search for identical Bayesian games[END_REF]. This paper extends the methodology of Dibangoye et al. to MARL, focussing on the three major issues that limit its applicability. Our primary result is the proof that, by restricting attention to plans instead of policies, a linear function over occupancy states and joint decision rules, which is simple to store and update, can capture the optimal performance for Dec-POMDPs. We further use plans instead of policies in a policy iteration algorithm, with the plan always being improved with respect to a linear function and a linear function always being driven toward the linear function for the plan. Under accurate estimation of the occupancy states, the resulting algorithm, called occupancystate SARSA (oSARSA) [START_REF] Rummery | On-line Q-learning using connectionist systems[END_REF], is guaranteed to converge with probability one to a near-optimal plan for any finite Dec-POMDP. To extend its applicability to higher-dimensional domains, oSARSA replaces the greedy (or soft) maximization by a mixed-integer linear program for finite settings. Altogether, we obtain a MARL algorithm that can apply to finite Dec-POMDPs. Experiments show our approach can learn to act near-optimally in many finite domains from the literature.

We organize the remainder of this paper as follows. Section 2 extends a recent planning theory, starting with a formal definition of finite Dec-POMDPs. We proceed with the introduction of a framework for centralized MARL in Dec-POMDPs along with solutions to the three limitations mentioned above in Section 3. We further present the resulting algorithm oSARSA along with convergence guarantees in Section 4. Finally, we conduct experiments in Section 5, demonstrating our approach learns to act optimally in many finite domains from the literature. Proofs are provided in the companion technical report [START_REF] Dibangoye | Learning to Act in Decentralized Partially Observable MDPs[END_REF].

Planning in Dec-POMDPs as oMDPs

Finite Dec-POMDPs

A finite Dec-POMDP is a tuple M . " pn, X, tU i u, tZ i u, p, r, , γ, b 0 q, where n denotes the number of agents involved in the decentralized stochastic control process; X is a finite set of hidden world states, denoted x or y; U i is a finite private control set of agent i P v1; nw, where U " U 1 ˆ¨¨¨ˆU n specifies the set of controls u " pu 1 , . . . , u n q; Z i is a finite private observation set of agent i, where Z " Z 1 ˆ¨¨¨ˆZ n specifies the set of observations z " pz 1 , . . . , z n q; p describes a transition function with conditional density p u,z px, yq; r is a reward model with immediate reward rpx, uq, we assume rewards are two-side bounded, i.e., for some c P R `, @x P X, u P U : |rpx, uq| ď c; is the planning horizon; γ P r0, 1s denotes the discount factor; and b 0 is the initial belief state with density b 0 px 0 q. We shall restrict attention to finite planning horizon ă 8 since an infinite planning horizon solution is within a small scalar ą 0 of a finite horizon solution where " rlog γ pp1 ´γq {cqs.

Because we are interested in MARL, we assume an incomplete knowledge about M , i.e., p and r are either unavailable or only through a generative model. Hence, the goal of solving M is to find a plan, i.e., a tuple of individual decision rules, one for each agent and time step: ρ .

" pa 1 0: , . . . , a n 0: q. A tth individual decision rule a i t : O i t Þ Ñ PpU i q of agent i prescribes private controls based on the whole information available to the agent up to the tth time step, i.e., history of controls and observations o i t " pu i 0:t´1 , z .

" λ 1 r t `¨¨¨`λ r , where λ t denotes the time-step dependent weighting factors, often set to λ t " γ t for discounted problems. For any control interval t, joint plans a 0:t of interest are those that achieve the highest performance measure Jpa 0:t q

. " E a0:t tR 0 | b 0 u starting at b 0 , where E a0:t t¨u denotes the expectation with respect to the probability distribution over state-action pairs joint plan a 0:t induces, in particular Jpρq . " Jpa 0: ´1q for ρ . " a 0: ´1. One can show that, in Dec-POMDPs, there always exists a deterministic plan that is as good as any stochastic plan (see Puterman, 1994, Lemma 4.3.1). Unfortunately, there is no direct way to apply the theory developed for Markov decision processes [START_REF] Bellman | Dynamic Programming[END_REF][START_REF] Puterman | Markov Decision Processes, Discrete Stochastic Dynamic Programming[END_REF] to Dec-POMDPs, including: the Bellman optimality equation; or the policy improvement theorem. To overcome these limitations, we rely on a recent theory by Dibangoye et al. that recasts M into an MDP, thereby allowing knowledge transfer from the MDP setting to Dec-POMDPs.

Occupancy-State MDPs

To overcome the fact that agents can neither see the actual state of the system nor explicitly communicate their noisy observations with each other, [START_REF] Szer | A Heuristic Search Algorithm for Solving Decentralized POMDPs[END_REF] and later on [START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF] suggest formalizing M from the perspective of a centralized algorithm. A centralized algorithm acts on behalf of the agents by selecting a joint decision rule to be executed at each control interval based on all data available about the system, namely the information state. The information state at the end of control interval t, denoted ι t`1

. " pb 0 , a 0:t q, is a sequence of joint decision rules the centralized algorithm selected starting at the initial belief state. Hence, the information state satisfies the following recursion: ι 0 . " pb 0 q and ι t`1 . " pι t , a t q for all control interval t, resulting in an ever-growing sequence. To generalize the value from one information state to another one, Dibangoye et al. introduced the concept of occupancy states. The occupancy state at control interval t, denoted s t

. " Ppx t , o t |ι t q, is a distribution over hidden states and joint histories conditional on information state ι t at control interval t. Interestingly, the occupancy state has many important properties. First, it is a sufficient statistic of the information state when estimating the (current and future) reward to be gained by executing a joint decision rule:

Rps t , a t q . " ÿ x ÿ o s t px, oq ÿ u a t pu|oq ¨rpx, uq.
In addition, it describes a deterministic and fully observable Markov decision process, where the next occupancy state depends only on the current occupancy state and next joint decision rule, for all y P X, o P O, u P U, z P Z:

T ps t , a t q . " s t`1 s t`1 py, po, u, zqq . " a t pu|oq ÿ x s t px, oq ¨pu,z px, yq.

The process the occupancy states describe is known as the occupancy-state Markov decision process (oMDP), and denoted M 1 . " pS, A, R, T, , γ, s 0 q. Similarly to POMDPs, it was proven that Dec-POMDPs can be recasted into MDPs, called oMDPs, and an optimal solution of the resulting oMDP is also an optimal solution for the original Dec-POMDP [START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF]. M 1 is an -steps deterministic and continuous MDP with respect to M , where S . " Y tPv0; ´1w S t is the set of occupancy states up to control interval ´1; A . " Y tPv0; ´1w A t is the set of joint decision rules up to control interval ´1; R is the reward model; and T is the transition rule; s 0 is the initial occupancy state, which is essentially the initial belief in M ; γ and are as in M . It is worth noticing that there is no need to construct explicitly M 1 ; instead we use M (when available) as a generative model for the occupancy states T ps t , a t q and rewards Rps t , a t q, for all control intervals t.

To better understand why we use plans instead of policies and how they relate, consider the MDP case. The solution of any finite MDP called a policy π : S Þ Ñ A can be represented as a decision tree, where nodes are labelled with actions and arcs are labelled with states. Since an oMDP is also an MDP, its policies can also be represented as decision trees, except that actions are decision rules and states are occupancy states. In contrast to standard MDPs, oMDPs are deterministic. This means that only a single branch in the decision-tree representation-i.e., a sequence of actions-is necessary to act optimally in oMDPs. A single branch of a decision tree is called a plan. Hence policies are more general than plans, but in deterministic MDPs, both can be employed while achieving optimal performance (plans inducing an open-loop approach, and policies a closed-loop approach). We shall restrict attention to plans because they are more concise than policies. Below, we review a closedloop approach based on the dynamic programming theory [START_REF] Bellman | Dynamic Programming[END_REF].

For any finite M , the Bellman equation is written as follows: for all occupancy state s t P S t , and some fixed policy π,

V π t ps t q . " Rps t , πps t qq `λ1 V π t`1 pT ps t , πps t qqq (1)
with boundary condition V π p¨q . " 0, describes the return of a particular occupancy state s t when taking decision rule a t " πps t q prescribed by π. The equation for an optimal policy π ˚is referred to as the Bellman optimality equation: for any control interval t, and occupancy state s t ,

V t ps t q . " max atPA Rps t , a t q `λ1 V t`1 pT ps t , a t qq (2)
with boundary condition V ˚ p¨q . " 0. Unfortunately, occupancy states lie in a continuum, which makes exact dynamic programming methods infeasible. Interestingly, when optimized exactly, the value function solution of (2) along with the boundary condition is always piece-wise linear and convex in the occupancy-state space [START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF].

Lemma 1. For any arbitrary M 1 , the solution V 0: of (2) is convex in the occupancy-state space. If we restrict attention to deterministic policies and finite M (and corresponding M 1 ), the solution of ( 2) is piece-wise linear and convex in the occupancy-state space. Hence, the optimal value at any occupancy state s t is as follows:

V t ps t q . " max αtPΓt xs t , α t y, (3)
where xs t , α t y is used to express the expectation of a linear function α t (also called α-vectorin the probability space defined by sample space X ˆO, the σ-algebra X ˆO and the probability distribution s t ; and Γ t is the set of all tth α-vectors.

Lemma 1 shows that for any arbitrary M and corresponding M1 , the solution of (2), represented by sets Γ 0: , is convex in the occupancy-state space. Each α-vector defines the value function over a bounded region of the occupancy-state space. In addition, it is associated with a plan, defining the optimal plan for a bounded region of the occupancy-state space. Sets Γ 0: are iteratively improved by adding a new α-vector that dominates current ones over certain regions of the occupancy-state space. The α-vector to be added is computed using point-based Bellman backup operator H:

rHΓ t`1 sps t q " arg max α a t : aPAt,αt`1PΓt`1 xs t , α a t y,
where α a t px, oq .

" Etrpx, uq `λ1 α t`1 py, po, u, zqq|au, for each hidden state x P X, and joint history o P O. To keep the number of α-vectors manageable, one can prune those that are dominated over the entire occupancy-state space. All in all, the oMDP reformulation permits us to solve finite M by means of M 1 using near-optimal planning methods leveraging on the special structure of the optimal value function [START_REF] Shani | A survey of pointbased POMDP solvers[END_REF]. This methodology results in the current state-of-the-art algorithm to optimally solving finite Dec-POMDPs [START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF]. So it seems natural to wonder if the same methodology can also succeed when applied to the corresponding reinforcement-learning problem. In other words, how can a centralized algorithm learn to coordinate a team of agents with possibly contradicting perceptual information?

Learning in Dec-POMDPs as oMDPs

Using the oMDP reformulation, a natural approach to achieve centralized RL for decentralized stochastic control suggests applying exact RL methods. In the Q-learning algorithm [START_REF] Watkins | Q-Learning[END_REF], for example, one would learn directly the Q-value function when following a fixed policy π: for any control interval t P v0; ´1w,

Q π t ps t , a t q
. " Rps t , a t q `λ1 V π t`1 pT ps t , a t qq (4)

with boundary condition Q π p¨, ¨q " 0. The policy improvement theorem provides a procedure to change a sub-optimal policy π into an improved one π [START_REF] Howard | Dynamic Programming and Markov Processes[END_REF]: for any control interval t P v0; ´1w, πps t q . " arg max atPAt Q π t ps t , a t q.

(5)

Unfortunately, this approach has three severe limitations. First, the occupancy states are unknown and must be estimated. Second, even if we assume a complete knowledge of the occupancy states, they lie in a continuum, which precludes exact RL methods to accurately predict α-vectors even in the limit of infinite time and data. Finally, the greedy maximization required to improve the value function proved to be NP-hard in finite settings [START_REF] Radner | Team Decision Problems[END_REF][START_REF] Dibangoye | Pointbased incremental pruning heuristic for solving finitehorizon DEC-POMDPs[END_REF][START_REF] Kumar | Constraint-based dynamic programming for decentralized POMDPs with structured interactions[END_REF][START_REF] Oliehoek | Heuristic search for identical Bayesian games[END_REF].

Addressing Estimation Issues

Although mappings T and R in M 1 are unknown to either agents or a centralized algorithm, one can instead estimate on the fly both T ps 0 , a 0:t´1 q and RpT ps 0 , a 0:t´1 q, a t q for some fixed plan ρ . " a 0: ´1 through successive interactions of agents with the environment. To this end, we shall distinguish between two settings. The first one assumes a generative model is available during the centralized learning phase, e.g. a black box simulator; and the second does not. In both cases, we build on the concept of replay pool [START_REF] Mnih | Human-level control through deep reinforcement learning[END_REF], except that we extend it from stationary single-agent domains to non-stationary multi-agent domains.

If a generative model is available during the learning phase, then a Monte Carlo method can approximate T ps 0 , a 0:t´1 q and RpT ps 0 , a 0:t´1 q, a t q arbitrary closely. To this end, the generative model allows the agents to sample experiences generated from M . An -steps experience is a 4-tuple ξ .

" px 0: ´1, u 0: ´1, r 0: ´1, z 1: q, where x 0: ´1 are sampled hidden states, u 0: ´1 are controls made, r 0: ´1 are reward signals drawn from the reward model, and z 1: are the resulting observations, drawn from the dynamics model. If we let D ρ .

" tξ ris u iPv1:Kw be the replay pool of K i.i.d random samples created through successive interactions with the generative model, then empirical occupancy state ŝt « T ps 0 , a 0:t´1 q and reward Rt « RpT ps 0 , a 0:t´1 q, a t q corresponding to the current D ρ are given by: for any control interval t P v0 : ´1w, ŝt px, oq

.

" 1 K ř K i"1 δ x px ris t q ¨δo pu ris 0:t , z ris
1:t q (6) and Rt . " 1 K ř K i"1 r ris t , (7)
where δ x p¨q and δ o p¨q denote the delta-Dirac mass located in hidden state and joint history pair, respectively. By the law of large numbers the sequence of averages of these estimates converges to their expected values, and the standarddeviation of its error falls as 1{ ? K (Sutton & Barto, 1998, chapter 5). The error introduced by Monte Carlo when estimating T pŝ t´1 , a t´1 q instead of T ps 0 , a 0:t´1 q is upper bounded by 2 { ? K. The proof follows from the performance guarantee of the policy-search algorithm by [START_REF] Bagnell | Policy Search by Dynamic Programming[END_REF]. Hence, to ensure the learned value function is within ą 0 of the optimal one, one should set the replaypool size to K " Θp4 2 2 q. When no generative model is available, the best we can do is to store samples agents collected during the learning phase into replay pools D ρ , one experience for each episode within the limit size of K. We maintain only the K recent experiences, and may discard 1 hidden states since they are unnecessary for the updates of future replay pools and the performance measure. The rationale behind this approach is that it achieves the same performances as a Monte Carlo method for the task of approximating T ps 0 , a 0:t´1 q and RpT ps 0 , a 0:t´1 q, a t q given a fixed plan ρ . " a 0: ´1. In fact, if we let D ρ be a replay pool of K i.i.d. samples generated according to ρ, the empirical occupancy state ŝt « T ps 0 , a 0:t´1 q and reward Rt « RpT ps 0 , a 0:t´1 q, a t q corresponding to D ρ are given by ( 6) and ( 7), respectively. One can further show this approach preserves performance guarantees similar to those obtained when using a generative model.

Addressing Prediction Issues

The key issue with large spaces of occupancy states and decision rules is that of generalization, that is, how experiences with a limited subset of occupancy states and decision rules can produce a good approximation over a much larger space. Fortunately, a fundamental property of oMDPs is the convexity of the optimal value function over the occupancystate space, see Lemma 1. Building on this property, we demonstrate a simple yet important preliminary result before stating the main result of this section.

Lemma 2. For any arbitrary M 1 (resp. M ), the optimal Qvalue function is the upper envelope of sets Ω 0: of α-vectors over occupancy states and joint decision rules: for any control interval t, Q t ps t , a t q " max qtPΩ t xs τ d a τ , q t y, where q t P Ω t are appropriate α-vectors, and s τ d a τ denotes the Hadamard product 2 .

Lemma 2 generalizes the convexity property demonstrated in Lemma 1 from optimal value functions over occupancy states to optimal value functions over occupancy states and decision rules. As a consequence, finite sets Ω 0: ´1 of αvectors can produce solutions arbitrarily close to the optimal Q-value function Q 0: ´1. Though Q-value function Q 0: ´1 generalizes from a pair of occupancy state and decision rule to another one, storing and updating a convex hull is non trivial. Instead of learning the optimal Q-value function over all occupancy states and decision rules, we explore a simpler yet tractable alternative, which will prove sufficient to preserve ability to eventually find an optimal plan starting at initial occupancy state s 0 .

Theorem 1. For any arbitrary M 1 (resp. M ), the Q-value function Q ρ 0 : ´1 under an optimal plan ρ ˚. " a 0: ´1 starting at initial occupancy state s 0 is linear in occupancy states and decision rules: Q ρ t ps t , a t q " xs t d a t , q ρ t y where q ρ t .

" arg max qtPΩ t xT ps 0 , a 0:t´1 q d a t , q t y .

Theorem 1 proves that the Q-function for a given optimal joint plan achieves performance at the initial occupancy state s 0 as good as the Q-value function for an optimal joint policy. Standard policy iteration algorithms search for an optimal joint policy, which requires a finite set of αvectors to approximate V ˚/Q ˚, hence the resulting PWLC approximator is tight almost everywhere. Building upon Theorem 1, we search for an optimal ρ, which requires 2 @px, o, uq : rsτ d aτ spx, o, uq . " sτ px, oq ¨aτ pu|oq.

only a single α-vector to approximate V ρ {Q ρ , thus the resulting linear approximator is loose everywhere except in the neighborhood of a few points. The former approach may require less iterations before convergence to an optimal joint policy, but the computational cost of each iteration shall increase with the number of α-vectors maintained. The latter approach may require much more iterations, but all iteration shares the same computational cost.

Addressing Plan Improvement Issues

A fundamental theorem in many RL algorithms is the policy improvement theorem, which helps improving policies over time until convergence. This section introduces a procedure to improve a plan starting with a sub-optimal one.

Suppose we have determined the value function V ρ 0: ´1 for any arbitrary ρ . " a 0: ´1. For some control interval t P v0; ´1w, we would like to know whether or not we should change decision rules a 0:t to choose ā0:t ‰ a 0:t . We know how good it is to follow the current plan from control interval t onward-that is V ρ t -but would it be better or worse to change to the new plan? One way to answer this question is to consider selecting ā0:t at control interval t and thereafter following decision rules a t`1: ´1 of the existing ρ. The value of the resulting joint plan is given by Jpā 0:t´1 q `λ1 V ρ t`1 pT ps 0 , ā0:t´1 qq. The key criterion is whether this quantity is greater or less than Jpρq. Next, we state the plan improvement theorem for oMDPs. Theorem 2. Let ρ . " a 0: ´1 and ρ .

" ā0: ´1 be any pair of plans and J 0: be a sequence of α-vectors such that, for all t, J t px t , o t q . " Etα 0 r 0 `. . . `αt r t |b 0 , x t , o t , a 0:t´1 u. Let st . " T ps 0 , ā0:t´1 q and s t . " T ps 0 , a 0:t´1 q be occupancy states at any control interval t P v0; ´1w under ρ and ρ, respectively. Then, xā 0:t ˚´1 , a t ˚: ´1y such that t ˚" arg max tPv0; ´1w xs t ´st , J t ´λ1 V ρ t y is as good as, or better than, ρ.

Proof. The proof follows from the difference between the performance measure of ρ . " a 0: ´1 and ρ . " ā0: ´1. Let ς t pρ, ρq be the advantage of taking plan xā 0:t´1 , a t: ´1y instead of ρ: for any control interval t P v0; ´1w, ς t pρ, ρq " Jpā 0:t´1 q `λ1 V ρ t pT ps 0 , ā0:t´1 qq ´Jpρq " Jpā 0:t´1 q ´Jpa 0:t´1 q `λ1 pV ρ t ps t q ´V ρ t ps t qq " xs t ´st , J t ´λ1 V ρ t y.

If we let t ˚. " arg max t"0,1,..., ´1 ς t pρ, ρq, then plan xā 0:t ˚´1 , a t ˚: ´1y achieves the highest advantage among plan set txā 0:t´1 , a t: ´1yu tPv0; ´1w constructed based on ρ.

If t ˚" 0, then xā 0:t ˚´1 , a t ˚: ´1y " ρ, and no improved plans were found from plan set generated from ρ. Otherwise, new xā 0:t ˚´1 , a t ˚: ´1y must be better than ρ.

Theorem 2 plays the same role in the plan space as does the policy improvement theorem in the policy space. More precisely, after sampling a plan, i.e., a sequence of decision rules, it tells us which of these decision rules will improve the current plan. More specifically, it shows how, given ρ . " a 0: ´1 and α-vector q ρ 0: ´1, we can easily evaluate a change in ρ at any control interval to a particular (possibly improved) plan. To ease exploration towards promising plans, we investigate the -greedy maximization (or softmaximization). At each control interval t and occupancy state s t , it randomly selects ât with probability ; otherwise, it greedily selects ât w.r. Unfortunately, this operation proved to be NP-hard for finite M [START_REF] Radner | Team Decision Problems[END_REF][START_REF] Dibangoye | Pointbased incremental pruning heuristic for solving finitehorizon DEC-POMDPs[END_REF][START_REF] Kumar | Constraint-based dynamic programming for decentralized POMDPs with structured interactions[END_REF][START_REF] Oliehoek | Heuristic search for identical Bayesian games[END_REF]. Searching for the best decision rule requires enumerating all of them, which is not possible in large planning horizons. Instead, we present a mixed-integer linear programming (MILP) method, which successfully performs the greedy maximization for finite M . Though MILP is NP-hard in the worst case, the solution of its LP relaxation, which is in P, is often integral in our experiments. In other words, the solution of the LP relaxation is already a solution of the MILP. A similar observation was done before by Mac-Dermed & Isbell. Mixed-Integer Linear Program 1 builds on [START_REF] Macdermed | Point Based Value Iteration with Optimal Belief Compression for Dec-POMDPs[END_REF], which introduced an integer program for the greedy maximization in finite M . We also exploit the occupancy state estimation, in which ŝt replaces s t , and the current α-vector q ρ t . Mixed-Integer Linear Program 1 (For finite M ).

Maximize

s.t.: ř u j a t pu j , u i |oq " a i t pu i |o i q, @i, u i , o (9) ř u a t pu|oq " 1, @o (8)
where ta t pu|oqu and ta i t pu i |o i qu are positive and boolean variables, respectively.

Mixed-Integer Linear program 1 optimizes positive variables ta t pu|oqu uPU,oPOt , one positive variable for each control-history pair. More precisely, each variable represents the probability a t pu|oq of control u being taken given that agents experienced joint history o. Constraints must be imposed on these variables to ensure they form proper probability distributions (10), and that they result from the product of independent probability distributions (9), one independent probability distribution for each agent. In order to make the description of the conditional independence,

a t pu|oq " a 1 t pu 1 |o 1 q ˆ¨¨¨ˆa n t pu n |o n q, (11)
we use additional variables ta i t pu i |o i qu iPv1;nw,u i PU i ,o i PO i t . Marginalizing out both sides of ( 11) over all control-history pairs of all agents except agent i, denoted ´i, leads to (9). That is not sufficient to ensure conditional independence in general. If we further constrain ta i t pu i |o i qu to be boolean, then system of equations ( 9) implies (11). Given ( 9) and (10), agent variables ta i t pu i |o i qu u i PU i ,o i PO i t describe a proper probability distribution, so we omit corresponding constraints. Our greedy maximization approach is fundamentally different from previous ones, including the integer program by [START_REF] Macdermed | Point Based Value Iteration with Optimal Belief Compression for Dec-POMDPs[END_REF] and the constraint optimization program by [START_REF] Kumar | Constraint-based dynamic programming for decentralized POMDPs with structured interactions[END_REF][START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF]. First, while previous approaches made use of boolean variables, we use both positive and boolean variables instead. Next, prior approaches optimize a value function represented as a convex hull; we optimize an α-vector instead.

The oSARSA Algorithm

This section presents the oSARSA algorithm with tabular representations and function approximations (using either linear functions or deep neural networks) along with convergence guarantees. oSARSA algorithms are specializations of Policy Iteration, except that we use plans instead of policies. For the sake of conciseness, we describe a generic algorithm, which can fit to either tabular or approximate representations.

In Dec-POMDPs, the goal of oSARSA is to learn q 0: ´1, a sequence of α-vectors of an optimal plan ρ ˚. In particular, we must estimate q t px, o, uq for the current plan ρ and for all reachable state x, joint history o, control u, and any control interval t. At the same time, the algorithm changes ρ towards improved plans according to the plan improvement theorem. The improved plans are constructed by exploring the occupancy-state space according to -greedy plans (see Section 3.3). To provide good estimations, we store all experiences in data set D ρ , from which we estimate the occupancy states and returns under ρ for any control interval (see Section 3.1). Upon estimating occupancy state ŝ and selecting joint decision rule a, we update parametrized αvector q t with parameter θ t using q t`1 , D ρ and a t`1 by means of temporal difference learning: for all px, o, uq, θ rτ `1s t

. " θ rτ s t `βτ E ŝ,a,D,at`1 tδ t ∇q rτ s t px, o, uqu (12) δ t " r `λ1 q rτ s t`1 py, o 1 , u 1 q ´qrτs t px, o, uq, where β τ is a step size, and quantity ∇q t px, o, uq denotes the gradient of q t at px, o, uq w.r.t. some parameter θ t . Using tabular representations (e.g., finite/small M ), θ t " q t and thus ∇q t px, o, uq is a unit vector e x,o,u whose value at px, o, uq is one and zero otherwise. Using linear function approximations (e.g., continuous/large M ), q t px, o, uq . " φ t px, o, uq J θ t , where ∇q t px, o, uq " φ t px, o, uq is the feature vector at px, o, uq. Algorithm 1 shows the pseudocode of oSARSA.

Algorithm 1 The oSARSA Algorithm Initialize ḡ " ´8, ρ and q 0: ´1 arbitrary, and D ρ. while q 0: ´1 has not converged do Select -greedily ρ w.r.t. q 0: ´1 and D ρ.

Compose D ρ with N trajectories tξ rτ s u N τ "1 . Estimate pg, ςq from r ř ´1 t"0 Rt |D ρ , ŝ0 " s 0 s. If g ´ς ě ḡ then pρ, ḡ, D ρq " pρ, g `ς, D ρ q. Update α-vectors q 0: ´1 as described in ( 12). end while

To establish the convergence of oSARSA, we introduce the following assumptions.

Theorem 3. Consider assumptions: (1) The stepsizes tβ τ u τ "1,2,... satisfy Robbins & Monro's conditions; (2) The occupancy states ŝ0: ´1 and immediate returns R0: ´1 are accurately estimated; and (3) Every pair of reachable occupancy state and joint decision rule is visited infinitely often. Under these assumptions, the sequence q rτ s 0: ´1 generated by oSARSA converges with probability 1 to q 0: ´1.

Proof. Under these assumptions, we define H ρ that maps a sequence of α-vectors q 0: ´1 to a new sequence of α-vectors H ρ q 0: ´1 according to the formula: for all hidden state x, joint history o and control u, at control interval t, pH ρ q 0: ´1qpx, o, uq " rpx, uq `λ1 Etv t`1 py, o ' pu, zqqu, where v t px, oq . " q t px, o, ρpoqq and ρpoq is the control prescribed by ρ at joint history o. Then, the plan evaluation step of the oSARSA algorithm is of the form q rτ `1s t px, o, uq " p1 ´βt qq 12), we converge with probability 1 to q ρ 0: ´1. It now remains to be verified that the plan improvement step of the oSARSA algorithm changes the current plan for an improved one. Initially, ḡ is arbitrarily bad, so any new plan is an improved one. Then, ḡ " Jpρq for the current best plan ρ since occupancy state and return are accurately estimated. Hence, when ever g ě ḡ, we know that the new plan ρ yields a performance measure Jpρq superior to Jpρq, thus ρ improves ρ. We conclude the proof noticing that in finite M , the number of deterministic plans is finite. As a consequence, by visiting infinitely often every pair of occupancy state and decision rule we are guaranteed to visit all deterministic plans, hence an optimal one.

It is now important to observe that we meet assumption (2) in Theorem 3 only when M is available. Otherwise, we rely on confidence bounds rg ´ς, g `ςs, e.g. Hoeffding's inequality, on estimate g « Jpρq. In particular, we use lowerbounds g ´ς on sample means instead of the sample means g themselves, to limit situations where g is overestimated. Small data sets often lead to suboptimal solutions, but as the number of experiences in data set D ρ increases, sample means and corresponding lower bounds get close to the mean, i.e., ς tends to 0. We require an accurate estimation of a plan's performance to know for sure its performance is above that of any other plans we may encounter. However, an estimation of a sample plan's performance can be refined over time until it becomes accurate. For example, if the algorithm samples a promising plan-i.e., its confidence bounds suggest it might achieve a better performance than that of the current plan-the algorithm can progressively refine it until it becomes accurate. Of course, having a good initial estimate can significantly speed up the convergence. In the extreme case, the initial estimate is the true value. It is also worth noticing that the memory complexity of the oS-ARSA algorithms is linear with the size of an α-vector, i.e., Θp|D ρ |q; and its time complexity is linear with the episodes.

Experiments

We ran the oSARSA algorithm on a Mac OSX machine with 3.8GHz Core i5 and 8GB of available RAM. We solved the MILPs using ILOG CPLEX Optimization Studio. We define features to use sequences of K last joint observations instead of joint histories, hence the dimension of the parameter vector θ is |X|p|U ||Z|q K for finite M . We evaluate our algorithm on multiple 2-agent benchmarks from the literature all available at masplan.org: Mabc, Recycling, Gridsmall, Grid3x3corners, Boxpushing, and Tiger. These are the largest and the most challenging benchmarks from the Dec-POMDP literature. For each of them, we compare our algorithm to the state-of-the-art algorithms based on either a complete or a generative model: FB-HSVI [START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF], RLaR [START_REF] Kraemer | Multi-agent reinforcement learning as a rehearsal for decentralized planning[END_REF], and MCEM [START_REF] Wu | Monte-Carlo Expectation Maximization for Decentralized POMDPs[END_REF]. We also reported results of the state-of-the-art model-free solver: (distributed) REINFORCE [START_REF] Peshkin | Learning to Cooperate via Policy Search[END_REF]. For REINFORCE and oSARSA, we used hyper-parameters and β ranging from 1 to 10 ´3 with a decaying factor of 10 4 , sample size |D| " 10 4 . We use maximum episodes and time limit 10 5 and 5 hours, respectively, as our stopping criteria. Surprisingly, REINFORCE performs very well on domains that consist of weakly coupled agents, see Figure 1. However, for domains with strongly coupled agents, e.g., Tiger or BoxPushing, it often gets stuck at some local optima. In contrast, oSARSA converges to near-optimal solutions when enough resources are available over all domains, see Figure 1 and Table 1. Regarding the most challenging benchmarks, which require more resources, oSARSA stops before the convergence to a near-optimal solution; yet, it often outperforms the other RL algorithms. RLaR can achieve near-optimal result for small domains and short planning horizon ( ď 5q, assuming there exists a unique optimal plan. As for MCEM, it can solve infinite horizon problems, but similarly to REINFORCE may get stuck in local optima; this is essentially as they both use a form of gradient descent in a parametrized policy space. Table 1. Comparing V ρ ps0q of all solvers when available, where the "-" sign mean "out of memory" and/or "out of time".

Figure 1. Comparing V ρ ps0q of solvers with " 8 and λ " 0.9, where x-axis denotes the number of episodes during training.

Discussion

This paper extends a recent but growing (deep) MARL paradigm [START_REF] Szer | A Heuristic Search Algorithm for Solving Decentralized POMDPs[END_REF][START_REF] Dibangoye | Optimally Solving Dec-POMDPs as Continuous-State MDPs[END_REF][START_REF] Kraemer | Multi-agent reinforcement learning as a rehearsal for decentralized planning[END_REF][START_REF] Mordatch | Emergence of Grounded Compositional Language in Multi-Agent Populations[END_REF][START_REF] Foerster | Counterfactual Multi-Agent Policy Gradients[END_REF], namely RL for decentralized control, from modelbased to model-free settings. This paradigm allows a centralized algorithm to learn on behalf of all agents how to select an optimal joint decision rule to be executed at each control interval based on all data available about the system during a learning phase, while still preserving ability for each agent to act based solely on its private histories at the execution phase. In particular, we introduced tabular and approximate oSARSA algorithms, which demonstrated promising results often outperforming state-of-the-art MARL approaches for Dec-POMDPs. To do so, oSARSA learns a value function that maps pairs of occupancy state and joint decision rule to reals. To ease the generalization in such high-dimensional continuous spaces, we restrict attention to plans rather than policies, which in turn restricts value functions of interest to linear functions. To speed up the greedy maximization, we used a MILP for finite settings-we shall use a gradient approach instead of a MILP for continuous settings in future works. Finally, we present a proof of optimality for a MARL algorithm when the estimation error is neglected. We shall investigate an approach to relax this somewhat restrictive assumption, perhaps within the probably approximately correct learning framework.

The RL for decentralized control paradigm is significantly different from the standard RL paradigm, in which agents have the same amount of information during both the learning and the execution phases. Another major difference lies in the fact that learned value functions in standard (deep) RL algorithms are mapping from histories (or states) to reals. In contrast, oSARSA learns a value function that maps occupancy-state/decision-rule pairs to reals-spaces of occupancy states and joint decision rules are multiple orders of magnitude larger than history or state spaces. As a consequence, standard (MA)RL methods, e.g. REINFORCE and MCEM, and recent actor-critic methods [START_REF] Bono | On the Study of Cooperative Multi-Agent Policy Gradient[END_REF], may converge towards a local optimum faster than oSARSA, but the latter often converges towards a nearoptimal solution. oSARSA uses occupancy states instead of joint histories mainly because occupancy states are (so far minimal) sufficient statistics for optimal decision-making in Dec-POMDPs-using joint histories instead of occupancy states may lead to suboptimal solutions except in quite restrictive settings. For example, RLaR learns value functions mapping history/action pairs to reals, but convergence towards an optimal solution is guaranteed only for domains that admit a unique optimal joint plan-which essentially restricts to POMDPs [START_REF] Kraemer | Multi-agent reinforcement learning as a rehearsal for decentralized planning[END_REF].

  t. the current Q-value function Q ρ t :

		ât	. " arg max at : a 1 t PA 1 t ,...,a n t PA n t Q ρ t ps t , a t q,
	where	ρ . " â0: ´1.

Note that one should keep hidden states when available since they often speed up the convergence.


Hana Mkaouar
email: hana.mkaouar@redcad.org

Bechir Zalila
email: bechir.zalila@enis.tn

Jérôme Hugues
email: jerome.hugues@isae.fr

Mohamed Jmaiel
email: mohamed.jmaiel@enis.rnu.tn

An Ocarina Extension for AADL Formal Semantics Generation

Keywords: Real-time systems, model transformation, formal verification, AADL

The formal verification has become a recommended practice in safety-critical software engineering. The hand-written of the formal specification requires a formal expertise and may become complex especially with large systems. In such context, the automatic generation of the formal specification seems helpful and rewarding, particularly for reused and generic mapping such as hardware representations and real-time features. In this paper, we aim to formally verify real-time systems designed by AADL language. We propose an extension AADL2LNT of the Ocarina tool suite allowing the automatic generation of an LNT specification to draw a gateway for the CADP formal analysis toolbox. This work is illustrated with the Pacemaker case study.

INTRODUCTION

The verification of real-time systems is a challenging topic, especially when they are used in safety-critical domains where one failure can result in serious damages. Recently, formal methods have become one of the advocated techniques in safety-critical software engineering. To be formally verified, the system should be firstly specified with a specific formalism and so it can be explored with analysis tools. However, the hand-written of the formal specification requires a formal expertise and may become complex and tedious task especially with large systems. Therefore, it is helpful to provide an automatic generation of the formal specification to assist designers in system verification. For the same purposes, systems designed with architectural languages such as AADL, MARTE and SysML are transformed into other formalisms like Petri nets, automata and process algebras, in order to draw gateways for verification tools.

In this context, we aim at the automation of the formal verification of systems modeled with AADL [START_REF]AS5506A:SAE Architecture Analysis & Design Language (AADL) Ver 2[END_REF] (Architecture Analysis & Design Language). AADL is an industrial standard 1 language for embedded and real-time system modeling. Many projects and tool-chains are dedicated to AADL processing, that often adopt model transformation techniques to allow formal analyses. Several AADL formal semantics are defined using different formalisms such as Petri nets [START_REF] Renault | From AADL architectural models to Petri Nets: Checking model viability[END_REF][START_REF] A E Rugina | The ADAPT Tool: From AADL Architectural Models to Stochastic Petri Nets through Model Transformation[END_REF], timed automata [START_REF] Hamdane | From AADL to Timed Automaton-A Verification Approach[END_REF][START_REF] Johnsen | Automated Verification of AADL-Specifications Using UPPAAL[END_REF] and different process algebras [START_REF] Berthomieu | Formal verification of AADL specifications in the Topcased environment[END_REF][START_REF] Besnard | Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony[END_REF][START_REF] Chkouri | Translating AADL into BIP-application to the verification of real-time systems[END_REF][START_REF] P C Ölveczky | Formal semantics and analysis of behavioral AADL models in Real-Time Maude[END_REF][START_REF] Yang | Two Formal Semantics of a Subset of the AADL[END_REF]. These approaches are implemented within platforms such as OSATE and TOPCASED aiming the convenient reuse of existing tools like UPPAAL, Tina and Polychrony. In our work, we choose Ocarina [START_REF] Lasnier | Ocarina: An environment for AADL models analysis and automatic code generation for high integrity applications[END_REF], a tool suite that gathers analysis of AADL models and the automatic code generation towards AADL runtimes PolyORB-HI/Ada or C. We define a model transformation AADL2LNT implemented within Ocarina to automatically generate a formal specification from the AADL model using the LNT [START_REF] Champelovier | Reference manual of the LNT to LOTOS translator (version 6.5)[END_REF] language. LNT2 is a process algebra based on two standards Lotos and E-Lotos. This language provides a simplified and user-friendly syntax with expressive operators for data and behavior, suitable for the mapping of complex real-time features (tasks, scheduling algorithm, etc). Moreover, we aim to provide an automatic verification based on model-checking of a set of generic properties with the CADP 3 [START_REF] Garavel | CADP 2011: a toolbox for the construction and analysis of distributed processes[END_REF] (Construction & Analysis of Distributed Processes) toolbox. CADP is a well experimented tool for formal analysis which supports LNT as input language and offers diverse formal techniques like model-checking and simulation.

This paper describes the LNT semantic definition for an AADL model and how its generation and verification are automated using Ocarina and CADP. The remainder of this article is organized as follows: section 2 presents AADL and LNT languages; section 3 gives an overview of the AADL2LNT transformation; we describe Ocarina extensions in Section 4; section 5 illustrates our work with the Pacemaker case study; a brief related work is discussed in Section 6; and finally, a conclusion ends the paper in Section 7.

BACKGROUND

Briefly, we describe the considered subset of AADL language and we present the LNT language (more details can be found in [START_REF] Mkaouar | From AADL Model to LNT Specification[END_REF]).

AADL subset

An AADL model describes a system as a hierarchy of components with their interfaces and their interconnections. AADL components are grouped in three categories: software components (data, subprogram, subprogram group, thread, thread group and process); hardware components (processor, bus, virtual processor, virtual bus, device and memory); and the system component. AADL is known by its extensibility, the model can be completed with additional information through properties and annexes. Properties are attached in AADL elements to complete their definitions and bind hierarchically the whole system. Annexes present specific additions, specified with separate syntax, like the Behavior annex [START_REF]SAE Architecture Analysis & Design Language[END_REF] (BA) for behavioral description.

In our work, the AADL model is viewed as a set of concurrent real-time tasks scheduled by a uniprocessor and asynchronously interacted. Generally described, we consider the following components: data, thread, process, processor and device. These components are connected through AADL port connections, enriched by the Behavior annex, completed with a set of standard properties and finally grouped in the system component.

The thread component is a schedulable unit that can be executed concurrently with other threads. It is declared within a process component (represents its virtual address space) and scheduled by the processor (bound with Actual_Processor_Binding property). threads can declare ports that are directional (in, out or in out). They are typed with a data component and they may be declared data, event or event data ports. The port connections are explicitly declared between two ports, allowing the transfer of data/event between two components. In addition, threads can be completed with the Behavior annex. A Behavior_Specification clause is included within the thread component to specify its behavior as a state-transition system guards and actions.

Note that, in our transformation, a set of temporal and queuing properties should be attributed with these possible values: Sched-uling_Protocol (RMS, EDF); Dispatch_Protocol (periodic, sporadic, timed); Period; Compute_Execution_Time; Queue_Processing_Protocol (FIFO, LIFO); Overflow_Handling_Protocol (drop oldest, drop newest); and Queue_Size.

LNT language

An LNT specification represents a system by a set of concurrent processes communicating through channels. The specification distinguishes two parts: a data part defines types and functions; and a control part defines the behavior (process). The control part includes all data part instructions and adds instructions for behavior like asynchronous parallelism and communications.

An LNT specification, typically, consists of a set of LNT modules (in separate source files *.lnt) composed of a set of definitions. These definitions may include types, functions, channels and processes using different LNT operators such as variable declaration statement var, loops statement loop, non-deterministic choice select, parallel composition statement par and communication. A particular root process named MAIN should be added to define an entry point of the whole specification.

The LNT specification represents an executable semantic in which all parallel processes start execution and terminate at the same time with the possibility of synchronization. The LNT process is an object describing a behavior. To be synchronized with other processes, the process should declare a set of gates. The communication is ensured through gates typed with channels (gate profiles). The same gate allows sending and receiving messages with a rendezvous that blocks the sender until the reception.

OVERVIEW OF THE TRANSFORMATION

The AADL2LNT transformation is described with a set of corresponding rules between AADL and LNT in a way to obtain a modular LNT specification: every AADL component is transformed and encapsulated into an LNT process. According to component categories, we define a set of LNT generic skeletons as shown in Figure 1 given a global view of the transformation: SCHEDULER process implements the processor scheduling protocol; THREAD process represents the thread component with its supported features, subcomponents and behavior specification; and DEVICE maps the device component. In addition, the AADL port connection is mapped with an auxiliary process CONNECTOR using to specify queuing properties and ensure the asynchronism of communications. Finally, all processes are composed and synchronized through LNT gates to form the whole system in the Main process.

The AADL2LNT transformation can be represented at three levels, allowing the mapping of different kind of AADL models: the scheduling mapping ensures the transformation of models with independent threads (no port connections); the communication mapping completes the mapping by considering port connections between threads and devices; finally, the thread component may be enriched with behavioral descriptions using BA which is transformed at the behavioral mapping level. In the rest of this section, we briefly explain each mapping level.

Scheduling mapping

At this level, we consider only thread and processor components mapped respectively to THREAD and SCHEDULER processes.

Processor mapping.

The AADL processor is a hardware component that ensures the scheduling and execution of threads. The SCHEDULER process represents the processor component by implementing its scheduling algorithm. This process plays a crucial role in the LNT specification, it encapsulates all temporal calculations ensuring the activation of threads according to their dispatch protocol. As shown in Figure 1, SCHEDULER and THREADs are connected by ACTIVATION gates. This synchronization allows the SCHEDULER to activate THREADs using a set of activation orders. Thanks to its programming ability, many scheduling algorithms may be implemented within the SCHEDULER process using the LNT language: preemptive/non-preemptive scheduling and fixed/unfixed based-priority scheduling. For example, the RM (Rate Monotonic) scheduler is based on the preemptive fixed-priority Generally described, the SCHEDULER process consists mainly of two parts as shown Figure 2: INITIALIZATION and OPERATIONAL. To schedule the threads execution, the SCHEDULER requires the set of threads with their temporal parameters which is included in the INITIALIZATION PART using an LNT array (THREAD_ARRAY). These information are extracted, at generation, from the AADL model (attributed by different temporal properties). The OPERATIONAL PART is the main part of the SCHEDULER ensuring the execution by applying the scheduling algorithm. The THREAD_ARRAY is visited to select the appropriate thread for execution. The selected thread is handled (allocate its execution time, update its state, prepare its activation order) to send an activation order with its corresponding ACTIVATION gate.

T _ C h a n n e l _ D i s p a t c h ] i s loop s e l e c t ACTIVATION ( T _ D i s p a t c h _ C o m p l e t i o n ) [ ] ACTIVATION ( T _ D i s p a t c h _ P r e e m p t i o n ) [ ] ACTIVATION ( T _ P r e e m p t i o n ) [ ] ACTIVATION ( T _ P r e e m p t i o n _ C o m p l e t i o n ) . . . end s e l e c t end loop end p r o c e s s

The THREAD process is dispatched according to the corresponding Dispatch_Protocol property. We support periodic, sporadic and timed dispatch models as follows:

• periodic threads are periodically dispatched, at every period (the specified Period property value). • sporadic threads have no fixed first activation, they are activated in response to asynchronous events (invocationevents). The Period property value is considered as the minimal delay between two successive activations. • timed threads are periodically dispatched and may be also activated by invocation-events. The Period property value represents a time-out value ensuring that a dispatch occurs after a period if no events have arrived.

The THREAD processes are generically implemented for all dispatch protocols, while the SCHEDULER maintains that: periodic threads are activated with regular-orders; sporadic threads receive irregularorders according to invocation-events reception; and timed threads are periodically activated as long as there is no invocation-events. While scheduling, the THREAD may be in one of states defined by the standard thread scheduling and execution states automaton added in Figure 3. We consider the Ready state (the thread is able to be executed) and the Running state (the thread is actually executing) and we except awaiting states (shared resources, subprogram calls and background threads) which are not supported in our transformation. A Ready thread can be selected by the SCHEDULER, thus, it moves to the Running state. In addition, while running, the thread can be preempted and so it returns to the Ready state or it can complete its execution and becomes in the Awaiting dispatch which is a suspended state for threads when completing the execution. A thread in Awaiting dispatch state may become Ready by a temporal event (dispatch for a new period) or an invocation-event.

The ACTIVATION communication defines the THREAD states: the current state is defined according to the received SCHEDULER order. Initially, THREAD is supposed in the Ready state. It is suspended until the reception of a new activation order and then it moves to Running state. At this level, four alternatives can be presented:

• T_Dispatch_Complete: THREAD starts and completes the execution of the current period and enters in the Awaiting dispatch state; • T_Dispatch_Preemption: THREAD starts the execution in the current period but with a preemption, thus, it returns to the Ready state; • T_Preemption: THREAD progresses in execution without attaining the completion time, so it returns to the Ready state; • T_Preemption_Complete: THREAD finishes the execution of the current period and enters in the Awaiting dispatch state. After the execution, THREAD sends an T_Complete to the SCHEDULER meaning that THREAD has accomplished the activation order and it is no more in the Running state.

Communication mapping

This mapping concerns port connections between threads and devices. They are declared at process and system levels and typed with data components. AADL provides a rich semantics of AADL ports and their connections in all aspects (topologies, directions, timing, etc) that can not be totally considered in a single work. Thus, we consider these restrictions: only 1-1 connections; no in out ports; event data and event port are similarly handled at this level; inputs are frozen at the start time of execution; and outputs are transferred at the completion time.

In this mapping, we aim to draw thread connections without the consideration of data contents. We simply maps data/event into an enumeration type (AADLDATA label) exchanged between different THREAD through the corresponding channel as included in Listing 2.

Listing 2: data type and channel type LNT_Type_Data i s AADLDATA, EMPTY end type channel LNT_Channel_Port i s ( LNT_Type_Data ) end channel

In addition, the device components are supported since they can be connected with threads. devices are not mapped at the scheduling mapping level since they are not scheduled, also their internal behavior is not considered. So the device component is simply transformed into a DEVICE process as shown in Figure 1. Mainly, DEVICE declares a set of gates equivalent to the device ports and gathers corresponding communications in its behavior.

Port mapping.

The THREAD declaration is completed with the gate declarations corresponding to the thread port declarations as shown in Listing 3. Since we deal with LNT gates, which are bidirectional, in and out ports are similarly represented. Then, the corresponding communication is also added after the ACTIVATION communication. Connections between LNT processes are drawn through gate synchronizations: communications are effected with rendezvous points which block sender until the reception. In this case, the asynchronous aspect of thread connections cannot be presented directly with LNT gate synchronizations. Hence, we add an auxiliary process (CONNECTOR) synchronized between sender and receiver threads.

The CONNECTOR represents the AADL semantic port connection which includes all port connection declarations (at process and system levels) that follow the component containment hierarchy in the instantiated system from a source thread to a destination thread. Thus, all port connection declarations are abstracted in the CONNECTOR synchronizations: connections ❶, ❷ and ❸ of Figure 1 are similarly transformed into CONNECTOR instances.

At THREAD level, communications are also controlled through SCHEDULER orders that fix input and output times:

• T_Dispatch_*: THREAD receives inputs at the start time;

• T_*_Complete: THREAD sends outputs the completion time.

The port type and the thread Dispatch_Protocol property allow the definition of three CONNECTOR types as shown in Listing 4. In the case of data port connections and periodic threads, a simple DATA_CONNECTOR is used without buffers. It keeps the data until the next reception, each time a new data is received, the last one is overwritten. When exchanging events, we use EVENT_CONNECTORs including a list of inputs with a definite size (Queue_Size parameter). Event buffers implement the set of queuing properties such as Queue_Processing_Protocol and Dequeue_Protocol. Since we support sporadic and timed threads, the SCHEDULER needs to be notified for every new incoming invocation-event: sporadic threads are ignored by the SCHEDULER until the reception of an invocation-event; also timed threads may be activated by invocation-events. So we add NOTIFICATION gates to synchronize EVENT_CONNECTORs with the SCHEDULER as shown in Figure 1. Thus, when receiving a new event, the EVENT_CONNECTOR notifies the SCHEDULER, to consider the concerned THREAD in scheduling.

Behavioral mapping

At this level, the AADL model is completed with behavioral descriptions using the Behavior annex. In our work, the BA is mainly supported to complete the thread component with behavior handling inputs and outputs in order to enrich the communication mechanism. The Listing 5 includes the Behavior_Specification which consists of: a variables section that allows the declaration of local variables used in descriptions within the scope of the Behavior_Specification clause; a states section allowing the declaration of the states of the behavior automaton that may be declared as initial, final or complete state; and a transitions section for the description of the behavior by linking states through guarded transitions (S i -[condition]->S j {actions}).

A behavior automaton starts from an initial state and terminates in a final state. A complete state, as defined in the BA standard [START_REF]SAE Architecture Analysis & Design Language[END_REF], acts as a suspend/resume state out of which threads are dispatched. The transitions specify behavior as a change of the current state from a source state S i to a destination state S j . A condition (dispatch or execution) determines whether a transition is taken and then the corresponding actions are performed. The dispatch condition (on dispatch) means that the thread controls its state when it is dispatched periodically or when satisfying the dispatch_trigger_condition which is a boolean expression describing a logical combination of triggering events (the arrival of events on ports). The execution condition signifies that the transition is guarded by a logical expressions based on input values. Periodic threads are always considered to be unconditionally handled by dispatch conditions without the dispatch_trigger_condition. In the case of sporadic or timed threads, invocation-events can be used in the expression of dispatch_trigger_condition, which refines the AADL dispatch model by defining different behaviors for each input when several event ports are declared.

Listing 5: Behavior_Specification

annex B e h a v i o r _ s p e c i f i c a t i o n { * * v a r i a b l e s V 1 : T 1 ; . . . Vm : Tm ; s t a t e s S 0 : i n i t i a l s t a t e ; S i , S j : c o m p l e t e s t a t e ; S l : s t a t e ;

Sn : f i n a l s t a t e ; t r a n s i t i o n s

S 0 -[on d i s p a t c h d i s p a t c h _ t r i g g e r _ c o n d i t i o n ] -> S i ; S i -[ e x e c u t i o n _ c o n d i t i o n ]-> S j { --a c t i o n s } ; * * } ;
3.3.1 Data mapping. In previous levels, data components were generically mapped into an enumeration type: the consideration of the data contents was useless since they are not handled in the component behavior. Now, inputs and outputs can be used in the BA description and port contents may be exploited in calculations. Thus, the data abstraction should be overridden and the data type should be considered while transformation. Currently, we deal with basic data types: each type from the AADL standard Base_Types package is mapped into a suitable LNT type. In addition, port types are now differently considered: we define for each data, event or event data port a separate LNT channel (Listing 6). The Bool type is used to map event (the true value marks a new incoming event). Due to the lack of space, we describe briefly this mapping level which needs to be well detailed in a further publications. The general idea consists of completing the THREAD with BA transitions mapping in order to embed the behavior automaton within its state automata: in the Running state, the THREAD may move in one of complete states of the behavior automaton.

As shown in the example of Listing 7, the set of local variables (V 1 , .., V m ) are added in the THREAD process using the var statement, they are declared with the same name and the suitable type. All states are added using an enumeration type.

The current state of the behavior automata is explicitly mapped within the THREAD process using a variable STATE. The transitions are specified using the LNT conditional statement (if ((STATE==S i ) and (conditions)) then .. end if), in which, we assign the STATE variable with the new state (STATE:=S j ;) and we include the corresponding actions. For illustration, we give the THREAD_T in Listing 7 whose behavior corresponds to the transition S0-[A < 5]-> S1 {V1 :=A+1;}. The on dispatch conditions are assumed implicitly since we include the BA mapping after the ACTIVATION communication and so every new dispatch the THREAD controls its state. The execution conditions or the dispatch_trigger_condition of dispatch conditions are easily added on the LNT if condition of the corresponding transition using logical disjunction and conjunction LNT operators. Since we use LNT Bool type to specify events, the dispatch_trigger_condition is satisfied when its logical expression becomes true (new incoming event).

The actions associated with transitions consist of control structures (action sequences, conditionals, finite loops, etc). In our work, basic actions are considered, that may be an assignment action or a communication action. These actions are transformed in the LNT language using the suitable LNT statement such as assignments and gate communications.

IMPLEMENTATION

Ocarina 4 [START_REF] Lasnier | Ocarina: An environment for AADL models analysis and automatic code generation for high integrity applications[END_REF] is an open source compiler developed since 2004 and recently deployed on GitHub under the OpenAADL project. The Ocarina compiler is designed with a modular architecture. Analyses and generations are handled using ASTs (Abstract Syntax Tree) which are the internal representation of models (AADL, annexes and other languages). Based on the grammar rules, the model is decomposed into a set nodes hierarchically connected to create the corresponding syntax tree. These ASTs are manipulated in three distinguished parts as follows.

• The Central library part consists of a set of routines (node builder and finder) allowing the AST construction and manipulation of the AADL models and other languages. The frontend ASTs are expanded and used for model/code generation. Each generation has its specific modules that implement transformation rules to produce code source files of the target language. In our work, we extend the compiler with a set of modules in its different parts to support the behavior annex and the AADL2LNT transformation. Briefly, the Central library is enriched with the required routines for both BA and LNT ASTs based respectively on BA [START_REF]SAE Architecture Analysis & Design Language[END_REF] and LNT [START_REF] Champelovier | Reference manual of the LNT to LOTOS translator (version 6.5)[END_REF] grammars. A set of analysis modules is added in the Frontend to handle Behavior_specification clauses. For each clause, a BA AST is created and hierarchically constructed at the syntax analysis phase. Then, it is attached to the corresponding AADL component. Thus, the AADL AST is completed with BA ASTs to obtain a final AADL-BA AST. Finally, the AADL2LNT transformation is implemented in the Backend to produce LNT files. In the following, we detail the LNT generation and the obtained tool-chain for AADL model analysis.

LNT code generation

The AADL2LNT is applied on an instantiable AADL system, means that the model is successfully analyzed lexically, syntactically, semantically and can be completely bound (all components are bounded such as, all threads are bound to the processor). In addition, a set of standard properties should be attributed (scheduling and queuing properties indicated in section 2.1), otherwise, an error or warning message is displayed. Thus, the AADL AST is created and instantiated to become ready for the LNT generation. Note that depending on AADL model kind, the appropriate transformation level is applied. The non-supported elements (e.g. bus, shared access) are automatically ignored. And when using Behavior annex, the transformation is applied on the complete AADL-BA AST.

Model transformation.

Following Ocarina Backend architecture, the AADL2LNT rules are applied on the AADL AST to simultaneously build the LNT AST. Then, the LNT AST is scanned by the LNT code printer in order to produce code source files 4 https://github.com/OpenAADL/ocarina (*.lnt). To obtain a modular specification, we generate a set of LNT modules which corresponds to the construction of a set of LNT LTSs. Two main modules, *_Types and *_Main, are always generated for all LNT specifications. Then, according to mapping level, a set of LNT modules is added as follows:

• *_Threads module consists of a set of THREAD and DEVICE declarations, whose generation depends mainly on port declarations in thread or device components. • *_Processor module contains the SCHEDULER process with a set of LNT function definitions required for scheduling and execution. The SCHEDULER generation needs the extraction and the calculation of a set of thread information to be included in its INITIALIZATION PART: the THREAD_ARRAY generation requires the number of thread instances and the set of values of each thread properties. • Port_Connections and Port_Connections_BA are generic modules included in the compiler resources. Each module consists of a set of CONNECTOR declarations that will be instantiated for each port connection.

All declared processes in different modules should be instantiated and synchronized to form the whole system in the Main process which requires the generation of two modules:

• *_Types module consists of a set of LNT types and channels required for different synchronizations: THREAD/CONNECTOR, CONNECTOR/SCHEDULER and THREAD/SCHEDULER. • *_Main module contains the Main process whose generation can be resumed in three steps: (1) preparation of the list of thread instances;

(2) synchronization of CONNECTOR processes: for each port connection, we create one CONNECTOR instance which is synchronized between THREADs equivalent to the source in port and the destination out port threads; (3) global composition: all THREADs are synchronized with the SCHEDULER on ACTIVATION gates, all CONNECTORs are synchronized with the SCHEDULER on NOTIFICATION gates.

To provide a traceable transformation, a set of naming rules is applied while generation. At the THREAD level, all AADL port identifiers are conserved and prefixed by "PORT_". Also, all port content variable, BA variable and state identifiers are conserved while the behavioral mapping. At the Main level, the generation conserves AADL component identifiers as follows: the thread identifier is prefixed by "THREAD_"; the device identifier is prefixed by "DEVICE_"; for each AADL connection, two identifiers are prepared (the connection name is prefixed by "SEND_" and "RECEIVE_") to present two gates for the THREAD/CONNECTOR synchronization. 4.1.2 SVL script. In addition to LNT modules, a second input is necessary for analysis with CADP toolbox. A script file (demo.svl) containing a set of operations with SVL (Script Verification Language) [START_REF] Garavel | SVL: a scripting language for compositional verification[END_REF] is constructed to orchestrate the verification. This file is generated directly for each AADL system (without an SVL AST) containing two parts: compilation of the LNT specification and a set of generic properties for verification by model-checking (deadlock, schedulability, data loss, buffer overflow). The model-checking technique consists of checking if a model satisfies a given property specified with temporal logic. In our work, properties are specified by the SVL property statement, that embeds the temporal logic verification statement, and checked with the CADP Evaluator model-checkers [START_REF] Mateescu | Efficient on-the-fly model-checking for Regular Alternation-free mu-Calculus[END_REF][START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF].

Tool-chain

The AADL2LNT transformation allows the definition of a toolchain, depicted in Figure 4, using Ocarina for architectural modeling and CADP for formal verification. The provided tool-chain ensures a transparent model transformation and verification. The transformation is proceeded using Ocarina command line, then, the generated SVL script is simply invoked to begin model analysis. Initially, the LNT specification is transformed into an LTS (Labeled transition system), to be exploited by verification tools. Then, the system is automatically checked by a set of generic properties, and it can be simulated with CADP simulators like OCIS [START_REF] Garavel | Open/Caesar: An open software architecture for verification, simulation, and testing[END_REF].

The analysis results help designers in model correction and improvement (validation of temporal parameters, deadlock detection, schedulability test, detection of connection failures, etc). This verification may be iteratively applied after each model modification until the generation of the final application. Moreover, the obtained specification can be considered as a good base of a manual verification. Designers, with formal expertise, may complete different LNT modules and verify new properties for a specific case study.

CASE STUDY

The current Ocarina version covers almost the BA frontend analysis and the generation of the scheduling and communication mapping, while for the behavioral mapping, further work needs to be completed to include the BA mapping within the THREAD skeleton. In this section, we report experiments performed on the Pacemaker case study. The Pacemaker is a medical device inserted in the body of a patient, to regulate his/her heart beating with electrical impulses. It is used in the case of heart rhythm problems (inability to maintain a normal heart rate). Depending on the heart problem, the Pacemaker provides different modes that perform different kinds of therapeutic behavior. In this paper, we consider the VVI mode which is the heart ventricle-chamber pacing mode.

Ocarina: modeling and generation

AADL modeling. The Pacemaker AADL model5 [START_REF] B R Larson | Formal semantics for the pacemaker system specification[END_REF] is depicted in Figure 5. Structurally speaking, the AADL system consists of two main parts: the pulse generator (PacemakerSW process) which embeds the software implementing the therapeutic behavior to monitor leads (Lead device) for ventricle-chamber. The pulse generator is connected with leads through event ports to sense the heart beating (sense in port) and send an order for pacing (pace out port). The VVI therapeutic mode is accomplished using three threads interconnected and enriched with BA specifications: a sporadic thread to present the VVI mode (thread VVIMode); and two timed threads (VRPTimeout/LRLTimeout) representing timers. These threads are collaborated to maintain the rate of pacing as follows: when the heart has no beat during an LRL period, VVIMode causes a pace (an event on pace port); if the sense (events on sense port) comes too soon after a beat (during the VRL period), it will be ignored; and when the heart is beating regularly, VVIMode detects a normal beating rhythm (an event on normal port). This behavior is mainly described within the VVIMode thread Behavior_Specification included in Listing 8. LNT generation. The Pacemaker LNT specification with its SVL script are generated by the AADL2LNT extension. In Listing 9, we include an extract from the obtained process THREAD_VVIMode equivalent to the VVIMode thread. The process gathers mainly the set of the equivalent declarations (gates and variables), the set of the required initializations and the BA code inserted after the ACTIVATION communication. The Table 1 resumes the Pacemaker transformation metrics. The obtained specification counts 765 lines, whose 75% is automatically generated by the current Ocarina version. This generation covers an important part of AADL2LNT transformation and eliminates the complexity of its rules. Particularly, the Main mapping seems tricky since we should compose a lot of process instances through an important number of gates: the Pacemaker Main process counts 12 instances synchronized on 23 different gates. The obtained specification complexity depends directly of threads/connections type and number: from models with independent threads, we obtain simple LNT models without CONNECTOR instances. While with highly connected models, especially for sporadic or timed threads, the process number increases significantly. Despite this fact, the obtained specifications still comprehensible and the correspondence between the AADL/BA syntax and the LNT code can be easily identified thanks to the applied naming rules (section 4.1.1).

CADP: formal analysis and evaluation

LTS generation. The obtained LNT specification is ready for CADP analysis. The demo.svl script allows the use of CADP tools for LTS generation and model-checking of a set of properties. The LTS represents the state space of the obtained LNT specification, characterized by a number of states and transitions. In the formal context, a well known problem is the state space explosion, when the number of states or transitions explodes. For this reason, the definition of the AADL2LNT transformation was refined several times (since the first proposition [START_REF] Mkaouar | From AADL Model to LNT Specification[END_REF]) to obtain the smallest state spaces. The Pacemaker LTS counts 5473 states and 5473 transitions which present a small state space compared to the considered AADL model with sporadic/timed threads, event port connections and BA descriptions. We note that with independent or only-periodic thread models, we obtain much smaller spaces. In more advanced experiments, we test excessively models with connected sporadic/periodic threads. We note that AADL models can reach 40 threads without space explosion problem (state spaces are about 900 states for models without BA descriptions).

Model-checking. After the LTS generation, we can move to modelcheck the set of generated properties. For illustration, Listing 10 presents the Connection property that assumes that every connection is well established: for each event sent, there is an inevitably reception. As shown in Listing 10, SVL property statements can be parameterized. Parameters are used to present connections and threads, so properties are separately applied on each thread/port connection. Thus, we obtain understandable results and the AADL model problems can be rapidly localized. For example, the Connection property is checked for each connection (the model-checker displays a true/false response): the Listing 11 presents the result of the verification of the inter-thread connection CNX_3 from the Pacemaker AADL model. More analysis. The Pacemaker model was successfully analyzed with different generated properties. In addition, advanced analysis was applied to verify the VVI therapeutic behavior of the pulse generator. As illustration, the normal rhythm detection can be checked as follows: the DEVICE_Lead is completed to be synchronized with the SCHEDULER, and so it can be periodically dispatched to send events at a normal heart rate on the ventricle_sense port; and a new SVL property (Listing 12) is added to check if the VVIMode thread sends events on the normal port without any pacing event.

Listing 12: Normal_Rhythm SVL property property Normal_Rhythm i s " Main . bcg " | = with e v a l u a t o r 3 NEVER ( " PACEMAKERSW_PACE__LEAD_VENTRICLE_PACE ! TRUE " ) and [ t r u e * . " SEND_PACEMAKERSW_NORMAL__LEAD_NORMAL ! TRUE " ] t r u e ; expected TRUE ; end property ;

RELATED WORK

The AADL language is supported by several tools, either opensource (OSATE, Ocarina, TOPCASED) or commercial (STOOD, AADL Inspector). In our work, we contribute on Ocarina opensource tool suite that can be used as stand-alone compiler since it provides different engineering steps (modeling, analysis and code generation) with the possibility of the use of extra tools like Cheddar and Bound-T. In addition, Ocarina can be easily integrated as a backend for other AADL editors (already used through OSATE and AADL Inspector tools), which increases the visibility of our work. AADL Formal approaches are often based on model transformation into different languages such as Lustre [START_REF] Jahier | Virtual execution of AADL models via a translation into synchronous programs[END_REF], TLA+ [START_REF] Rolland | Modes in asynchronous systems[END_REF], Signal [START_REF] Besnard | Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony[END_REF], ACSR [START_REF] Sokolsky | Schedulability analysis of AADL models[END_REF], TASM [START_REF] Yang | Two Formal Semantics of a Subset of the AADL[END_REF], Fiacre [START_REF] Berthomieu | Formal verification of AADL specifications in the Topcased environment[END_REF], Real-time Maude [START_REF] P C Ölveczky | Formal semantics and analysis of behavioral AADL models in Real-Time Maude[END_REF] and BIP [START_REF] Chkouri | Translating AADL into BIP-application to the verification of real-time systems[END_REF]. As examples: many work [START_REF] Besnard | Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony[END_REF][START_REF] Yu | Exploring system architectures in AADL via Polychrony and SynDEx[END_REF] are around the Polychrony platform and Signal language for synchronous verification of AADL models where behavior is specified by BA or Simulink. The transformations are implemented within OSATE and the analyses are performed by Polychrony and SynDEx tools; authors in [START_REF] Yang | Two Formal Semantics of a Subset of the AADL[END_REF] transform a synchronous AADL subset (periodic threads, data port connections, modes and BA) to the TASM language, in order to verify behavioral properties (deadlock and reachability) with TASM tool suite and UPPAAL; the transformation of AADL model into the Fiacre language is addressed in the TOPCASED environment [START_REF] Berthomieu | Formal verification of AADL specifications in the Topcased environment[END_REF]. This work supports periodic/sporadic thread and event/data port connections, but it is restricted to the non-preemptive scheduling. The AADL model needs a first transformation into Fiacre which is considered as a pivot language for other transformations for connection to Tina and CADP tools. This proposition is extended in [START_REF] Bodeveix | Towards a verified transformation from AADL to the formal component-based language FIACRE[END_REF] aiming the validation of the transformation for an AADL synchronous subset; authors in [START_REF] P C Ölveczky | Formal semantics and analysis of behavioral AADL models in Real-Time Maude[END_REF] use the Real time Maude language to transform an AADL subset with BA to be analyzed with the Real-Time Maude platform. This work is extended in [START_REF] Bae | Definition, semantics, and analysis of Multirate Synchronous AADL[END_REF] considering a defined Synchronous AADL sub-language.

Generally speaking, these transformations aim at the same objectives: the definition of an AADL executable formal semantics for model-checking of behavioral and temporal properties. Yet, they can be distinguished according to the considered AADL subset (synchronous subsets, non-preemptive scheduling, etc). We note also that most of these transformations is implemented as OSATE plugins and a majority requires more than one model transformation to be connected to the analysis tools. Comparing to these work, we provide a tool-chain that automatizes both generation and model-checking. We use a direct input language to CADP without additional transformations. We consider an important AADL subset that especially includes event-driven threads, asynchronous connections and preemptive scheduling. The considered subset covers fundamental real-time features that can be used in more realistic applications rather than synchronous and non-preemptive approaches.

Figure 1 :

 1 Figure 1: Overview of the AADL2LNT transformation

Figure 2 :

 2 Figure 2: SCHEDULER graphical skeleton

Listing 1 :

 1 THREAD LNT skeleton p r o c e s s THREAD_ * [ ACTIVATION : L N

Figure 3 :

 3 Figure3: AADL thread scheduling and execution states[START_REF]AS5506A:SAE Architecture Analysis & Design Language (AADL) Ver 2[END_REF]

Listing 3 :

 3 THREAD LNT skeleton p r o c e s s THREAD_ * [ ACTIVATION : LNT_Channel_Dispatch , PORT_ * : LNT_Channel_Port ] i s loop s e l e c t . . . [ ] . . . ACTIVATION ( T _ D i s p a t c h _ C o m p l e t i o n ) ; PORT_ * (AADLDATA) [ ] . . . end s e l e c t end loop end p r o c e s s 3.2.2 Connection mapping.

Listing 4 :

 4 Diffrent LNT CONNECTORs p r o c e s s DATA_CONNECTOR [ INPUT : LNT_Channel_Port , OUTPUT : LNT_Channel_Port ] p r o c e s s PERIODIC_EVENT_CONNECTOR [ INPUT : LNT_Channel_Port , OUTPUT : LNT_Channel_Port ] ( Q u e u e _ S i z e : Nat ) p r o c e s s EVENT_CONNECTOR [ INPUT : LNT_Channel_Port , OUTPUT : LNT_Channel_Port , NOTIFICATION : LNT_Channel_Event ] ( Q u e u e _ S i z e : Nat )

Listing 6 :

 6 data new type and channels channel L N T_ C h a n ne l _ D at a _ P o rt i s ( LNT_Type_Data ) end channel channel L N T _ C h a n n e l _ E v e n t _ P o r t i s ( B o o l ) end channel channel L N T _ C h a n n e l _ E v e n t _ D a t a _ P o r t i s ( LNT_Type_Data , B o o l ) end channel 3.3.2 Behavioral annex mapping.

Listing 7 :

 7 THREAD LNT skeleton p r o c e s s Thread_T [ ACTIVATION : LNT_Channel_Dispatch , PORT_A : LNT_Channel_Port ] i s -p o r t d e c l a r a t i o n var A : LNT_Type_Data , -p o r t v a r i a b l e V1 : LNT_Type_Data , . . . -b e h a v i o r v a r i a b l e STATE : LNT_Type_STATES -c u r r e n t s t a t e in STATE : = S0 ; A : = LNT_Type_Data ( 0 ) ; V1 : = LNT_Type_Data ( 0 ) ; loop s e l e c t ACTIVATION ( T _ D i s p a t c h _ C o m p l e t i o n ) ; PORT_A ( ? A ) ; -p o r t c o m m u n i c a t i o n i f ( STATE == S0 ) and ( A < 5 ) then STATE : = S1 ; V1 : = A + 1 end i f ; . . .

Figure 4 :

 4 Figure 4: Ocarina-CADP tool-chain

Figure 5 :

 5 Figure 5: AADL model of the Pacemaker case study

Listing 9 :

 9 An extract of the THREAD_VVIMode p r o c e s s THREAD_VVIMode [ ACTIVATION : LNT_Channel_Dispatch , PORT_SENSE : LNT_Channel_Event , . . , PORT_PACE : LNT_Channel_Event ] i s var STATE : LNT_Type_STATES , VRP : Nat , . . . in STATE : = S1 ; VRP_TIMEOUT : = f a l s e ; . . . loop ACTIVATION ( T _ D i s p a t c h _ C o m p l e t i o n ) ; PORT_SENSE ( ? SENSE ) ; PORT_LRL_TIMEOUT ( ? LRL_TIMEOUT ) ; PORT_VRP_TIMEOUT ( ? VRP_TIMEOUT ) ; i f ( STATE == S1 ) and ( VRP_TIMEOUT ) then STATE : = S1 ; VRP : = 0 e l s i f ( STATE == S1 ) and ( LRL_TIMEOUT ) then STATE : = S1 ; PORT_PACE ( t r u e ) ; PORT_P_OR_N_VRP ( t r u e ) ; PORT_P_OR_N_LRL ( t r u e ) ; VRP : = 1 . . . end i f ; . . .

Listing 10 :

 10 An extract of the Pacemaker SVL script --LTS g e n e r a t i o n " Main . bcg " = d i v b r a n c h i n g r e d u c t i o n of " PACEMAKER_Main . l n t " ; --P r o p e r t i e s f o r model-c h e c k i n g property C o n n e c t i o n ( ID ) " A f t e r a SNED a c t i o n , a RECEIVE i s e v e n t u a l l y r e a c h a b l e " i s " Main . bcg " | = with e v a l u a t o r 4 AFTER_1_INEVITABLE_2 ( SEND_$ID , RECEIVE_$ID ) ; expected TRUE ; end property ; check C o n n e c t i o n ( CNX_PACE ) ; check C o n n e c t i o n ( CNX_3 ) ; Listing 11: Analysis results from Pacemaker case study p r o p e r t y C o n n e c t i o n ( CNX_3 ) | A f t e r a SNED a c t i o n , a RECEIVE i s e v e n t u a l l y r e a c h a b l e PASS

  • The Frontend part ensures lexical, syntactic and semantic analyses of the AADL model. At this level an AADL AST is created, analyzed and then instantiated (decorated with information). Indeed, if the AADL model includes annexes, they are similarly handled with separate ASTs.• The Backend part provides different automatic generations.

Table 1 :

 1 Pacemaker metrics

		AADL	LNT	SVL
	Number of	lines 157	lines 765	lines 40
		element	process
		2 thread	2 THREAD
	Equivalence of	1 process 1 device	-1 DEVICE
		15 event connections	7 EVENT_CONNECTOR
		1 processor	1 SCHEDULER
		1 system	1 Main

AADL is standardized by SAE (Society of Automotive Engineers)

LNT is developed by the Vasy team from INRIA for safety-critical systems

CADP official web site: http://cadp.inria.fr/

This model is inspired from the pacemaker model published by Ellidiss technologies.

CONCLUSION AND FUTURE WORK

In this paper, we described the AADL2LNT Ocarina extension for AADL formal semantic generation in the context of software engineering of real-time systems. This work is based on the transformation of the AADL model into an LNT specification considering mainly scheduling execution and task communication which are indispensable features for a useful real-time analysis. In addition, we support the Behavior annex for more complete AADL models. We provide an automatic tool-chain for formal analysis of AADL models by CADP toolbox, through which the LNT specification is generated and then checked by a set of generic properties.

The current AADL2LNT version allows an important generation and we are working continuously on our implementations in Ocarina for a total automation. As future work, we aim to extend the scheduling mapping to support multi-core scheduling.