Meysam Hashemi
email: meysam.hashemi@inria.fr

Axel Hutt
email: axel.hutt@inria.fr

A thalamocortical feedback model to explain EEG during anesthesia

Keywords: General anesthesia, Thalamocortical model, EEG, Power spectrum

General anesthesia (GA) is a medical procedure which aims to achieve unconsciousness, analgesia, amnesia, and immobility. Although GA is commonly used in medical care for patients undergoing surgery, its precise underlying mechanisms and the molecular action of anesthetic agents (AA) remain to be elucidated. A wide variety of drugs are used in modern anesthetic practice and it has been observed that for many AAs, during the transition from consciousness to unconsciousness, the electroencephalogram shows biphasic effects in amplitude: an initial increase of the spectral power followed by a decrease at higher concentrations. Moreover during the administration of propofol, specific changes in EEG rhythms can be observed. The aim of this work is the extended discussion of a recent model by Hindriks and van Putten [8] that reproduces specific changes in EEG rhythms by the study of a neuronal population model of a single thalamocortical module. We illustrate specific features of the model, such as the physiological assumptions, the derivation of the power spectral density and the impact of the propofol concentration and of the stationary state. We show that the propofol-induced modification of the stationary state plays an important role in the understanding of the observed EEG.

Introduction

General anesthetics (GAs) include a large number of drugs which without them, modern medicine, especially surgery, would not have been possible. However, the mechanism underlying its anesthetic effects on human beings is not yet fully understood [START_REF] Alkire | Consciousness and anesthesia[END_REF].

It has been observed that during the transition from consciousness to unconsciousness, by induction thippental, propofol, and sevoflurane, many derived EEG variables show biphasic effects, that is an initial increase of the spectral power followed by a decrease at higher concentrations [START_REF] Kuizenga | Biphasiceegchanges inrelation to loss of consciousness during induction with thiopental, propofol, etomidate, midazolam or sevoflurane[END_REF]. Moreover, during the induction phase of propofol, enhanced oscillatory activity within several frequency bands can be observed [START_REF] Cimenser | Tracking brain states under general anesthesia by using global coherence analysis[END_REF]. For clinically relevant concentration of propofol specific changes in EEG rhythms include an increase in alpha peak frequency, over frontal regions, accompanied by increase in delta and theta power [START_REF] Murphy | Propofol anesthesia and sleep: a high-density EEG study[END_REF][START_REF] Ching | Thalamocortical model for a propofol-induced rhythm associ-ated with loss of consciousness[END_REF].

Most of the previous studies on anesthetic phenomena have been done by considering a mean-field model to explain the biphasic behavior and describe some experimental feature of specific changes in electroencephalography (EEG) data recorded during anesthesia [START_REF] Bojak | Modeling the effects of anesthesia on the electroencephalogram[END_REF][START_REF] Steyn-Ross | Theoretical electroencephalogram stationary spectrum for a white-noise-drivenvcortex: evidence for ageneral anesthetic-induced phase transition[END_REF][START_REF] Hindriks | Meanfield modeling of propofolinduced changes in spontaneous EEG rhythms[END_REF][START_REF] Hutt | Effects of the anesthetic agent propofol on neural populations[END_REF]. While some previous theoretical studies (Steyn-Ross 1999; [START_REF] Bojak | Modeling the effects of anesthesia on the electroencephalogram[END_REF]; Hindriks and van Putten 2012) are based on the same type of continuous spatial mean-field model involving spatial partial derivatives [START_REF] Liley | A continuum theory of electrocortical activity[END_REF], Hutt and Longtin have considered a neural populations model motivated by Wilson and Cowan [11] and Amari [START_REF] Amari | Dynamics of pattern formation in lateral inhibition type neural fields[END_REF].

In this study we use a thalamocortical feedback model first developed by Rennie et al. [START_REF] Rennie | Unified neurophysical model of EEG spectra and evoked potentials[END_REF] and recently extended to model general anesthesia by Hindriks and van Putten [START_REF] Hindriks | Meanfield modeling of propofolinduced changes in spontaneous EEG rhythms[END_REF] to reproduce the specific changes in EEG activity that can be observed during the propofol-induced general anesthesia. The present work reviews this latter model and points out the importance of stationary states to understand EEG power spectra during anesthesia.

Methods

Model

The body of the model [START_REF] Hindriks | Meanfield modeling of propofolinduced changes in spontaneous EEG rhythms[END_REF] is based on a population-level model of a single thalamocortical module consisting of four populations of neurons, namely excitatory (E) and inhibitory (I) cortical neurons, a thalamic relay nucleus (S), and a thalamic reticular nucleus (R). The average soma membrane potential for a ∈ E, I, S, R is modeled by

V a (t) = b=E,I,R,S h(t) ⊗ K ab φ b (t -τ ab ), (1)
where φ b is the pulse firing rate of the population b (units Hz). The constants K ab are the strengths of the connections from population of type b to population of type a (units mVs). The delay term, τ ab is zero if the both populations are in the thalamus or in the cortex. For thalamocortical or corticothalamic pathway, the delay is nonzero [START_REF] Victor | Mean-field modeling of thalamocortical dynamics and a model-driven approach to EEG analysis[END_REF]. We point out that this model does not distinguish excitatory and inhibitory synapses in contrast to other models for general anaesthesia as [START_REF] Bojak | Modeling the effects of anesthesia on the electroencephalogram[END_REF][START_REF] Steyn-Ross | Theoretical electroencephalogram stationary spectrum for a white-noise-drivenvcortex: evidence for ageneral anesthetic-induced phase transition[END_REF][START_REF] Hutt | Effects of the anesthetic agent propofol on neural populations[END_REF]. In this model, only the axons of excitatory cortical neurons are long enough to emit propagating pulses along axons and the φ E obeys the damped oscillator equation

Dφ E = S(V a ), (2)
in which the operator D is defined as

D = 1 γ ∂ ∂t + 1 2 , ( 3
)
where γ is the ratio of propagation velocity to mean axonal length. It is assumed that the spatial spread of activity is very fast in other populations and the activity variable can be approximated by a sigmoidal function as

φ a = S(V a ) = S max [1 + exp(- V a -θ σ )] -1 , (4)
in which S max is the maximal firing rate (units Hz), θ is the average activation threshold (units mV), and σ is proportional to the standard deviation of activation thresholds over the populations (units mV -1 ). In Eqs. ( 1), ⊗ denotes the convolution operator and h(t) denotes the mean synaptic response function

h(t) = αβ β -α e -αt -e -βt , (5)
where α and β are the synaptic decay and rise rate of synaptic response function, respectively.

External input to the system can be considered as a non-specific input to relay neurons as

K SN φ N = φ N + √ 2κξ(t), (6)
where φ N indicates its mean value, ξ(t) is a Gaussian white noise with average zero and κ is the intensity of the driving noise. For more details of model and the nominal parameter values see [START_REF] Hindriks | Meanfield modeling of propofolinduced changes in spontaneous EEG rhythms[END_REF].

Effect of propofol on populations

It has been shown that propofol increases the decay time constant of GABA A synapses, and hence increases the total charge transfer in these synapses but not that of excitatory synapses [START_REF] Kitamura | Effects of halothane and propofol on excita tory and inhibitory synaptic transmission in rat cortical neurons[END_REF]. Interestingly propofol has been shown to have a negligible effect on the amplitude synaptic receptors in cortical neurons [START_REF] Kitamura | Effects of halothane and propofol on excita tory and inhibitory synaptic transmission in rat cortical neurons[END_REF].

To integrate physiological observations into the model, the potentiation of synaptic receptors in anesthesia condition can be modeled by α → α/p with p ≥ 1, which leads to a decrease in the decay rate constant α or equivalently, an increase in decay time constant of GABA A receptors. The factor p indicates the target concentration of propofol in the neural populations. We take p = 1 for zero concentration i.e, baseline condition. Then we could replace the synaptic response h(t) by

h(t) = H η(α, β) h(t), (7)
in which

η(α, β) = αβ β -α exp -α ln(β/α) β -α -exp -β ln(β/α) β -α , (8)
where the constant H indicates the synaptic efficacy [START_REF] Hindriks | Meanfield modeling of propofolinduced changes in spontaneous EEG rhythms[END_REF]. The maximum height of h(t) indeed is H and hence is independent of the rate constants α and β.

The baseline value chosen for α and β; α=50 Hz, β=200 Hz leads to the value η(α, β) = 31.5 Hz .

Theoretical power spectrum

The stationary state of Eqs. ( 1) obeys dV a (t)/dt = 0. We could linearize the Eqs.

(1) about the stationary state and write them in a general matrix form of a linear DDE as

L ∂ ∂t X(t) = AX(t) + BX(t -τ ) + I(t), (9)
with matrices A, B, the system activity vector X and the external input I. The solution of system can be written as

X(t) = ∞ -∞ G(t -t ′ )I(t ′ )dt ′ , (10)
and the Green function obeys

L ∂ ∂t G(t) = AG(t) + BG(t -τ ) + 1δ(t), (11)
in which 1 is unitary matrix. Applying the Fourier transform

G(t) = 1 √ 2π ∞ -∞ G(ω)e iωt dω (12)
yields

G(ω) = 1 √ 2π [ L(ω) -A -Be -iωτ ] -1 . (13)
The power spectral density matrix P (ω) of X(t) is the Fourier transform of the auto-correlation function matrix X(t) t X(t -T ) (Wiener-Khinchine Theorem) leading to

P (ω) = 2κ √ 2π G(ω) Gt (-ω),
where the high index t denotes the transposed vector or matrix [START_REF] Hutt | The anesthetic propofol shifts the frequency of maximum spectral power in EEG during general anesthesia: analytical insights from a linear moddel[END_REF].

At the end, the model assumes that excitatory activity generates the EEG and by virtue of the specific choice of external input the power spectrum of the EEG depends just on one matrix component of the Greens function by

P E (ω) = 2κ √ 2π G1,3 (ω) G1,3 (-ω) = 2κ √ 2π G1,3 (ω) 2 . ( 14
)
The stationary state of Eqs. ( 1) is given by

V 0E = K EE S(V 0E ) + p 1 K EI S(V 0I ) + K ES S(V 0S ), V 0I = K IE S(V 0E ) + p 2 K II S(V 0I ) + K IS S(V 0S ), V 0S = K SN φ N + p 3 K SR S(V 0R ) + K SE S(V 0E ), V 0R = K RS S(V 0S ) + K RE S(V 0E ), (15)
where K SN φ N = 1mV and we take three different impact factors for the anesthetic effect of propofol as

H η ei = p 1 , H η ii = p 2 , H η sr = p 3 ,
in which we parametrize η ei , η ii and η sr by

η ei : α → α p 1 , η ii : α → α p 2 , η sr : α → α p 3 .
This assumes a complete insensitivity of synaptic receptors located on cortical pyramidal neurons and reticular nucleus.

For the linearization of Eqs. ( 1) one obtains

X(t) =     φ E (t) V I (t) V S (t) V R (t)     , A =     K 1 K 2 0 0 K 4 K 5 0 0 0 0 0 K 8 0 0 K 10 0     , B =     0 0 K 3 0 0 0 K 6 0 K 7 0 0 0 K 9 0 0 0     , I(t) =     0 0 √ 2κξ(t) 0     , with K 1 = K EE , K 2 = p 1 K EI ∂S[V ] ∂V | V =V 0I , K 3 = K ES ∂S[V ] ∂V | V =V 0S , K 4 = K IE , K 5 = p 2 K II ∂S[V ] ∂V | V =V 0I , K 6 = K IS ∂S[V ] ∂V | V =V 0S , K 7 = K SE , K 8 = p 3 K SR ∂S[V ] ∂V | V =V 0R , K 9 = K RE , K 10 = K RS ∂S[V ] ∂V | V =V 0S , K 11 = ∂S[V ] ∂V | V =V 0E , and
L(ω) -A -Be -iωτ =     L D K11 -K 1 -K 2 -K 3 e -iωτ 0 -K 4 L -K5 -K 6 0 -K 7 e -iωτ 0 L -K 8 -K 9 e -iωτ 0 -K 10 L     (16)
where L = (1 + iω/α)(1 + iω/β) and D = (1 + iω/γ) 2 . We point out that the new constants K i , i = 2, 3, 5, 6, 8, 10, 11 are proportional to the nonlinear gain ∂S/∂V computed at the stationary state. With Eq. ( 13) and ( 16), it turns out that the stationary state and the corresponding nonlinear gain play in important role in the power spectrum.

Results

This section shows that the model under study reproduce the specific changes observed in EEG data during the propofol-induced anesthesia. Figure 2 shows the theoretical EEG power spectrum in the baseline condition and after the administration of propofol. The spectrum resembles well experimental observation in EEG power spectrum, i.e. increases in delta and theta power as well as more pronounced alpha oscillations with increased peak-frequency. Figure 3 shows how the nonlinear gain and the stationary states dependent on the propofol concentration. We observe that the nonlinear gain may increase (a) or decrease (b) with increasing propofol dependent on the synapses that are modified. If the inhibitory synapses at cortical excitatory neurons (p 1 ) and at relay neurons (p 3 ) respond identically to a change of the propofol concentration in a specific relation to the response of synapses at cortical inhibitory neurons (p 2 ), then the nonlinear gain increases (Fig. 3(a)) reflecting an increased excitability and the power values increase as well (Fig. 2, red curves). In contrast, if the response of all three synapse types respond identically (as assumed in previous studies such as [START_REF] Hutt | Effects of the anesthetic agent propofol on neural populations[END_REF]), then the nonlinear gain decreases (Fig. 3(a)) and the decreased excitability diminishes the power spectrum values (cf. Fig. 2, blue curve).

1 1.2 1.4 1 2 3 4 5 F actorP 2 dS (V ) dV | V =V0 E 1 1.2 1.4 0.5 1 1.5 2 F actorP 2 dS (V ) dV | V =V0 E 1 1.5 2 0 50 100 150 F actorP 2 V 0E [mV ]
Moreover, the stationary states behave differently in the two cases, cf. Fig. 3(c) and (d). Increasing (decreasing) the nonlinear gain is accompanied by an increasing (decreasing) value of the corresponding stationary state, see panels (c) and (d). It is also remarkable that in (c) the two lower stationary states collide to a single state whereas in (d) the two upper states collide. This difference indicates two fundamentally different mechanisms which may yield the different dynamics observed in the power spectrum. This link will be a research topic of future work.

Discussion

In the recent study of Hindriks and van Putten the authors have considered a high-dimensional mean field model to reproduce observed EEG changes during general anesthesia. The present work illustrates this work in some detail and highlights the important assumptions. We have extended the previous work by investigating the effect of the stationary state and have revealed the the increase or decrease of power seems to be strongly related the the increase or decrease of the stationary state of the system. This new finding proposes a more detailed study of the stationary state of neural population activity under anesthesia.

Fig. 1 .

 1 Fig. 1. The temporal synaptic response function h(t) of inhibitory GABAA synapses subject to p. Parameters are set to α=50 Hz, β=200 Hz.

Fig. 2 .

 2 Fig.2. Theoretical power spectrum of EEG in the baseline condition (solid black line) and three different sets of factor p in the anesthesia condition; p1=p3=1+0.5(p2-1), p2=1.1 (dashed red line), p2=1.25 (solid red line) and p1=p2=p3=1.05 (dashed blue line).

Fig. 3 .

 3 Fig.3. The stationary states and the nonlinear gain dS/dV computed at the lowest stationary state of pyramidal neurons V0E subjected to the factor p2. a, c) p1=p3= 1+0.5(p2-1), b, d) p1=p2= p3. We observe three states in (c) and (d) for p = 1 where (c) the two lower states collide or (d) the two upper states collide. The center branch (red) is linearly unstable, whereas the other branches are linearly stable.

Acknowledgments.

The authors acknowledge funding from the European Research Council for support under the European Union's Seventh Framework Program (FP7/2007-2013) ERC grant agreement No.257253.


Zhoulai Fu

Targeted Update -Aggressive Memory Abstraction Beyond Common Sense and its Application on Static Numeric Analysis

Keywords: abstract interpretation, points-to analysis, abstract numeric domain, abstract semantics, strong update

Summarizing techniques are widely used in the reasoning of unbounded data structures. These techniques prohibit strong update unless certain restricted safety conditions are satisfied. We find that by setting and enforcing the analysis boundaries to a limited scope of program identifiers, called targets in this paper, more cases of strong update can be shown sound, not with regard to the entire heap, but with regard to the targets. We have implemented the analysis for inferring numeric properties in Java programs. The experimental results show a tangible precision enhancement compared with classical approaches while preserving a high scalability.

Introduction

Static analysis of heap-manipulating programs has received much attention due to its fundamental role supporting a growing list of other analyses (Blanchet et al., 2003b;[START_REF] Chen | Compiler support for speculative multithreading architecture with probabilistic points-to analysis[END_REF][START_REF] Fink | Effective typestate verification in the presence of aliasing[END_REF]. Summarizing techniques, where the heap is partitioned into finite groups,can manipulate unbounded data structures through summarized dimensions [START_REF] Gopan | Numeric domains with summarized dimensions[END_REF]). These techniques have many possible uses in heap analyses, such as points-to analysis [START_REF] Emami | Context-sensitive interprocedural points-to analysis in the presence of function pointers[END_REF] and TVLA [START_REF] Sagiv | TVLA: A system for implementing static analyses[END_REF], and also have been investigated as a basis underpinning the extension of classic numeric abstract domains to pointer-aware programs [START_REF] Fu | Static Analysis of Numerical Properties in the Presence of Pointers[END_REF]. Most of these analyses follow the strong/weak update paradigm [START_REF] Chase | Analysis of pointers and structures (with retrospective)[END_REF] to model the effects of assignments on summarized dimensions. A strong update overwrites the data that may be accessed with a new value, whereas a weak update adds a new value to the summarized dimensions and preserves their old values. Strong update is desired whenever safe as it provides better precision.

Applying strong update to a summarized dimension requires that it represent a single run-time memory. This requirement poses a difficulty for applying strong update as it is usually hard to know the element number represented by a summarized dimension. Efforts have been made to use sophisticated heap disambiguation techniques [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF]. While such approaches indeed help to find out more strong update circumstances, many of the proposed algorithms, such as focus and blur operations in shape analysis, are often hard to implement or come with a considerable complexity overhead.

The paper presents a new memory abstraction that makes strong update possible for summarized dimensions even if they do not necessarily represent a singleton. The approach is called targeted update. It extends the traditional notion of soundness in heap analysis by focusing the abstract semantics on a selected set of program identifiers, called targets.

Our major finding can be summarized as follows: By focusing on the targets, we are able to perform an aggressive analysis even if the traditional safety condition for strong update fails.

A motivating example Consider the assignment y.f = 7. Assume that the memory state before the assignment is informally represented in Fig. 1. The two access paths x.f and y.f are of integer type. The two gray clouds denoted by δ 1 and δ 2 represent two disjoint summarized dimensions. They initially store numeric values in the range of [0,5] and [0,9] respectively. An edge from an access path to a cloud indicates a may-access relation.

δ 1 δ 2 x.f y.f [0, 5] [0, 9] ❄ ❄ ✟ ✟ ✟ ✟ ✟ ✙
The memory state does not tell which summarized dimension (δ 1 or δ 2 ) should be updated. In addition, more than one concrete memory cell may be associated with δ 1 or δ 2 . Thus, traditional analysis of y.f = 7 performs weak update on δ 1 and δ 2 . The abstract state after the assignment becomes δ 1 ∈ [0, 7] ∧ δ 2 ∈ [0, 9], following which we infer x.f ∈ [0, 7] ∧ y.f ∈ [0, 9]. We call this approach common sense strong/weak update paradigm. Now we present the targeted update approach. In this approach, a set of access paths needs to be selected before the analysis. The selected set is called target set. Here, if we set {y.f } as target set, we are able to apply strong update on both δ 1 and δ 2 . This is because making wrong assertions on the concrete memories of δ 1 or δ 2 that are not pointed to by y.f does not contravene the soundness with regard to the targets: The two clouds are at most pointed to by x.f and y.f , yet x.f is not a target. The described approach is called targeted update. Applying targeted update with target set {y.f } allows for precise analysis of y.f , but the value of the non-target x.f is not tracked. The obtained δ 1 = 7 ∧ δ 2 = 7 only infers y.f = 7. There is no information concerning x.f . It can be seen that depending on specific analysis requirement, the target set {y.f } may not be appropriate. Imagine that we want to verify this post-condition of the statement y.f = 7

x.f ∈ [0, 7] ∧ y.f ∈ [0, 7] (1)
This property cannot be verified by the strong/weak update paradigm, neither by the targeted update using {y.f } as the target set. To use targeted update with the target set T = {x.f, y.f } solves the problem. The summarized dimension δ 1 is now pointed to by both targets, and δ 2 by one target. Targeted update weakly updates δ 1 because updating δ 1 has an effect on both x.f and y.f that are targets. It strongly updates δ 2 because it is a region that can only be "observed" from y.f : For the concrete memories represented by δ 2 that are not pointed to by y.f , nothing is wrong to associate whatever values with δ 2 ; for the concrete memories represented by δ 2 that are truly pointed to by y.f , the values associated with δ 2 due to targeted update are correct. Finally, targeted update obtains δ 1 ∈ [0, 7] ∧ δ 2 = 7, from which we infer (1). In summary, targeted update has only responsibilities for its targets, namely, the objects pointed to by these targets, and it has no obligation to be sound with regard to the entire heap as in the common sense approach. As illustrated by the example, targeted update has two major characteristics: 1) More strong update cases on summarized dimensions can be discovered by targeted update.

2) Picking up right target set is a trade-off problem since targeted update can be very precise for targets, but it does not track non-targets.

This paper makes the following key contributions:

-We introduce the concept of targets and formalize the soundness notion with regard to targets (Sect. 3). The crucial insight lies in the fundamental difference of this notion of soundness with that in the common sense strong/weak paradigm. -We derive an aggressive abstract semantics (Sect. 4 and 5) from the notion of targets. This is made possible due to a simple condition we have discovered that allows targeted update to be safely applied. We have formalized and proved the soundness of targeted update. -Important design choices are discussed in Sect. 6. The implemented analyzer was tested on the SPECjvm98 benchmark suite, composed of 10 real-world Java programs.

Preliminaries

This section gives a brief review of some basic concepts from static program analysis that are used in this paper. Some notions of abstract interpretation are recalled In Sect. A.

General notations

Syntactical notations

The primary data types include scalar numbers in I, where I can be integers, rationals or reals, and pointers (or references) in Ref .

The primary syntactical entities include the universe of local variables and fields.

They are denoted by Var and Fld respectively. An access path [START_REF] Landi | A safe approximate algorithm for interprocedural pointer aliasing[END_REF] is either a variable or a variable followed by a sequence of fields. The universe of access paths is denoted by Path. We subscript Var τ , Fld τ , Path τ and their elements with τ ∈ {n, p} to indicate their types as scalar number or reference. We use Imp n to refer to the basic statements involving only numeric variables and use the meta-variables s n to range over these statements. Similarly, we let Imp p be the statements that use only pointer variables and let s p range over these statements. Below we show the main syntactical categories and the meta-variables used in the paper.

xn = k | xn = yn | xn = yn ⋄ zn | xn ⊲⊳ yn sp ∈ Imp p xp = new | xp = null | xp = yp.fp | xp = yp | xp.fp = yp
where ⋄ ∈ {+, -, * , /}, and ⊲⊳ is an arithmetic comparison operator.

Analysis of Imp n

We express a numeric property by a conjunction of arithmetic formulae such as {x + y ≤ 1, x ≤ 0}. The universe of the numeric properties is denoted by Num ♯ . As usual, an environment maps variables to their values. We consider numeric environments Num Var n → I ⊥ . The relationship between an environment and a property can be formalized by the relation of valuation. We say that n ∈ Num is a valuation of n ♯ ∈ Num ♯ , denoted by

n |= n ♯ (2)
if n ♯ becomes a tautology after each of its free variables is replaced by its corresponded value in n. For example, if n = {x → 7, y → 7}, and n ♯ = {x + y < 15} then we have n |= n ♯ . For each statement s n of Imp n , the concrete semantics is given by a standard rule of state transition

Num -→ (s n ) ∈ Num → Num.
We write ⊔ and ▽ for the join and widening operator.

In this paper, we assume that a sound abstract semantics of

s n of signature [|•|] ♯ n ∈ Imp n → (Num ♯ → Num ♯
) is available to us. The abstract semantics is assumed to be sound with regard to the concrete Num -→: For any n, n ♯ and

s n ∈ Imp n , n |= n ♯ ⇒ Num -→ (s n )(n) |= [|s n |] ♯ n (n ♯ ).
Analysis of Imp p A concrete state in Imp p is thought of as a graph-like structure representing the environment and heap. The universe of the concrete states is denoted by Pter . We write p to range over them.

p ∈ Pter (Var p → Ref ⊥ ) × ((Ref × Fld p ) → Ref ⊥ ) (3)
Points-to analysis is a dataflow analysis for detecting pointer relations. The essential process is to partition Ref into a finite set H and then to summarize the run-time pointer relations via elements of H and program variables. The elements of H are called allocation sites or abstract references. The process can be interfaced with a function ⊲ called naming scheme.

⊲ ∈ Ref → H (4)
In this paper, we consider a standard naming scheme that names heap objects after the control points where the objects are allocated. We assume that the naming scheme is flow-independent. That is to say, the analysis of two control branches uses the same naming scheme. Note that this is the case for points-to analysis but not for shape-analysis.

Definition 1 (Interface of traditional points-to analyzer).

(Imp p , Pter , Pter -→, Pter ♯ , γ p , [|•|] ♯ p )
The universe of the concrete states is denoted by Pter , and the concrete transition rule is denoted by Pter -→∈ Imp p → (Pter → Pter ). The universe of the abstract states is denoted by Pter ♯ . We write p ♯ to range over them.

p ♯ ∈ Pter ♯ (Var p → ℘(H)) × ((H × Fld p ) → ℘(H))
(5)

Each

Summarizing Technique with Targets

In this section, we introduce the concept of targets and how summarizing technique with targets differs from classic summarizing technique.

The analyzed language This paper focuses on how to deal with language Imp np . The statements in Imp np include these in Imp n and Imp p , and statements in the forms of y p .f n = x n and x n = y p .f n . We write s np to range over Imp np .

s np ::= s n | s p | y p .f n = x n | x n = y p .f n (6)
We call y p .f n = x n or y p .f n = k a write access and x n = y p .f n a read access.

A non-standard concrete semantics A concrete state in Imp np is an environment mapping variables to values and a mapping from fields of references to values. By grouping the numeric and pointer parts, we formalize the universe of the concrete states as

State = Num[Var n ∪(Ref ×Fldn)] (Var n → I ⊥ ) × ((Ref × Fld n) → I ⊥ ) (7) × (Var p → Ref ⊥ ) × ((Ref × Fld p) → Ref ⊥ ) Pter (8)
1 L i s t tmp = null , hd ; 2 i n t i d x ; 3 f o r ( i d x = 0 ; i d x < 3 ; i d x ++){ 4 hd = new L i s t ( ) ; / / a l l o c a t i o n s i t e h 5 hd . v a l = i d x ; 6 hd . n ext = tmp ; 7 tmp = hd ; 8 }
The integers 0, 1 and 2 are stored iteratively on the heap. The head of the list is pointed to by the variable hd. The concrete state at the end of the program can be specified as (n, p). We write r 0 , r 1 and r 2 for the concrete memories allocated at allocation site h.

n = {(r 0 , val) → 0, (r 1 , val) → 1, (r 2 , val) → 2, idx → 3} p = {hd → r 2 , tmp → r 2 , (r 2 , next) → r 1 , (r 1 , next) → r 0 } (9)
Common Sense Summarizing Technique A naming scheme ⊲ ∈ Ref → H is assumed for the analysis of Imp np . In this context, the idea of summarizing technique is to use the names computed by the naming scheme to create summarized dimensions that represent the numeric values stored on the heap. Below we show an abstraction of the concrete state ( 9).

(n ♯ , p ♯ ) = δ h,val ∈ [0, 2], idx = 3, hd / / h next y y (10)
In this abstraction, the naming scheme maps the concrete r 0 , r 1 and r 2 to an abstract reference h ∈ H. We can perform pointer analysis based on the naming scheme and, on the other hand, summarize numeric information on the val field of r 0 , r 1 and r 2 by a summarized dimension related to h and val, denoted by δ h,val . The summarized dimension in this context is an element H × Fld n .

In the following, we denote H × Fld n by ∆, and use δ to range over the pairs in ∆. We also write δ h,fn to indicate the summarized dimension corresponding to the allocation site h and the field f n .

Definition 2. An abstract state is defined to be a pair

(n ♯ , p ♯ ) of NumP ♯ Num ♯ [Var n ∪ ∆] × Pter ♯ (11)
where Num ♯ [Var n ∪ ∆] is similar to Num ♯ , but defined over Var n ∪ ∆, and Pter ♯ is the universe of points-to graphs (Sect. 2).

The summarizing process can be formalized through the extended naming scheme on Ref × Fld n → H × Fld n , defined as λ(r, f n ).(⊲(r), f n ). By abuse of notation, we still write ⊲ for the extended naming scheme. For example, the naming scheme used in (10) satisfies ⊲(r i , f ) = δ h,f for i = 0, 1 and 2. In (10), δ h,val → [0, 2] asserts that its concrete state (n, p) must satisfy

∀(r, val) ∈ ⊲ -1 (δ h,val ) : n(r, val) ∈ [0, 2] ( 12
)
This is common sense -a summarized dimension represents a set of concrete locations, and the fact over the summarized dimension translates to all the heap locations represented by the summarized dimension. Although it seems natural to require (12), we find that this kind of "contract" between the abstract and concrete states can be in some circumstances, too strong to be useful.

Assume that we have an extra statement hd.val = 0 after l. 8. Imagine that we only want to ensure that hd.val becomes 0 after the statement. We cannot update δ h,val to 0 because that would mean all (r, val) ∈ ⊲ -1 (δ h,val ) store the value 0, which is clearly unsound. To make a more precise analysis in this situation, we need to relax the condition (12) so that a fact over a summarized dimension does not always translate to all their represented concrete heap locations. This is where targeted update comes in. It allows a subset S ⊆ ⊲ -1 (δ h,val ) in ( 12) to be specified so that the abstract semantics only needs to guarantee n(r, val) ∈ [0, 2] for (r, val) belonging to the specified subset S.

Targets In the context of Imp np , a target set, or targets, is a set of access paths holding numeric values on the heap. These access paths should not be local variables, and may not occur in the analyzed program syntax.

We use two operations on targets: Let t be an access path of a target set, p ∈ Pter , d ∈ Ref × Fld n . Then d = p(t) reads as t resolves to or points to d under p. If p has an arc from variable x to r, then p(x.f n ) = (r, f n ); δ ∈ p ♯ (t) reads as t resolves to or points to δ under p ♯ . For example, in Fig. 1, we have p ♯ (x.f ) = {δ 1 } and p ♯ (y.f ) = {δ 1 , δ 2 }. See Sect.B for their formal definitions.

Below we write p ∈ γ p (p ♯ ) to denote that p is abstracted by p ♯ ; we write n |= [ins]n ♯ to denote that n is a valuation (the symbol |= is introduced in Sect. 2) of n ♯ with its variables substituted following ins. For example, let ins =

{δ 1 → d 1 , δ 2 → d 2 } and n ♯ = {δ 1 + δ 2 > 0, δ > 10}. Then we have [ins]n ♯ = {d 1 + d 2 > 0, d 2 > 10}.
If a target set is selected and the soundness is enforced with regard to the targets, the abstract state (n ♯ , p ♯ ) represents all concrete states (n, p) as long as p is abstracted by p ♯ and n can be abstracted by whatever n ♯ ′ that is n ♯ with its summarizing dimensions δ 1 , . . . , δ m instantiated with some d 1 , . . . , d m satisfying: For 1 ≤ i ≤ m, ⊲(d i ) = δ i and d i can be reached by targets, i.e., ∃t ∈ T : d i = p(t). Definition 3. Let T be the target set. The concretization of a state (n ♯ , p ♯ ) ∈ NumP ♯ is defined as S assigns x n to δ, regarding x n and δ as scalar variables. For example, if it is interval domain on which targeted update is built, we have

γ T (n ♯ , p ♯ ) {(n, p) | p ∈ γ p (p ♯ ), ∀ins ∈ Ins p T : n |= [ins](n ♯ )} (13) with Ins p T {ins ∈ ∆ → D | ∀(δ, d) ∈ ins : ⊲(d) = δ ∧ d ∈ post[p](T )}. Read it as, an element (n, p) is in the concretization γ T (n ♯ , p ♯ ), if p is in the concretization of p ♯ ,
[|δ = x n |] S ({δ ∈ [1, 2], x n ∈ [3, 4]}) = {δ ∈ [3, 4], x n ∈ [3, 4]} (14) Another operator [|δ = x n |]
W is called local weak update operator. It assigns x n to δ and then joins the result with its original state, for example,

[|δ = x n |] W ({δ ∈ [1, 2], x n ∈ [3, 4]}) = {δ ∈ [1, 4], x n ∈ [3, 4]} (15)
It is clear that both operators can be computed from traditional numeric domains.

The input of targeted update is an abstract state (n ♯ , p ♯ ) ∈ NumP ♯ and a pre-selected target set T . We do not care about how this set is selected for now. Targeted update first computes the summarized dimensions to which y p .f n resolves, namely p ♯ (y p .f n ). Each summarized dimension δ is then treated one by one.1 If the following condition holds:

δ is pointed to by no target in T \{y p .f n } (TU )
then local strong update will be performed on δ; otherwise, local weak update has to be performed on δ. The above condition is referred to as (TU ) condition subsequently. This algorithm for the abstract semantics is presented in Algo. 1.

(n ♯ , p ♯ ) 1 n ♯ ′ ← n ♯ 2 for δ ∈ p ♯ (yp.fn) do 3 if there exists no t ∈ T \{yp.fn} satisfying δ ∈ p ♯ (t) then 4 n ♯ ′ ← [|δ = xn|] S (n ♯ ′) 5 else 6 n ♯ ′ ← [|δ = xn|] W (n ♯ ′) 7 end if 8 end for 9 return n ♯ ′, p ♯
Remark 1. Automatically finding targets adapted to specific problem requirements is a problem in itself. In our implementation, we use the numeric access paths (excluding scalar variables) that appear syntactically in the program as targets.

Comparison with Strong/Weak Update Below, we present a case study. It shows how targeted update works and in which way it differs from the common sense strong/weak update paradigm.

Example 2. Assume that a program has three numeric access paths: t, y p .f n and s, and there are three summarized dimensions: δ 1 , δ 2 and δ 3 . Assume that the access paths resolve to summarized dimensions as depicted:

t * * y p .f n x x & & s x x δ 1 δ 2 δ 3 (16) namely, p ♯ (t) = {δ 3 }, p ♯ (y p .f n ) = {δ 1 , δ 2 , δ 3 }, p ♯ (s) = {δ 2 , δ 3 }.
We shall compare targeted update and strong/weak update paradigm of y p .f n = x n .

The concrete semantics of y p .f n = x n is known: It modifies one element of

d ∈ ⊲ -1 (δ 1 ) ∪ ⊲ -1 (δ 2 ) ∪ ⊲ -1 (δ 3 ).
It is clear that the information from ( 16) does not help to identify the one among δ 1 , δ 2 , and δ 3 that will be modified by the statement. In addition, this specific δ may have more than one concrete represented element. Thus, the traditional approach performs weak update which amounts to a conservative join of

[|δ 1 = x n |] W (n ♯ ), [|δ 2 = x n |] W (n ♯ ) and [|δ 3 = x n |] W (n ♯ ).
Formally, the weak update is defined as

[|y p .f n = x n |] ♯ (n ♯ , p ♯ ) ⊔ δ∈p ♯ (yp.fn) [|δ = x n |] W (n ♯ ) , p ♯ (17)
Now, let us consider targeted update. Assume that all three access paths are targets, T = {t, y p .f n , s}. Because only δ 1 satisfies (TU ) condition, targeted update abstracts y p .f n = x n as a composition of local weak update of δ 2 and δ 3 , and local strong update of δ 1 , namely, [

|δ 3 = x n |] W • [|δ 2 = x n |] W • [|δ 1 = x n |]
S . Formally, we define targeted update as follows.

Definition 4. Let T be a set of targets, (n ♯ , p ♯ ) ∈ NumP ♯ . Define the targeted update for y p .f n = x n :

[|y p .f n = x n |] ♯ T (n ♯ , p ♯ ) [|δ 1 = x n |] η(δ1) • • • • • [|δ M = x n |] η(δ M ) n ♯ , p ♯ (18) with {δ 1 , . . . , δ M } = p ♯ (y p .f n ), η λδ : p ♯ (y p .f n ). S if {t ∈ T | t = y p .f n ∧ δ ∈ p ♯ (t)} = ∅ W otherwise (19)
Correctness The correctness of the abstract semantics can be formalized as follows.

Theorem 1. Let T be a target set. For any abstract state (n ♯ , p ♯ ) of NumP ♯ and any (n, p) ∈ γ T (n ♯ , p ♯ ). We have

-→ ♮ (y p .f n = x n )(n, p) ∈ γ T • [|y p .f n = x n |] ♯ T (n ♯ , p ♯ ) ( 20
)
We need a lemma for the proof. If the (TU ) condition holds, the summarized dimension δ specified in the condition is pointed to by at most one target. Observationally, δ is a singleton representing only one object, although δ may represent more than one object that is not necessarily pointed to by targets. This intuition is formalized as the lemma below. We write tu(T, p ♯ , y p .f n , δ) as a shortcut for (TU ), namely ∃t ∈ T \{y p .f n } : δ ∈ p ♯ (y p .f n ). The proof of the lemma needs a property as stated of points-to graph: For any concrete p and abstract p ♯ such that p ∈ γ p (p ♯ ), if access path u resolves to d ∈ Ref × Fld n , i.e. p(u) = d, then we have ⊲(d) ∈ p ♯ (u). This property ensures, for example, if p(x) = r in the concrete, then p ♯ (x) has to contain ⊲(r).

Lemma 1. Assume that tu(T, p ♯ , y p .f n , δ) holds. Then, for any p ∈ γ p (p ♯ ) and ins ∈ Ins p T , we have ins(δ) = p(y p .f n ).

Proof (Proof of Lem. 1). Because ins ∈ Ins p T , we have ins(δ) must be pointed to by targets in T .

ins(δ) ∈ {p(t) | t ∈ T, t = y p .f n } ∪ {p(y p .f n )} (21)
Condition (TU ) combined with the semantics of points-to graph tells that the first part of (21) has to be empty. Otherwise, we have some t ∈ T \{y p .f n } pointing to δ, which contradicts tu(T, p ♯ , y p .f n , δ). By consequence, we have

ins(δ) = p(y p .f n ). ⊓ ⊔
This lemma plays a crucial role in proving the correctness of the abstract semantics. We give its proof sketch in Sect. F.

Targeted Update

-the case of read access x n = y p .f n , s n and s p

We have developed an abstract semantics for the write access statement using the soundness notion with regard to targets. This section presents our abstract semantics for other types of statements in Imp np .

Case for x n = y p .f n Assume that y p .f n only resolves to δ. It is tempting, but wrong, to abstract statement as in traditional numeric analysis, i.e., [

|x n = δ|] ♯ n . Consider a = x.f; b = y.f; if (a < b){...}. Assume that p ♯ (x.f ) = p ♯ (y.f ) = {δ}.
If the abstract semantics relates a (resp. b) with δ after a = x.f (resp. b = y.f ), the analysis will wrongly argue that the following if branch can never be reached. The above reasoning is wrong because we should not, in general, correlate a summarized dimension with a scalar variable.

Gopan et al. have pointed out that to assign a summarized dimension δ to a non-summarized dimension x n takes three steps: First, extend δ to a fresh dimension δ ′ (using the operator expand ♯ δ,δ ′ that copies dimensions. Then, relate x n with δ ′ using traditional abstract semantics for assignment

[|x n = δ ′ |] ♯ n .
Finally, the newly introduced dimension δ ′ has to be dropped (using the operator drop ♯ δ ′ that removes dimensions). See [START_REF] Gopan | Numeric domains with summarized dimensions[END_REF] for the details of drop ♯ δ ′ and expand ♯ δ,δ ′ . In summary, Gopan's operator copies the values of the summarized dimension to the scalar variable but keeps them uncorrelated. The following operator is used to assign a summarized dimension δ to a scalar variable x n .

G(x n , δ) λn ♯ . drop ♯ δ ′ • [|x n = δ ′ |] ♯ n • expand ♯ δ,δ ′ n ♯ (22)
For example, the property G(x n = δ){δ > 1} = {x n > 1, δ > 1} after applying x = δ. We see that scalar variable x n and summarized dimension δ cannot be related, even if the underlined numeric domain is relational.

Remark 2. The lack of correlation between δ and x n reveals another source of imprecision of the classic soundness notion, besides its weak update semantics. Sharper analysis can be obtained thanks to the notion of targets. In Lem. 1, we have shown an important consequence of (TU ), that is, the underlined summarized dimension δ represents a single concrete object among the objects pointed to by the targets. This lemma allows us to deal with δ satisfying (TU ) as a scalar variable.

Consider the read access x n = y p .f n . Let (n ♯ , p ♯ ) be the input abstract state, T be the targets. If y p .f n ∈ T , we have to unconstrain x n . If y p .f n ∈ T and p ♯ (y p .f n ) = {δ 1 , . . . , δ M }, targeted update joins the effects of assigning δ i to x n for 1 ≤ i ≤ M . For each δ i , if (TU ) satisfies, the effect of assigning δ i to x n is the same as [|x n = δ i |] ♯ n (n ♯ ), as if δ i is a scalar variable; if (TU ) fails, the best we can do is to copy the possible values of δ i into x n , which amounts to using Gopan's operator (22). This is summarized in Algo. 2. That is,

[|x n = y p .f n |] ♯ T (n ♯ , p ♯ ) [|x n =?|] ♯ n n ♯ , p ♯ y p .f n ∈ T δ∈p ♯ (yp.fn) [|x n = δ|] η(δ) n ♯ , p ♯ y p .f n ∈ T (23)
where the operator [|x n =?|]

♯ n unconstrains x n , η is the shortcut defined in ( 19), and

[|x n = δ|] S [|x n = δ|] ♯ n , [|x n = δ|] W G(x n , δ) (24
(n ♯ , p ♯ ) 1 if yp.fn ∈ T then 2 return [|xn =?|] ♯ n (n ♯ ), p ♯ 3 n ♯ ′ ← ⊥ 4 for δ ∈ p ♯ (yp.fn) do 5 if there exists no t ∈ T \{yp.fn} satisfying δ ∈ p ♯ (t) then 6 n ♯ ′ ← n ♯ ′ ⊔ [|xn = δ|] ♯ n (n ♯ ′) 7 else 8 n ♯ ′ ← n ♯ ′ ⊔ G(xn, δ) 9 end if 10 end for 11 return n ♯ ′, p ♯
Case for s n If s n is an assignment in Imp n , it can be treated in the same way as in traditional numeric analysis using its abstract transfer function

[|•|] ♯ n (Sect.
2). In this paper, the transfer function for updating (n ♯ , p ♯ ) with s n is defined as:

[|s n |] ♯ T (n ♯ , p ♯ ) ([|s n |] ♯ n n ♯ , p ♯ ) (25)
Case for s p Targeted update tracks the heap objects pointed to by the targets. An important thing to note is that s p may cause changes to what objects the access paths are pointing-necessitating changes to the numeric portion of the abstract state. Subsequently, we write s p in the form of 'l=r'. Given a target set T and an abstract state (n ♯ , p ♯ ) ∈ NumP ♯ . Taking an arbitrary (n, p) ∈ γ T (n ♯ , p ♯ ), we want to find n ♯ ′ so that (n, In conclusion, a conservative way to model s p is to unconstrain targets that do not necessarily point to where they previously pointed. Thus, we unconstrain all p ♯ (t) such that t ∈ T and t has l as prefix. For example, in x = new; we unconstrain δ if it is pointed to by the target x.val. The transfer function for s p is modeled as:

[|s p |] ♯ T (n ♯ , p ♯ ) δ∈uncons T (sp,p ♯ ) [|δ =?|] ♯ n n ♯ , [|s p |] ♯ p p ♯ (26)
Here, uncons T (s p , p ♯ ) {δ | s p = 'l=r', ∃t ∈ T : t has l as prefix ∧ δ ∈ p ♯ (t)}.

A Discussion of Some Important Design Choices

Targets Our implementation uses the numeric access paths excluding variables that appear syntactically in the program as targets. Without prior knowledge of specific program properties to be verified, this design choice seems to give a tradeoff between expressiveness and precision. Although this target set may appear large, our experiments (Sect. 8) show that targeted update using this target set still provides a significant precision enhancement while covering common cases where program properties to be expressed only use program syntax.

Join and widening

The design of the join operator is usually a difficult step for developing abstract domains. We have assumed (Sect. 2) that the naming scheme should be flow independent. Thanks to the naming scheme hypothesis, our join operator seems to be delightfully uncomplicated: We just compute the join (or widening) component-wise. Then, if a concrete state (n, p) is in γ

T (n ♯ 1 , p ♯ 1 ) or in γ T (n ♯ 2 , p ♯ 2 ), it is also in the concretization of (n ♯ 1 ⊔ n ♯ 2 , p ♯ 1 ∪ p ♯ 2 ).
The case for widening is similar.

(n ♯ 1 , p ♯ 1 ) ⊔ ♯ (n ♯ 2 , p ♯ 2 ) = (n ♯ 1 ⊔ n ♯ 2 , p ♯ 1 ∪ p ♯ 2 ) (27) (n ♯ 1 , p ♯ 1 ) ▽ ♯ (n ♯ 2 , p ♯ 2 ) = (n ♯ 1 ▽ n ♯ 2 , p ♯ 1 ∪ p ♯ 2 ) ( 28
)
Constraint system with a flow-insensitive points-to analysis As in the implementation of [START_REF] Fu | Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for java[END_REF], we use a flow-insensitive points-to analysis to simplify the states propagation. The analysis is done in a pre-analysis phase and does not participate with the propagation of numeric lattices. The obtained flow-insensitive points-to graph is then used at each control point as a superset of the flow-sensitive points-to graph.

Using flow-insensitive variant does not cause any soundness issue. This is because the soundness of our analysis is based on the soundness of its component numeric domains and pointer analysis. Using the single flow-insensitive pointsto graph for all program control points can be modeled as an analysis that is initialized with an over-approximation of the least fixpoint of a flow-sensitive analysis that propagates in the style of skip.

Let

F ♯ (s) λn ♯ .fst • [|s|] ♯ T (n ♯ , p ♯ f i
), where p ♯ f i is the flow-insensitive pointsto graph, and fst is the operator that extracts the first element from a pair of components. We use the following the constraint system that operates on numeric lattice n ♯ only (rather than on (n ♯ , p ♯ ) pair):

n ♯ [l] ⊒ F ♯ (s)(n ♯ [l ′ ]) ( 29
)
where we write n ♯ [l] (resp. n ♯ [l ′ ]) for the numeric component of NumP ♯ at control point l (resp. l ′ ), l ′ is the control point of statement s, and (l ′ , l) is an arc in the program control flow.

Intra-procedural numeric analysis While the points-to graph is computed by an interprocedural pointer analysis, the static numeric anlaysis is intentionally left intra-procedural.

Existing numeric domains, in particular the relational ones, are generally sensitive to the size of the program and number of variables. The objective of scalability is hard to achieve if the problem solving has to iterate through all the program call-graph. To take variables in all the procedures as a whole necessarily incurs a high complexity for the numeric part in our analysis. To give an idea of this complexity, our experiments on the abstract domains in PPL show that octagonal analysis can hardly run on several hundreds of variables, and polyhedral analysis can quickly time out with more than 30 variables; on the other hand, a real-world Java program, with all its procedures put in together, could easily reach tens of thousands of variables to be analyzed.

A known workaround exists. The pre-analysis of variable packing technique allows ASTREE (Blanchet et al., 2003a) to successfully scale up to large sized C programs. We regard intra-procedural numeric analysis as a lightweight alternative to variable packing: Variables are related only if they are in the same procedure. In this way, we do not need to invent strategies to pack variables.

An Example

We discuss a Java program with interesting operations on a single linked list. Fig. 2 presents the program. Here, our goal is to show how targeted update works in practice and to prove two properties that are challenging for a human. The analysis results from our implemented analyzer are shown in Sect. E. 1 L i s t hd , node ; i n t i d x ; 2 hd = new L i s t ( ) ; / / a l l o c a t i o n s i t e h1 3 hd . v a l = 0 ; 4 hd . n ext = null ; 5 f o r ( i d x = -1 7 ; i d x < 4 2 ; i d x ++){ 6 node = new L i s t ( ) ; / / a l l o c a t i o n s i t e h2 7 node . v a l = i d x ; Example 3. Observe that there are two allocation sites h 1 and h 2 in the program, with the head of the list stored in h 1 and the body of the list stored in h 2 . The head node has a special meaning. It is used to indicate of length of the list. From l. 1 to l. 4, the program creates an empty list with a single head node. From l. 5 to l. 11, a list of integers is iteratively stored on the list. Within the loop, the head node is updated (l. 10) to track list length whenever a new list cell is created.

Targeted update, instantiated with polyhedral analysis, is able to infer the following properties:

-Prop1: At the loop entry (l. 5), hd.val ∈ [0, 60] ∧ hd.validx = 17.

-Prop2: From l. 5 to l. 10, hd.valnode.val = 17.

-Prop3: At the exit of the loop (l. 12), hd.val = 60.

Targeted update works as follows: First, it pre-analyzes the program with flow-insensitive points-to analysis. All numeric access paths appeared in program syntax that are not variables are taken as targets: T = {hd.val, node.val}. By computing {δ | ∃t ∈ T, δ ∈ p ♯ f i (t)}, targeted update obtains two summarized dimensions δ h1,val and δ h2,val . The initial abstract state is set to {δ h1,val → ⊤, δ h2,val → ⊤, idx → ⊤}. Then, we apply transfer functions of targeted update and solve the constraint system (29). For example, the statements at l. 3 and l. 7 are treated as write access y p .f n = x n . The statement at l .10 is transformed by SOOT into three short ones: tmp1 = hd.val, tmp2 = tmp1 + 1 and hd.val = tmp2. They are treated as read access, s n and write access statements, respectively. Finally, targeted update obtains (1) at l. 5: δ h1.val ∈ [0, 60] ∧ δ h1,validx = 17, (2) at l. 5 to l. 10: δ h1.valδ h2.val = 17 and (3) At l. 12: δ h1.val = 60. From these, we deduce Prop1, Prop2 and Prop3 respectively (based on the concretization function defined in Def. 3).

These properties are interesting and useful. Prop1 tells a non-trivial loop invariant involving access paths and scalar variables. Prop2 is particularly difficult to infer: hd.val and node.val have an invariant difference 17 because this is the case at the loop entry; in addition, node.val increments by one (because it is correlated with the idx at l. 7) at each iteration, and hd.val increments by one as well (l. 10). Prop3 gives a precise value stored in the head node, indicating that the list length is tracked as 60, precisely.

Remark 3. Targeted update is able to infer these relations because the summarized dimensions δ h1,val and δ h2,val lose their original sense: They can be correlated with scalar variables and strongly updated because (TU ) condition is satisfied there. In addition, since targeted update is built on traditional numeric domains, we can take the best from these, such as the very precise polyhedral abstraction and the widening/narrowing techniques [START_REF] Cousot | Comparing the Galois connection and widening/narrowing approaches to Abstract interpretation[END_REF] used in this example.

Experiments

The implemented targeted update is built on the static numeric analyzer NumP developed in [START_REF] Fu | Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for java[END_REF]. Our implementation of targeted update is called T-NumP. The analyzed language of T-NumP is Jimple [START_REF] Vallée-Rai | Soot -a Java bytecode optimization framework[END_REF]. The compiler framework SOOT is used as the analysis front-end. It offers a range of pointer analyses as well, including the points-to analysis and the side-effect analysis (to approximate the effects of invocation). The default flow-insensitive pointsto analysis used in SOOT is denoted by Pter subsequently. For the purpose of comparison, we have implemented a traditional static numeric analyzer for Java by wrapping abstract domains in PPL. The implemented analyzer is called Num.

Assessment To demonstrate the effectiveness of our technique, we evaluate it on the SPECjvm98 benchmark suite. The experiments were performed on a 3.06 GHz Intel Core 2 Duo with 4 GB of DDR3 RAM laptop with JDK 1.6.

We tested all the 10 benchmarks in SPECjvm98. The corresponding results are given in Tab. 1 and 2. The characteristics of the benchmarks are presented by the number of the analyzed Jimple statements (col. 2, STATEMENT), the number of write access statements in the form of y p .f n = x n or y p .f n = k (col. 3, WA), and the number of read access statements in the form of x n = y p .f n (col. 4, RA). Experimental results are shown in Tab. 1 where we use the interval domain Int64 Box of PPL.

Three parameters TU, PRCS, and SCALAR (col. 5-7) are measured to estimate the precision gain. The parameter TU counts the number of write access statements before which condition (TU ) is satisfied. We record PRCS for the (col. 11-12) are the ratios of TU and PRCS to the number of write access statements. The metrics Q SCALAR SCALAR/RA (col. 13) is defined with regard to read-access statements. The metric Q T T TNUMP/(T Num+T Pter) (col. 14) records the ratio of the time spent by our analysis to the total time of its component analyses.

The size of the analyzed Jimple statements ranges from 2307 ( 200 check) to 25973 ( 213 javac).2 We observe that T Pter is always much larger than T Num. This is because the points-to analysis is interprocedural while the numeric analysis is run procedures by procedures. Our analysis relies on the pointer analysis and is thus bottlenecked by it in terms of efficiency. Still, the time spent for the benchmark takes several minutes, with an average Q T = 151%. The average precision metrics is calculated on the last row of Tab. 1. Q TU = 90%, Q PRCS = 48% show a clear precision enhancement of our approach over traditional approaches.

Please mind the gap between TU and PRCS in Tab. 1 (and between Q TU nd Q PRCS as well). Besides the non-monotonicity of widening operators [START_REF] Cortesi | Widening and narrowing operators for abstract interpretation[END_REF], we observe that the practical reason causing this disparity is that targeted update, in the context of non-relational analysis (as the interval analysis above), is helpless in dealing with write-access statements in the form of y p .f n = x n as long as no information on x n has been gathered. This point can be remedied by relational analysis. Tab. 2 shows our experimental results with octagonal analysis and the same points-to analysis as above. Since the condition (TU ) can not be influenced by numeric analysis, we obtain the same Q TU as in Tab. 1. The parameters Q PRCS and Q SCALAR can be greatly improved due to the relational analysis, with similar time overhead Q TU as in Tab. 1. The experimental results show that targeted update discovers significantly more program properties in summarized dimensions and scalar variables as well, at a cost comparable to that of running the numeric and pointer analysis separately.

Related Work

This research continues the work in [START_REF] Fu | Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for java[END_REF] that addresses the general issue of lifting numeric domains to heap-manipulating programs.

Memory abstraction using strong and weak updates [START_REF] Chase | Analysis of pointers and structures (with retrospective)[END_REF][START_REF] Wilson | Efficient Context-Sensitive Pointer Analysis for C Programs[END_REF] is common sense. Efforts have been made to enable safe application of strong update. Sagiv et al. used the focus operation (that isolates individual elements of the summarized dimensions) of shape analysis [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF] to apply strong update. Fink et al. [START_REF] Fink | Effective typestate verification in the presence of aliasing[END_REF] used a uniqueness analysis based on must-alias and liveness information to facilitate the verification of whether a summarized node represents more than one concrete reference.

The recency abstraction [START_REF] Balakrishnan | Recency-abstraction for heap-allocated storage[END_REF]) is a simple and elegant technique that enables strong update by distinguishing the objects recently allocated from those created earlier. This approach allows strong update to be applied whenever a write access immediately follows an allocation, which is usually the case for initialization. Although the objective of recency abstraction is similar to targeted update, it uses a different abstraction that is not comparable to ours.

The issue of strong/weak update has been mostly studied for array structures. [START_REF] Cousot | A scalable segmented decision tree abstract domain[END_REF] proposed an efficient solution based on the ordering of array indexes. It may be not easy to generalize their method to the analysis of the pointer access. Fluid update [START_REF] Dillig | Fluid updates: Beyond strong vs. weak updates[END_REF] is much closer to our approach. It is an abstract semantics that provides a sharp analysis for the array structure. The authors used bracket constraints to refine points-to information on arrays, which was shown to be effective to disambiguate array indexes. This approach was also extended in [START_REF] Dillig | Precise reasoning for programs using containers[END_REF] to deal with containers and other non-array structures.

Conclusion

Targeted update introduces a novel dimension in program analysis for tuning precision and efficiency. We have derived the abstract semantics from the concept of targets. This approach is validated on the benchmark suite SPECjvm98. The experimental results show a tangible precision enhancement compared with classical approaches while preserving a high scalability.

By "being sound", we always refer to the partial soundness, i.e., if P terminates, then (31) holds.

B Definitions for p(•) and p ♯ (•)

Here, we give the precise definitions of the operators that resolve access paths. In the following, we use p and p ♯ for elements of Pter and Pter ♯ respectively. Definition 5. Let p = (p env , p hp ). We say an access path u ∈ Path p resolves to a reference r, or the reference can be reached by the access path following p, if one of the following rules is satisfied.

u = x p env (x) = r p(u) = r u = u ′ .f p(u ′ ) = r p hp (r ′ , f ) = r p(u) = r (32)
Similar to the notation p(u), we write p ♯ (u) for the resolved abstract references of u ∈ Path p , called the points-to set of u under p ♯ . Let p ♯ = (p ♯ env , p ♯ hp ), p ♯ (u) is defined to be the smallest set satisfying:

u = x h ∈ p ♯ env (x) h ∈ p ♯ (u) u = u ′ .f h ′ ∈ p ♯ (u ′ ) h ∈ p ♯ hp (h ′ , f ) h ∈ p ♯ (u) ( 33
)
For a numeric access path in the form of u p .f n , with u p ∈ Path p and f n ∈ Fld n , the definitions above can be extended as: For example, if a variable x resolves to r under p ∈ γ p (p ♯ ) and h is an abstraction of r, then h must be in the points-to set of x.

D Concrete semantics of Imp np

As a shortcut, we set Below we write n[d := n(x n )] to represent a mapping that is as n except that at d it takes the value of n(x n ); we write ins -1 for the inverse of ins. (Without loss of generality, we assume that ins is bijective, since it has to be injective) It suffices to prove -

D = Ref × Fld n (

Fig. 1 :

 1 Fig. 1: Memory state before statement y.f = 7

  For a given set U , the notation U ⊥ represents the disjoint union U ∪ {⊥}. Given a mapping m ∈ A → B ⊥ , we express the fact that m is undefined in a point x by m(x) = ⊥. We write post[m] ∈ ℘(A) → ℘(B) for the mapping λA 1 .{b | ∃a ∈ A 1 : m(a) = b}.

Pter-→

  (s p )p) is in the concretization of (n ♯ ′, [|s p |] ♯ p (p ♯ )). The hypothesis (n, p) ∈ γ T (n ♯ , p ♯ ) states that n |= [ins]n ♯ for any ins ∈ Ins p T ; for the sake of soundness, the updated n ♯ ′ has to satisfy n |= [ins]n ♯ ′ for any ins ∈ Ins Pter -→(sp)p T . Following Def. 3, it suffices to unconstrain all summarized dimensions of n ♯ ′ in the form of ⊲(d) with d ∈ post[ Pter -→ (s p )p](T )\post[p](T ). Let M post[ Pter -→ (s p )p](T ) ∩ post[p](T ). We can show that M ⊇ {p(t) | t ∈ T, t does not have l as prefix}. This is because for any p(t) such that t ∈ T and t does not have l as prefix, p(t) ∈ post[p](T ) immediately implies p(t) ∈ post[ Pter -→ (s p )](T ).

  Fig. 2: A Java program

  p(u p .f n ) = p(u p ), f n (34) p ♯ (u p .f n ) = {δ h,fn | h ∈ p ♯ (u)}(35)C Definition of γ p Definition 6. The semantics of points-to graph is defined through the concretization function γ p ∈ Pter ♯ → ℘(Pter ):γ p (p ♯ ) {p ∈ Pter | ∀u ∈ Path p , ∀r ∈ Ref : p(u) = r ⇒ ⊲(r) ∈ p ♯ (u)} (36)

  37) and use meta-variable d to range over the pairs in D. In Fig. 3, we show the Structural Operational Semantics (SOS) of Imp np , denoted by -→ ♮ . It is expressed by Pter the figure extended over D ∪ Var n ).

[

  ins -1 ](n[d := n(x n )]) |= [|δ = x n |] η(δ) (n ♯ ) (39)We make two cases following whether ins maps δ to d. Subsequently, the left hand side of the proof goal (39) is denoted by lhs.-Case I: If ins maps δ to d, lhs can be written as ([ins -1 ]n)[δ := n(x n )].Since [ins -1 ]n |= n ♯ by assumption, we obtain lhs |= [|δ = x n |]

  Var τ numeric/pointer variables fτ , gτ ∈ Fld τ numeric/pointer fields uτ , vτ ∈ Pathτ numeric/pointer access paths sn ∈ Imp n

	k ∈ I	scalar numbers
	r ∈ Ref	concrete references
	xτ , yτ ∈

  ♯ and s p ∈ Imp p , p |= p ♯ ⇒

	abstract state is called a points-to graph. The concretization function
	γ p : Pter ♯ → ℘(Pter ) specifies the semantics of points-to graph. The abstract
	semantics [|•|]	♯ p is assumed to be sound with regard to the concrete	Pter -→: For any
	p, p Pter -→ (s p )(p) ∈ γ p • [|s p |]	♯ p (p ♯ ).

  Thus, a state is a pair (n, p) where n can be regarded as a concrete state of Imp n over Var n ∪ (Ref × Fld n ), and p as a concrete state of Imp p . In Sect. D, we express the concrete semantics of Imp np , denoted by -→ ♮ , via

	Num -→ and

Pter

-→.

Example 1. Consider the following program:

  and n is in the concretization of [ins]n ♯ where ins is called an instantiation mapping summarized dimensions to concrete d ∈ D that are pointed to by the targets T .Below, we present the abstract semantics of statements in Imp np , called targeted update.

4 Targeted Update -the case of write access y p .f n = x n Algorithm Targeted update uses two operators: The local strong update operator [|δ = x n |]

  Algorithm 1: Targeted update for y p .f n = x n Input: Abstract state (n ♯ , p ♯ ), targets T Output: The abstract state after targeted update [|yp.fn = xn|] ♯ T

Table 1 :

 1 Evaluation of targeted update on the benchmark suite SPECjvm98: Interval + Spark number of the write access statements after which the obtained invariants are strictly more precise than Num. Improvement on scalar variables is assessed by the number of read-access statements after which the obtained numeric invariant by T-NumP is strictly more precise than Num in terms of scalar variables (summarized dimensions are unconstrained for this comparison). The execution time is measured for Num, Pter, and T-NumP (col. 8-10). The parameters T Num and T Pter are the times spent by Num and Pter when they analyze individually. The parameter T TNUMP records the time of our analysis.The last four columns compute the metrics for assessment. The metrics Q TU TU/WA and Q PRCS PRCS/WA

	Benchmark Characteristics	Precision	Time		Metrics
	BENCHMARK STATEMENT WA RA TU PRCS SCALAR T NUM T PTER T TNUMP Q TU Q PRCS Q SCALAR Q T
	200 check	2307 25 48 19	18	6 00m12s 02m36s	03m13s 76%	72%	13% 115%
	201 compress	2724 96 142 89	55	9 00m07s 02m39s	03m34s 93%	57%	6% 129%
	202 jess	12834 232 646 212	102	2 00m16s 02m43s	05m02s 91%	44%	0% 169%
	205 raytrace	5465 53 64 52	24	0 00m05s 02m35s	03m35s 98%	45%	0% 134%
	209 db	2770 32 65 31	19	0 00m04s 02m41s	03m47s 97%	59%	0% 138%
	213 javac	25973 342 1362 312	143	25 00m12s 04m15s	10m12s 91%	42%	2% 229%
	222 mpegaudio	14604 138 247 124	62	6 00m18s 02m50s	04m15s 90%	45%	2% 136%
	227 mtrt	5466 53 64 52	24	0 00m06s 02m40s	03m42s 98%	45%	0% 134%
	228 jack	12221 462 414 436	102	7 00m31s 02m45s	06m03s 94%	22%	2% 185%
	999 checkit	3038 38 53 29	19	0 00m05s 02m38s	03m44s 76%	50%	0% 137%
	Mean				90%	48%	3% 151%

Table 2 :

 2 Evaluation of targeted update on the benchmark suite SPECjvm98: Octagonal + Spark

	Benchmark Characteristics	Precision	Time		Metrics
	BENCHMARK STATEMENT WA RA TU PRCS SCALAR T NUM T PTER T TNUMP Q TU Q PRCS Q SCALAR Q T
	200 check	2307 25 48 19	19	6 00m13s 02m44s	03m48s 76%	76%	13% 129%
	201 compress	2724 96 142 89	93	70 00m09s 03m18s	05m16s 93%	97%	49% 153%
	202 jess	12834 232 646 212	215	52 00m36s 02m46s	06m38s 91%	93%	8% 197%
	205 raytrace	5465 53 64 52	52	8 00m10s 02m38s	03m52s 98%	98%	13% 138%
	209 db	2770 32 65 31	31	13 00m08s 02m42s	03m51s 97%	97%	20% 136%
	213 javac	25973 342 1362 312	244	156 02m35s 05m31s	14m28s 91%	71%	11% 179%
	222 mpegaudio	14604 138 247 124	117	36 00m39s 02m45s	06m44s 90%	85%	15% 198%
	227 mtrt	5466 53 64 52	52	8 00m21s 02m37s	03m58s 98%	98%	13% 134%
	228 jack	12221 462 414 436	410	168 00m34s 02m43s	08m06s 94%	89%	41% 247%
	999 checkit	3038 38 53 29	28	6 00m09s 02m52s	04m46s 76%	74%	11% 158%
	Mean				90%	88%	19% 167%

  Case II: If ins does not map δ to d, we can then prove lhs |= n ♯ . This is because variable d does not appear in the free variables of n ♯ . (To be more clear, we always have, for any n, n ♯ : n |= n ♯ ⇒ n ′ |= n ♯ with n ′ being n restricted to the free variables of n ♯ . For example, {x → 2, y → 3} |= {x ≥ 0} ⇒ {x → 2} |= {x ≥ 0}.) Following Lem. 1, if (TU ) holds, the second case can be ruled out. If (TU ) is not satisfied, we have to join the two cases, obtaining lhs |= [|δ = x n |]

♯ n (n ♯ ) ⊔ n ♯ . ⊓ ⊔

⋆ In addition to research facilities granted by IMDEA Software, this work has also received financial support from AX -L'Association des Anciens Élèves et Diplômés de l' École polytechnique at 5, rue Descartes 75005 Paris.

Dealing with δ in different orders could have an influence on precision, but this point is not studied in the paper.

The Jimple statements are generally less than in the source program, because SOOT typically analyzes a subset of its call-graph nodes.

Acknowledgments. The author wishes to thank Laurent Mauborgne for his thoughtful feedback.

A Elements of Abstract Interpretation

Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is a theory of semantic approximation. The semantics of a program P can often be expressed by the least fixpoint lfp t [|P |] of a transfer function t [|P |] over a partial ordered set (A, ⊑), called the semantic domain. There may be different choices for the transfer function and semantic domain, depending on the level of precision we want to describe the program. In general, we have a very precise semantics (A ♮ , ⊑ ♮ ), that describes exactly what a program does, called the concrete semantics, and a less precise but computable semantics (A ♯ , ⊑ ♯ ), called the abstract semantics. The soundness of the abstract semantics is described using a concretization function γ : A ♯ → A ♮ , giving the meaning of the abstract elements in terms of concrete elements. We say that the abstract semantics lfp t ♯ [|P |] is sound with respect to the concrete semantics lfp t ♮ [|P |], or say that the latter is approximated by the former,

In this paper, we frequently verify a stronger soundness condition in the form of

E Analysis Results for the Example in Sect. 7

Here, we show the analysis results of the example program in Fig. 2. The results are shown in Tab. 3. Column left shows the inferred constraints before each control point. Column right shows the Jimple statements. The part starting with "//" is our comments. In the constraints, δ i for i = 1, 2 corresponds to δ hi,val of the example in Sect. 7. In the Jimple statements, r 2 (resp. r 3 ) corresponds to variables hd (resp. node) in the original program.

Table 3: Analysis results for the program in Fig. 2.

F Proof Sketch of Thm. 1

Here, we give the proof sketch of Thm. 1.

Proof. Take an arbitrary (n, p) ∈ γ T (n ♯ , p ♯ ), δ ∈ p ♯ (y p .f n ), ins ∈ Ins p T . Let d = p(y p .f n ). We prove a stronger condition:


Messaoud Rahim
email: rahimmes@yahoo.fr

Ahmed Hammad
email: ahmed.hammad@femto-st.fr

Malika Ioualalen
email: mioualalen@usthb.dz

Modular and Distributed Verification of SysML Activity Diagrams

Keywords: SysML, Activity diagram, Places bordered Petri nets, Distributed Model-Checking

Model-based development for complex system design has been used to support the increase of systems complexity. SysML is a modeling language that allows a system description with various integrated diagrams, but SysML lacks formality for the requirement verification. Translating SysML-based specification into Petri nets allows to enable rigorous system analysis. However, for complex systems, we have to deal with the state space explosion problem. In this paper, we propose new approach to allow a modular and distributed verification of SysML Activity Diagram basing on the derived Petri net.

Introduction

The System Modeling Language (SysML) is UML profile that can be used to specify graphically all aspects of complex systems [START_REF] Friedenthal | Omg systems modeling language (omg sysml) tutorial[END_REF]. Nevertheless, despite the various advantages of SysML, it remains a semi-formal language without possibilities of formally verifying the models described by it. Industrial safety-related standards strongly recommend the use of formal methods to validate critical systems. For that purposes, it is needed to use SysML in conjunction with formal method to provide formal verification of the specified system. Several approaches based on mapping SysML behavioural diagrams to Petri nets have been proposed [START_REF] Carneiro | Mapping sysml state machine diagram to time petri net for analysis and verification of embedded realtime systems with energy constraints[END_REF][START_REF] Andrade | A methodology for mapping sysml activity diagram to time petri net for requirement validation of embedded real-time systems with energy constraints[END_REF][START_REF] Linhares | Introducing the modeling and verification process in sysml[END_REF]. The aim of these approaches was to provide a way to verify the specified system with a Model checking technique. However, in the case of complex systems, we have to deal with the state space explosion problem to analyse the resulting Petri net. A way to overcome the state space explosion is the use of modular analysis. Another way that had gained interest, in the recent years is the use of distributed processing [START_REF] Kristensen | An approach to distributed state space exploration for coloured petri nets[END_REF][START_REF] Saad | A general lockfree algorithm for parallel state space construction[END_REF][START_REF] Barnat | Shared hash tables in parallel model checking[END_REF]. In this paper, we propose a global approach for performing a modular and distributed verification of the SysML activity diagram. Basing on composite activities, we derive places-bordered Petri net module for each activity. The verification of the system can concern only one simple activity or the global SysML activity diagram. For the second case, and in order to deal with the state space explosion problem, we propose to adapt the distributed verification process using a cluster of computing nodes [START_REF] Boukala | Distributed verification of modular systems[END_REF][START_REF] Abid | A distributed verification approach for modular petri nets[END_REF] for verifying the derived modular Petri net. For mapping a SysML activity diagram into places-bordered Petri net, we propose a translation rule for the call behavior action. The translation of the other basic SysML activity constructs is inspired from previous works.

The rest of this paper is organized as follows: in Section 2, we discuss related works. In Section 3, we present the SysML activity diagram. In Section 4, we give a definitions of places bordered Petri net. In section 5, we present the mapping technique. We present the modular and distributed verification process in Section 6. Finally, in Section 7, we conclude and we outline some ideas for future works.

Related Works

The most proposed approaches concerning the formal specification of SysML diagrams have used Petri net models due to their expressiveness and formality [START_REF] Linhares | Introducing the modeling and verification process in sysml[END_REF][START_REF] Carneiro | Mapping sysml state machine diagram to time petri net for analysis and verification of embedded realtime systems with energy constraints[END_REF][START_REF] Andrade | A methodology for mapping sysml activity diagram to time petri net for requirement validation of embedded real-time systems with energy constraints[END_REF]. To our knowledges, this work is the first that considers the composite structure of the SysML activity diagram for a verification purposes. The composite and modular verification approaches aim to take benefit from some information about the components of the system and the way they communicate. Modular Petri nets as presented in [START_REF] Christensen | Modular analysis of petri nets[END_REF] allow designers to specify a system as communicating modules. Modules communicate using shared transitions or fusion places. The work presented in [START_REF] Valmari | Compositional analysis with placebordered subnets[END_REF] proposes a compositional verification method for Petri net composed of place bordered subnets. The verification approach used in this work is based on Model checking technique. However, for complex system, we have to overcome the state space explosion problem. Several recent approaches use distributed processing environments to extend the size of the state space to be constructed [START_REF] Boukala | Distributed verification of modular systems[END_REF]. This work proposes to adapt these approaches combined with a modular analysis to verify a SysML activity diagrams.

The SysML Activity diagram

In SysML(?), an activity is a formalism for describing behaviour that specifies the transformation of inputs to outputs through a controlled sequence of actions. The basic constructs of an activity are actions and control nodes as illustrated in Figure 1. Actions are the building blocks of activities, each action can accept inputs and produces outputs, called tokens. These tokens can correspond to anything that flows such as information or physical item (e.g., water, signal). Control nodes include fork, join, decision,

Places-bordered Petri nets

Formally a Petri net is [START_REF] Valmari | Compositional analysis with placebordered subnets[END_REF]: Definition 1. A Petri net is triplet: PN = (P, T,W ). Where: P is finite set of places, T is finite set of transitions, (P ∩ T = / 0) and W : (PXT ) ∪ (T XP) → N is a weight function, W (p,t) (resp. W (t, p)) gives the weight of the arc from p to t (resp. from t to p).

Usually, an initial marking is associated with the Petri net: Definition 2. A marked Petri net (PN, M 0 ), is a Petri net PN with an initial marking M 0 : P → N. The initial marking of a place p ∈ P is M 0 (p).

To compose a large Petri net from smaller pieces, we define a places-bordered Petri [START_REF] Valmari | Compositional analysis with placebordered subnets[END_REF]. A places-bordered Petri net modules interface with each other via common places, called border places.

Definition 3. A places-bordered Petri net module is the 4-tuple NC = (P, T,W, B). where : P, T , and W are as in a Petri net, B ⊆ P is the set of border places.

The mapping technique

Mapping initial and final nodes

Mapping routing object flows

For mapping a fork node 4 we use a transition t A f ork that represents the split operation with out A as input place and in B with in C as output places. For mapping a join node 4 we use a transition t AB join that represents the synchronisation between out A and out B as input places and in C as output place.

Mapping call behavior action

To map A call behavior action we consider that the invoked activity is already mapped into places bordered Petri net module. As presented in Figure 5, the mapping of a call behavior action A that invokes an activity Act with one input and one output flow is places bordered Petri net module which has in act, en Act, out Act and end Act as border places with the Petri net module that represents the calling activity. The transition t Abact is used to pass all input flows of the call behavior action to the invoked activity and to enable its execution. When the called activity terminates, we use the transition t Aeact to pass all output flows of the invoked activity to the call behavior action. As described in the mapping technique, the resulting Petri net is set of place bordered Petri net modules. Modular verification is enabled by the fact that each Petri net module specifies the behavior of an activity. A simple activity can be verified by using only its related Petri net module. For verifying a composite activity we have to use its related Petri net module and all the Petri net modules corresponding to their call behavior actions. A modular and distributed verification can be used to perform the analysis of a complex composite activities. The main step in the model-checking is the construction of the state space. In order to construct the state space of the Petri net derived from the SysML activity diagram we decompose the state space construction problem into a number of distributed tasks. The decomposition is guided by the SysML activities. The approach we propose is parallel objects based [START_REF] Kale | Charm++ and ampi: Adaptive runtime strategies via migratable objects[END_REF]. For constructing the state space, we use one main task to initialize the state space construction process, and a set of parallel tasks which we call activity tasks to explore and store the state space. Activity tasks are used to encode a place bordered Petri net modules. Each Petri net module is assigned to an activity task which explores independently the internal states of the module. Activity tasks encapsulate informations about transitions and border places. They perform the exploration of a given state, the storing of internal successors state, seek for previously explored states and invoke the storing of external states.

Each activity task encapsulates a hash table that is used to store a fragments of the state space. From a logical point of view, we consider all the processing nodes as a unique computing node. The activity tasks are viewed as an arrays of parallel Tasks. Physically, all the tasks are mapped over the physical nodes. The mapping is done when we create the tasks. The Figure 6 presents an example using four (4) computing nodes to illustrate the logical and the physical architecture of the distributed application. The state space is the basic model on which most verifications are built. The constructed state space is modular. It can be used to verify behavioural properties in the hole activity diagram or just on some activities. The properties to verify can be basic such as reachability, deadlocks, liveness and home state. We can adopt the approach presented in [START_REF] Boukala | Distributed verification of modular systems[END_REF] to verify such properties in the distributed and modular state space. Functional properties have to be extracted and translated from the SysML requirements diagram to temporal logic such as LTL and CTL. Various works have been proposed to verify LTL and CTL formulas in distributed and modular state space [START_REF] Christensen | Modular analysis of petri nets[END_REF][START_REF] Latvala | Ltl model checking for modular petri nets[END_REF].

Conclusion

The paper presents a modular and distributed verification approach for formally verifying complex systems described by SysML activity diagrams. A technique for mapping the SysML activities to Petri net have been proposed. The mapping is guided by the call behavior actions. The modular verification is enabled by analysing each activity using its related Petri net module. For enabling the verification of complex and composite activities a modular and distributed verification technique have been proposed to overcome the state space explosion problem. As future works, it is important to consider the process of extracting properties as temporal logic formulas from the SysML requirement diagram to complete the approach presented in this paper.

Figure 1 :

 1 Figure 1: Activity diagram basic constructs merge, initial, activity final, and flow final. A call behavior action permits to invoke an activity when it starts, and passes the tokens from its input pins to the input parameter nodes of the invoked activity.

  Basing on the previous works that propose a mapping of UML and SysML activity diagram to Petri nets (N.[START_REF] Yang | Mapping uml activity diagrams to analyzable petri net models[END_REF][START_REF] Andrade | A methodology for mapping sysml activity diagram to time petri net for requirement validation of embedded real-time systems with energy constraints[END_REF][START_REF] Staines | Intuitive mapping of uml 2 activity diagrams into fundamental modeling concept petri net diagrams and colored petri nets[END_REF], our technique defines a mapping for the call behavior actions and propose to map the SysML activity diagram to modular Petri net with border places. The mapping we propose is activity based decomposition. The decomposition is guided by the call behavior actions which permits to facilitate the mapping of a SysML activity diagram even it includes several composite activities. The Petri net derived from the SysML activity diagram is a set of places-bordered Petri net modules, each one represents an activity instance.

  Initial node represents the start point of an activity. As illustrated in figure 2, to map the initial node, we use one transition (t in Act) with one input place and two output places. The input place (en Act) is used to enable the execution of the activity. The first output place (on Act) is used to indicate that we are executing the activity and the second output place (Ctl out) is used to represent the control flow. Activity final represents the end point of an activity. As illustrated in figure2, to map final node, we use one transition (t out Act) with two input places and one output place. The first input place (on Act) represents that we are executing the activity and the second input place (Ctl in) represents the output flow enabling the termination of the activity. The output place (end Act) is used to indicate that the activity is terminated.

Figure 2 :

 2 Figure 2: Mapping initial and final activity node

Figure 3 :

 3 Figure 3: Mapping simple action and Object flows between actions

Figure 4 :

 4 Figure 4: Mapping join and fork nodes

Figure 5 :

 5 Figure 5: Mapping call behavior action

Figure 6 :

 6 Figure 6: Logical and physical view of the application architecture