Mauricio Cano

Jaime Arias

Jorge A Pérez

Session-based Concurrency, Reactively

This paper concerns formal models for the analysis of communication-centric software systems that feature declarative and reactive behaviors. We focus on session-based concurrency, the interaction model induced by session types, which uses (variants of) the π-calculus as specification languages. While well-established, such process models are not expressive enough to specify declarative and reactive behaviors common in emerging communication-centric software systems. Here we propose the synchronous reactive programming paradigm as a uniform foundation for session-based concurrency. We present correct encodings of session-based calculi into ReactiveML, a synchronous reactive programming language. Our encodings bridge the gap between process specifications and concurrent programs in which session-based concurrency seamlessly coexists with declarative, reactive, timed, and contextual behaviors.

A Motivating Example

We use a toy example to illustrate (i) the limitations of session π-calculi in representing structured communications with declarative/reactive behaviors, and (ii) how our approach, based on encodings into ReactiveML, can neatly overcome such limitations. A Ride Protocol Suppose a conference attendee who finds himself in a foreign airport. To get in time for his presentation, he uses a mobile app in his phone to request a ride to the conference venue. The intended protocol may be intuitively described as follows:

Introduction

In this paper, we introduce the synchronous reactive programming paradigm as a practical foundation for communication-centric software systems. Our motivation is twofold. First, synchronous reactive programming allows us to uniformly integrate point-to-point communications (as in the π-calculus) with declarative, reactive, timed, and contextual behaviors-this is an elusive combination for process models such as the π-calculus. Second, by relying on ReactiveML (a synchronous reactive programming language with a formal semantics), we may bridge the gap between π-calculus processes and actual concurrent programs, thus bringing a rigorous communication model to programmers.

Large software systems are deployed as aggregations of distributed interacting components, which are built using a myriad of different programming platforms and/or made available as black-boxes that expose minimal interaction interfaces. In these complex, heterogeneous systems communication emerges as the key unifying glue. Certifying that interacting components conform to their prescribed protocols is thus an important but challenging task, and is essential in ensuring overall system correctness.

Besides protocol conformance, analyzing communication-centric software systems entails addressing additional challenges, which can be seen as related to the increasing ubiquity of these systems. Indeed, communication-centric software appears in emerging trends (e.g., collective adaptive systems) and as such is subject to various classes of requirements that are orthogonal to communication correctness. We focus on communication-centric software systems featuring declarative, reactive, timed, and contextual behaviors. (In §2 we illustrate these intended systems, using a transactional protocol subject to failures.) By stipulating governing conditions (rather than how to implement such conditions), declarative approaches naturally specify, e.g., security policies. Closely intertwined, constructs modeling reactivity, time, and context-awareness are at the heart of mechanisms that enforce, e.g., self-adaptation and fault-tolerance in dependable systems. Therefore, while not directly connected to protocol specifications, declarative, reactive, timed, and contextual behaviors (and their interplay) do influence communication and should be integrated into the analysis of protocol conformance.

Process calculi (such as the π-calculus [START_REF] Milner | A calculus of mobile processes[END_REF]) have long offered a principled basis for the compositional analysis of message-passing programs. Within these approaches, our work concerns session-based concurrency, the interaction model induced by session types [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF], which organize protocols as sessions between two or more participants. In session-based concurrency, a session type describes the contribution of each partner to the protocol. Interactions are structured, and always occur in matching pairs; e.g., when one partner sends, the other receives; when one partner offers a selection, the other chooses. Different session type theories for binary (two-party) and multiparty protocols have been developed [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]; here we focus on binary sessions.

Binary and multiparty session types rely on π-calculi with session constructs. These session calculi have been extended with declarative, reactive, timed, and contextual behaviors, but none of these extensions captures all these features. For instance, session calculi with assertions (logical predicates) [START_REF] Bonelli | Correspondence assertions for process synchronization in concurrent communications[END_REF][START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF] may describe certain declarative requirements, but do not account for reactive and contextual behaviors. Frameworks with time-related conditions, such as [START_REF] Bocchi | Timed multiparty session types[END_REF][START_REF] Bartoletti | Compliance and subtyping in timed session types[END_REF], have similar limitations. The framework in [START_REF] Kouzapas | On asynchronous eventful session semantics[END_REF] supports contextual information through events, but does not represent reactive, declarative behaviors. Integrating these extensions into a single process framework seems rather difficult, for they rely on different languages and often conflicting assumptions.

Here we pursue a different approach: we embed session-based concurrency within the synchronous reactive programming (SRP) model for reactive, timed systems [START_REF] Benveniste | The synchronous languages 12 years later[END_REF][START_REF] Halbwachs | Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE[END_REF]. Hence, rather than extending session π-calculi with declarative, reactive, timed, and contextual features, we encode session-based communication into a setting where these features (and their interplay) are already well understood. We consider ReactiveML, a programming language based on SRP [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF][START_REF] Mandel | ReactiveML, ten years later[END_REF], as target language in our developments. ReactiveML is a general purpose functional language with a well-defined formal semantics. Our technical contributions are two correct encodings of session π-calculi into ReactiveML. In a nutshell, we use signals in ReactiveML to mimick names in session π-calculi. Our encodings enable us to integrate, in a seamless and uniform way, session-based constructs as "macros" in ReactiveML programs with declarative and reactive constructs. Moreover, since our encodings are executable (well-typed) Reac-tiveML programs, our results have a direct practical character, which serves to bridge the gap between specifications in process models and actual concurrent programs.

This paper is structured as follows. §2 illustrates our approach via an example. §3 summarizes the syntax and semantics of a session π-calculus and of ReactiveML. In both cases, we consider languages with synchronous and asynchronous (queue-based) communication. §4 presents our two encodings and states their correctness. §5 collects closing remarks. An online appendix includes further examples and technical details (omitted definitions and proofs) [START_REF] Cano | Session-based Concurrency, Reactively (Extended Version)[END_REF].

1. Attendee sends his current location and destination to a neighbouring Driver. 2. Driver receives these two pieces of information and offers three options to Attendee: a ride right now, a ride at a later time, or to abort the transaction. 3. Attendee is in a hurry, and so he selects to be picked up right now. 4. Driver replies by sending an estimated arrival time at Attendee's location.

Using session π-calculus processes (as in, e.g., [START_REF] Vasconcelos | Fundamentals of session types[END_REF]), this protocol may be implemented as a process S = (νxy)(A(x) | D(y)), where processes A(x) and D(y), abstract the behavior of Attendee and Driver as follows:

A(x) = x loc .x des .x now.x(e).0 D(y) = y(l).y(d).y {now : y eta .0 , later : y(t).y ok .0 , quit : Close y } where process Close y denotes an unspecified sub-protocol for closing the transaction. Above, we write x z .P (resp. x(w).P ) to denote the output (resp. input) along name x with continuation P . Processes x l.P and x {l i : P i } i∈I denote internal and external labeled choices, respectively. Above, now, later, and quit denote labels. Process 0 denotes inaction. Process (νxy)P declares x and y as dual session endpoints in P . This way, S says that A(x) and D(y) play complementary roles in the session protocol. The Need for Richer Behaviors Session-based concurrency assumes that once a session is established, communication may proceed without interruptions. This is unrealistic in most real-life scenarios, where established sessions are prone to failures or interruptions. For instance, a connectivity issue in the middle of the protocol with Driver may leave Attendee stuck in the airport. In such cases, notions of contextual information, reactivity, and time become essential: Contextual Information such as, e.g., external events signalling a malfunction, allows relating the system with its environment. For instance, we may like to relate A(x) and D(y) with a connectivity manager that triggers warning events. Reactivity serves to detect unforeseen circumstances (e.g., failures) and to define appropriate system behaviors to run in such cases. For instance, we may like to define A(x) so that another driver is requested if a failure in a protocol with D(y) arises. Time allows to track the instant in which a failure occurred, and also to establish a deadline within which the failure should be resolved. For instance, in case of failure A(x) may try contacting alternative drivers only until k instants after the failure.

As mentioned above, the session π-calculus does not support these features, and proposed extensions do not comprehensively address them. We rely on synchronous reactive programming (SRP) and ReactiveML, which already have the ingredients for seamlessly integrating declarative, reactive behavior into session-based concurrency.

ReactiveML ReactiveML extends OCaml with reactive, timed behavior. We illustrate • f by revisiting our example above. Let us define a concurrent reactive program in which A(x) f , D(y) f , and D (w) f represent ReactiveML snippets that implement session-based communication. We consider a simple possibility for failure: that Driver (D(y)) may cancel a ride anytime or that communication with Attendee (A(x)) fails and cannot be recovered. Ideally, we would like a new driver D (w), whose implementation may be the same as D(y), to continue with the protocol, without disrupting the protocol from the perspective of A(x). This could be easily expressed in ReactiveML as the expression S = signal w 1 , w 2 in (RA RD) where:

RA = do ( A(x) {x←w1} ) until f ail → (await w 2 (z) in A(x) {x←z} ) RD = do ( D(y) {y←w1} ) until f ail → (BD) BD = signal w 3 in (emit w 2 w 3 ; D (w) {w←w3} )
S declares two signals: while signal w 1 connects a reactive attendee RA and the reactive driver RD, signal w 2 connects RA with a backup driver BD. If no failure arises, RA and RD run their expected session protocol. Otherwise, the presence of signal f ail will be detected by both RA and RD: as a result, the attendee will await a new signal for restarting the session; process D(y) stops and BD will become active in the next instant. After emitting a fresh signal w 3 , BD can execute the protocol with RA.

Preliminaries

A Session π-calculus Our presentation follows closely that of [START_REF] Vasconcelos | Fundamentals of session types[END_REF]. We assume a countable infinite set of variables V s , ranged over by x, y, . . .. A variable represents one of the two endpoints of a session. We use v, v , . . . to range over values, which include variables and the boolean constants tt, ff. Also, we use l, l , . . . to range over labels. We write x to denote a finite sequence of variables (and similarly for other elements).

Definition 1 (π). The set π of session processes is defined as:

P, Q ::= x v .P | x(y).P | x l.P | x {l i : P i } i∈I | v? (P ) : (Q) | P | Q | 0 | (νxy)P | * x(y).P
Process x v .P sends value v over x and then continues as P ; dually, process x(y).Q expects a value v on x that will replace all free occurrences of y in Q. Processes x l j .P and x {l i : Q i } i∈I define a labeled choice mechanism, with labels indexed by the finite set I: given j ∈ I, process x l j .P uses x to select l j and trigger process

Q j . COM (νxy)(x v .P | y(z).Q) -→ (νxy)(P | Q{ v /z}) SEL (νxy)(x lj.P | y {li:Qi}i∈I ) -→ (νxy)(P | Qj) (j ∈ I) REP (νxy)(x v .P | * y(z).Q) -→ (νxy)(P | Q{ v /z} | * y(z).Q) IFT tt? (P ) : (Q) -→ P IFF ff? (P ) : (Q) -→ Q Fig. 1.
Reduction relation for π processes (contextual congruence rules omitted).

We assume pairwise distinct labels. The conditional process v? (P ) : (Q) behaves as P if v evaluates to tt; otherwise it behaves as Q. Parallel composition and inaction are standard. We often write

n i=1 P i to stand for P 1 | • • • | P n .
The double restriction (νxy)P binds together x and y in P , thus indicating that they are the two endpoints of a session. Process * x(y).P denotes a replicated input process, which allows us to express infinite server behaviors. In x(y).P (resp. (νyz)P ) occurrences of y (resp. y, z) are bound with scope P . The set of free variables of P , denoted fv(P ), is as expected.

The operational semantics for π is given as a reduction relation -→, the smallest relation generated by the rules in Fig. 1. Reduction expresses the computation steps that a process performs on its own. It relies on a structural congruence on processes, denoted ≡ S , which identifies processes up to consistent renaming of bound variables, denoted ≡ α . Formally, ≡ S is the smallest congruence that satisfies the axioms:

P | 0 ≡ S P P | Q ≡ S Q | P P ≡ S Q if P ≡ α Q (P | Q) | R ≡ S P | (Q | R) (νxy)(νwz)P ≡ S (νwz)(νxy)P (νxy)0 ≡ S 0 (νxy)P | Q ≡ S (νxy)(P | Q) if x, y ∈ fv(Q)
We briefly comment on the rules in Fig. 1. Reduction requires an enclosing restriction (νxy)(• • • ); this represents the fact that a session connecting endpoints x and y has been already established. Rule COM represents the synchronous communication of value v through endpoint x to endpoint y. While Rule SEL formalizes a labeled choice mechanism, in which communication of a label l j is used to choose which of the Q i will be executed, Rule REPL is similar to Rule COM , and used to spawn a new copy of Q, available as a replicated server. Rules IFT and IFF are self-explanatory. Rules for reduction within parallel, restriction, and ≡ S (not given in Fig. 1) are as expected.

The following notion will be useful in stating properties of our translations.

Definition 2 (Contexts for π). The syntax of (evaluation) contexts in π is given by the following grammar:

E ::= [•] | E | P | P | E | (νxy)(E)
, where P is a π process and

'[•]' represents a 'hole'. We write C[•] to range over contexts (ν x y)([•] | P 1 | . . . | P n ), with n ≥ 1. E[P ] (resp. C[P ]
) will denote the process obtained by filling [•] with P .

An Asynchronous Session π-calculus (aπ) Following [START_REF] Kouzapas | On asynchronous eventful session semantics[END_REF], we now define aπ, a variant of π with asynchronous (queue-based) semantics. The syntax of aπ includes variables x, y, . . . and co-variables, denoted x, y. Intuitively, x and x denote the two endpoints of a session, with x = x. We write V a to denote the set of variables and covariables; k, k will be used to range over V a . As before, values include booleans and variables. The syntax of processes is as follows:

SEND x v .P | x[i : m1, o : m2] -→A P | x[i : m1, o : m2 • v] SEL x l.P | x[i : m1, o : m2] -→A P | x[i : m1, o : m2 • l] COM x[i : m1, o : m • m2] | x[i : m1, o : m2] -→A x[i : m1, o : m2] | x[i : m1 • m, o : m2] RECV x(y).P | x[i : v • m1, o : m2] -→A P { v /y} | x[i : m1, o : m2] BRA x {li : Pi}i∈I | x[i : lj • m1, o : m2] -→A Pj | x[i : m1, o : m2] (j ∈ I) IFT tt? (P ) : (Q) -→A P IFF ff? (P ) : (Q) -→A Q Fig. 2.
Reduction relation for aπ processes (contextual congruence rules omitted).

Definition 3 (aπ and aπ ). The set aπ of asynchronous session processes is defined as:

P, Q ::= k v .P | k(y).P | k l.P | k {l i : P i } i∈I | v? (P ) : (Q) | P | Q | 0 | (νx)P | µX.P | X | k[i : m; o : m]
We write aπ to denote the sub-language of aπ without queues.

Differences with respect to Def. 1 appear in the second line of the above grammar.

The usual (single) restriction (νx)P is convenient in a queue-based setting; it binds both x and x in P . We consider recursion µX.P rather than input-guarded replication.

Communication in aπ is mediated by queues of messages m (values v or labels l), one for each endpoint k; these queues, denoted k[i : m; o : m], have output and input parts. Synchronization proceeds as follows: the sending endpoint first enqueues the message m in its own output queue; then, m is moved to the input queue of the receiving endpoint; finally, the receiving endpoint retrieves m from its input queue. We will use to denote the empty queue. Notions of free/bound (recursive) variables are as expected.

The operational semantics of aπ is defined as a reduction relation coupled with a structural congruence relation ≡ A . The former is defined by the rules in Fig. 2, which either follow the above intuitions for queue-based message passing or are exactly as for π; the latter is defined as the smallest congruence on processes that considers standard principles for parallel composition and inaction, together with the axioms:

(νx)(νy)P ≡ A (νy)(νx)P (νx)0 ≡ A 0 µX.P

≡ A P { µX.P /X} k[i : ; o : ] ≡ A 0 (νx)P | Q ≡ A (νx)(P | Q) if x ∈ fv(Q).
The notion of contexts for aπ includes unary contexts E and binary contexts C: Definition 4 (Contexts for aπ). The syntax of contexts in aπ is given by the following grammar:

E ::= [•] | E | P | P | E | (νx)E, where P is an aπ process and '[•]' rep- resents a 'hole'. We write C[• 1 , • 2 ] to denote binary contexts (ν x)([• 1 ] | [• 2 ] | n i=1 P i )
with n ≥ 1. We will write E[P ] (resp. C[P, Q]) to denote the aπ process obtained by filling the hole in

E[•] (resp. C[• 1 , • 2 ]
) with P (resp. P and Q).

Both π and aπ abstract from an explicit phase of session initiation in which endpoints are bound together. We thus find it useful to identify aπ processes which are properly initialized (PI): intuitively, processes that contain all queues required to reduce.

Definition 5 (Properly Initialized Processes). Let P ≡ A (ν x)(P 1 | P 2 ) be an aπ process such that P 1 is in aπ (i.e., it does not include queues) and fv(P 1 ) = {k 1 , . . . , k n }. We say P is properly initialized (PI) if P 2 contains a queue for each session declared in P 1 , i.e., if

P 2 = k 1 [i : , o : ] | • • • | k n [i : , o : ].
ReactiveML: A synchronous reactive programming language Based on the reactive model given in [START_REF] Boussinot | The SL synchronous language[END_REF], ReactiveML [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF] is an extension of OCaml that allows unbounded time response from processes, avoiding causality issues present in other SRP approaches. ReactiveML extends OCaml with processes: state machines whose behavior can be executed through several instants. Processes are the reactive counterpart of OCaml functions, which ReactiveML executes instantaneously. In ReactiveML, synchronization is based on signals: events that occur in one instant. Signals can trigger reactions in processes; these reactions can be run instantaneously or in the next instant. Signals carry values and can be emitted from different processes in the same instant.

We present the syntax of ReactiveML following [START_REF] Mandel | Reactivity of Cooperative Systems -Application to ReactiveML[END_REF], together with two semantics, with synchronous and asynchronous communication. We will assume countable infinite sets of variables V r and names N r (ranged over by x 1 , x 2 and n 1 , n 2 , respectively). x in one instant. When d and g are unimportant (e.g., when the signal will only be emitted once), we will write simply signal x in P . We will also write signal x 1 , . . . , x n in e when declaring n > 1 distinct signals in e. If expression e 1 transitions to the name of a signal then emit e 1 e 2 emits a signal carrying the value from the instantaneous execution of e 2 . Expression pause postpones execution to the next instant. The conditional expression present e 1 ? (e 2 ) : (e 3 ) checks the presence of a signal: if e 1 transitions to the name of a signal present in the current instant, then e 2 is run in the same instant; otherwise, e 3 is run in the next instant. Expression do e when e 1 executes e only when e 1 transitions to the name of a signal present in the current instant, and suspends its execution otherwise. Expression do (e 1 ) until e(x) → (e 2 ) executes e 1 until e transitions into the name of a signal currently present that carries a value which will substitute x. If this occurs, the execution of e 1 stops at the end of the instant and e 2 is executed in the next one. Using these basic constructs, we may obtain the useful derived expressions reported in Fig. 3, which include the parallel composition e 1 e 2 . We will say that an expression with no parallel composition operator at top level is a thread. We write ≡ R to denote the smallest equivalence that satisfies the following axioms: (i) e () ≡ R e; (ii) e 1 e 2 ≡ R e 2 e 1 ; (iii) (e 1 e 2 ) e 3 ≡ R e 1 (e 2 e 3 ). A Synchronous Semantics for RML Following [START_REF] Mandel | Reactivity of Cooperative Systems -Application to ReactiveML[END_REF], we define a big-step operational semantics for RML. We require some auxiliary definitions for signal environments and events. Below, and denote usual multiset union and inclusion, respectively. Definition 7 (Signal Environment). Let D, G, M be sets of default values, gathering functions, and multisets, respectively. A signal environment is a function

S : N r → (D × G × M), denoted S = [(d 1 , g 1 , m 1 )/n 1 , . . . , (d k , g k , m k )/n k ], with k ≥ 1.
We use the following notations: S d (n i ) = d i , S g (n i ) = g i , and S m (n i ) = m i . Also, S v = fold g i m i d i where fold recursively gathers multiple emissions of different values in the same signal; see [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF][START_REF] Mandel | Reactivity of Cooperative Systems -Application to ReactiveML[END_REF] for details. An event E associates a signal n i to a multiset m i that represents the values emitted during an instant:

Definition 8 (Events). An event is defined as a function

E : N r → M, i.e., E = [m 1 /n 1 , . . . , m k /n k ], with k ≥ 1.
Given events E 1 and E 2 , we say that

E 1 is included in E 2 (written E 1 E E 2 ) if and only if ∀n ∈ Dom(E 1 ) ∪ Dom(E 2 ) ⇒ E 1 (n) E 2 (n). The union E 1 and E 2 (written E 1 E E 2 ) is defined for all n ∈ Dom(E 1 ) ∪ Dom(E 2 ) as (E 1 E E 2 )(n) = E 1 (n) E 2 (n).
We now define the semantics of RML expressions. A big-step transition in RML captures reactions within a single instant, and is of the form e Fig. 4 gives selected transition rules; see [START_REF] Cano | Session-based Concurrency, Reactively (Extended Version)[END_REF] for a full account. Rules L-PAR and L-DONE handle let expressions, distinguishing when (a) at least one of the parallel branches has not yet terminated, and (b) both branches have terminated and their resulting values can be used. Rule RUN ensures that declared processes can only be executed while they are preceded by run . Rules LP-STU and LP-UN handle loop expressions: the former decrees that a loop will stop executing when the termination boolean of its body becomes ff; the latter executes a loop until Rule LP-STU is applied. Rule SIG-DEC declares a signal by instantiating it with a fresh name in the continuation; its default value and gathering function must be instantaneous expressions. Rule EMIT governs signal emission. Rule PAUSE suspends the process for an instant. Rules SIG-P and SIG-NP check for presence of a signal n: when n is currently present, the body e 2 is run in the same instant; otherwise, e 3 is executed in the next instant. Rules DU-END , DU-P , and DU-NP handle expressions do (e 1 ) until e 2 (x) → (e 3 ). Rule DU-END says that if e 1 terminates instanta- -------------→ S () neously, then the whole expression terminates. Rule DU-P says that if e 2 transitions to a currently present signal n, then e 3 is executed in the next instant, substituting x with the values gathered in n. Rule DU-NP executes e 1 as long as e 2 does not reduce to a currently present signal. We shall rely on a simple notion of equality:

L-PAR e1 E 1 ,b 1 ----→ S e 1 e2 E 2 ,b 2 ----→ S e 2 b1 ∧ b2 = ff let x1 = e1 and x2 = e2 in e3 E 1 E E 2 ,ff -------→ S let x1 = e 1 and x2 = e 2 in e3 L-DONE e1 E 1 ,tt ---→ S v1 e2 E 2 ,tt ---→ S v2 e3{ v1, v2 /x1, x2} E 3 ,b ---→ S e 3 let x1 = e1 and x2 = e2 in e3 E 1 E E 2 E E 3 ,b ----------→ S e 3 RUN e E 1 ,tt ---→ S process e e
---→ S v loop e E 2 ,b ---→ S e loop e E 1 E E 2 ,b ------→ S e SIG-DEC e1 E 1 ,tt ---→ S v1 e2 E 2 ,tt ---→ S v2 e3{ n /x} E 3 ,b ---→ S e 3 n fresh S(n) = (v1, v2, m) signal e 2 x : e1 in e3 E 1 E E 2 E E 3 ,b ----------→ S e 3 EMIT e1 E 1 ,tt ---→ S n e2 E 2 ,tt ---→ S v emit e1 e2 E 1 E E 2 E [{v}/n],tt
PAUSE pause ∅,ff --→ S ( )
SIG-P e1 E 1 ,tt ---→ S n n ∈ S e2 E 2 ,b ---→ S e 2 present e1? (e2) : (e3) E,ff ---→ S e 2 SIG-NP e1 E,tt ---→ S n n ∈ S present e1? (e2) : (e3) E,ff ---→ S e3 DU-END e2 E 2 ,tt ---→ S n e1 E 1 ,tt ---→ S v do (e1) until e2(x) → (e3) E 1 E E 2 ,tt -------→ S v DU-P e2 E 2 ,tt ---→ S n n ∈ S e1 E 1 ,ff ---→ S e 1 do (e1) until e2(x) → (e3) E 1 E E 2 ,ff -------→ S e3{ S v (n) /x} DU-NP e2 E 2 ,tt ---→ S n n ∈ S e1 E 1 ,ff ---→ S e 1 do (e1) until e2(x) → (e3) E 1 E E 2 ,ff -------→ S do (e 1 ) until e2(x) → (e3)
Definition 9 (Equality with case normalization). Let → R denote the extension of ≡ R with the axiom match c j with {c i → P i } i∈I → R P j , where c j is a constant and j ∈ I.

RMLq: ReactiveML with a Queue-based Semantics We extend RML with an explicit store of queues that keeps the state of the executed program. Unlike signals, the store of queues is preserved throughout time. The syntax of RML is extended with constructs that modify the queues located in the store; the resulting language is called RMLq:

Definition 10 (RMLq). RMLq expressions are obtained by extending the grammar of values in Def. 6 with the following forms:

v ::= • • • | pop | put | isEmpty. PUT-Q put q v ; Σ, q : h ∅,tt S () ; Σ, q : h • v POP-Q pop q ; Σ, q : v • h ∅,tt S v ; Σ, q : h NEMPTY isEmpty q ; Σ, q : h ∅,tt S () ; Σ, q : h POP-Q pop q ; Σ, q :
∅,ff S pop q ; Σ, q :

EMPTY isEmpty q ; Σ, q :

∅,ff S isEmpty q ; Σ, q : Fig. 5. Big-step semantics for RMLq: Queue-related operations.

The new constructs allow RMLq programs to modify queues, which are ranged over by q, q , . . .. Construct put receives a queue and an element as parameters and pushes the element into the end of the queue. Construct pop takes a queue and dequeues its first element; if the queue is empty in the current instant the process will block the current thread until an element is obtained. Construct isEmpty blocks a thread until the instant in which a queue stops being empty.

The semantics of RMLq includes a state Σ, Σ ::= ∅ | Σ, q : v (i.e., a possibly empty collection of queues) and configurations K, K ::= e ; Σ . The big-step semantics then has transitions of the form e ; Σ E,b S e ; Σ , where S is a signal environment, b is a termination boolean, and E is an event. The corresponding transition system is generated by rules including those in Fig. 5 (see also [START_REF] Cano | Session-based Concurrency, Reactively (Extended Version)[END_REF]). Most transition rules for RMLq are interpreted as for RML; we briefly discuss queue-related rules in Fig. 5. Rule PUT-Q pushes an element into a queue and terminates instantaneously. Rule POP-Q takes the first element from the queue (if not empty) and terminates instantaneously. Rule NEMPTY enables isEmpty to terminate instantaneously if the queue is not empty. Rule POP-Q keeps the thread execution stuck for at least one instant if the queue is empty; Rule EMPTY is similar. We rule out programs with parallel pop/put operations along the same session in the same instant.

Expressiveness Results

We present our main results: correct translations of π into RML and of aπ into RMLq.

The Formal Notion of Encoding We define notions of language, translation, and encoding by adapting those from Gorla's framework for relative expressiveness [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF].

Definition 11 (Languages & Translations).

A language L is a tuple P, -→, ≈ , where P is a set of processes, -→ denotes an operational semantics, and ≈ is a behavioral equality on P. A translation from L s = P s , -→ s , ≈ s into L t = P t , -→ t , ≈ t (each with countably infinite sets of variables V s and V t , respectively) is a pair • , ψ • , where • : P s → P t is a mapping, and ψ • : V s → V t is a renaming policy for • .

We are interested in encodings: translations that satisfy certain correctness criteria: Definition 12 (Encoding). Let L s = P s , -→ s , ≈ s and L t = P t , -→ t , ≈ t be languages; also let • , ψ • be a translation between them (cf. Def. 11). We say that such a translation is an encoding if it satisfies the following criteria:

1. Name invariance: For all S ∈ P s and substitution σ, there exists σ such that Sσ = S σ , with ψ • (σ(x)) = σ (ψ • (x)), for any x ∈ V s . 2. Compositionality: Let res s (•, •) and par s (•, •) (resp. res t (•, •) and par t (•, •)) denote restriction and parallel composition operators in P s (resp. P t ). Then, we define: res s ( x, P ) = res t (ψ • ( x), P ) and par s (P, Q) = par t ( P , Q ). 3. Operational correspondence, i.e., it is sound and complete: (1) Soundness: For all S ∈ P s , if S -→ s S , there exists T ∈ P t such that S =⇒ t T and T ≈ t S .

(2) Completeness: For all S ∈ P s and T ∈ P t , if S =⇒ t T , there exists S such that S =⇒ s S and T ≈ t S .

While name invariance and compositionality are static correctness criteria, operational correspondence is a dynamic correctness criterion. Notice that our notion of compositionality is less general than that in [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]: this is due to the several important differences in the structure of the languages under comparison (π vs. RML and aπ vs. RMLq).

We shall present translations of π into RML and of aπ into RMLq, which we will show to be encodings. We instantiate Def. 11 with the following languages: Definition 13 (Concrete Languages). We shall consider:

-L π will denote the tuple π, -→, ≡ S , where π is as in Def. 1; -→ is the reduction semantics in Fig. 1; and ≡ S is the structural congruence relation for π.

-L RML will denote the tuple RML,

E,b --→ S , → R , where RML is as in Def. 6; E,b --→ S is
the big-step semantics for RML; and → R is the equivalence in Def. 9. -L aπ will denote the tuple aπ, -→ A , ≡ A , where aπ is as in Def. 3; -→ A is the reduction semantics in Fig. 2; and ≡ A is the structural congruence relation for aπ.

-L RMLq will denote the tuple RMLq, is the big-step semantics for RMLq; and ≡ R is the equivalence for RML.

When events, termination booleans, and signal environments are unimportant, we write

P -→ Q instead of P E,b --→ S Q, and K K instead of K E,b S K .
Encoding L π into L RML Key aspects in our translation of L π into L RML are: (i) the use of value carrying signals to model communication channels; and (ii) the use of a continuation-passing style (following [START_REF] Dardha | Session types revisited[END_REF]) to model variables in π using RML signals.

Definition 14 (Translating L π into L RML ). Let • f , ψ • f be a translation where:

(1) ψ • f (x) = x, i.e., every variable in π is mapped to the same variable in RML.

(2) • f : L π → L RML is as in Fig. 6, where f is a substitution function.

Function f in • f ensures that fresh signal identifiers are used in each protocol action. The translation of x v .P declares a new signal x which will be sent paired with value v through signal x; process P f,{x←x } is executed in the next instant. Dually, the translation of x(y).P awaits a signal carrying a pair, composed of a value and the signal name that to be used in the continuation, which is executed in the next instant.

Translations for selection and branching are special cases of those for output and input. Restriction (νxy)P is translated by declaring a fresh signal w, which replaces

x v .P f = signal x in (emit fx (v, x ); pause ; P f,{x←x } ) x(y).P f = await fx(y, w) in P f,{x←w} x l.P f = signal x in (emit fx (l, x ); pause ; P f,{x←x } ) x lj{li : Pi}i∈I f = await fx(l, w) in match l with {li → Pi f,{x←w} } v? (P ) :

(Q) f = if v
) P | Q f = P f Q f 0 f = ()
Fig. 6. Translation from Lπ to L RML (Def. 14). Notice that fx is a shorthand for f (x).

x, y in P f . Conditionals, parallel composition and inaction are translated homomorphically. Input-guarded replication is a special case of recursion, enabling at most one copy of the spawned process in the same instant; such a copy will be blocked until the process that spawned it interacts with some process. In Fig. 6, α, β denote variables inside the declaration of a recursive process, distinct from any other variables. We state our first technical result: the translation of L π into L RML is an encoding. In the proof, we identify a class of well-formed π processes that have at most one output and selection per endpoint in the same instant; see [START_REF] Cano | Session-based Concurrency, Reactively (Extended Version)[END_REF] for details.

Theorem 1. Translation • f , ψ • f is an encoding, in the sense of Def. 12.

Encoding L aπ into L RMLq The main intuition in translating aπ into RMLq is to use the queues of RMLq coupled with a handler process that implements the output-input transmission between queues. We start by introducing some auxiliary notions.

Notation 1 Let

P ≡ A (ν x)( i∈{1,...,n} Q i | kj ∈ k k j [i : , o : ] be PI (cf. Def. 5)
with variables k. We will write P as

C l [Q l , K( k)], where l ∈ {1, . . . , n}, C l [• 1 , • 2 ] = j∈{1,...,n}\{l} Q j | [• 1 ] | [• 2 ], and K( k) = kj ∈ k k j [i : , o : ].
This notation allows us to distinguish two parts in a PI process: the non-queue processes and the queue processes K( k). We now define the key notion of handler process: Definition 15 (Handler process). Given k = {k 1 , . . . , k n }, the handler process H( k) is defined as i∈{1,...,n} I(k i ) O(k i ), where I(k) and O(k) are as in Fig. 7.

Given an endpoint k, a handler defines parallel processes I k and O k to handle input and output queues. Transmission is a handshake where both O k and I k (or viceversa) must be ready to communicate. If ready, O k sends a pair containing the message (pop k o ) and a fresh signal for further actions (α ). Once the pair is received, it is enqueued in k i (i.e., the dual I k ). The process is recursively called in the next instant with the new endpoints. The translation of aπ into RMLq requires a final auxiliary definition: queues. Because of this two-part structure, static correctness properties are established for {[•]} (for this is the actual translation of source processes), whereas operational correspondence is established for ([•]) (which generates an RMLq configuration). 1. Soundness:

If C[Q, K( k)] -→ A C[Q , K ( k)] then ([C[Q, K( k)]]) ([C [Q , K ( k)]]), for some Q , K ( x), C where C[Q, K( x)] -→ A C[Q , K ( x)] -→ * A (ν x)C [Q , K ( x)]. 2. Completeness: If ([C[Q, K( x)]]) R then there exist Q ,C ,K ( x) such that C[Q, K( x)] -→ * A (ν x)C [Q , K ( x)] and R = ([C [Q , K ( x)
]]). In soundness, a single RMLq step mimicks one or more steps in aπ, i.e., several source computations can be grouped into the same instant. This way, e.g., the interaction of several outputs along the same session with their queue (cf. Rule SEND ) will take place in the same instant. In contrast, several queue synchronizations in the same session (cf. Rule COM ) will be sliced over different instants. Conversely, completeness ensures that our encoding does not introduce extraneous behaviors: for every RMLq transition of a translated process there exists one or more corresponding aπ reductions.

Closing Remarks

We have shown that ReactiveML can correctly encode session-based concurrency, covering both synchronous and asynchronous (queue-based) communications. 4 Our encodings are executable: as such, they enable to integrate session-based concurrency in actual RML programs featuring declarative, reactive, timed, and contextual behavior. This is an improvement with respect to previous works, which extend the π-calculus with some (but not all) of these features and/or lack programming support. Interestingly, since ReactiveML has a well-defined semantics, it already offers a firm basis for both foundational and practical studies on session-based concurrency. Indeed, ongoing work concerns the principled extension of our approach to the case of multiparty sessions.

We have not considered types in source/target languages, but we do not foresee major obstacles. In fact, we have already shown that our encoding • f supports a large class of well-typed π processes in the system of [START_REF] Vasconcelos | Fundamentals of session types[END_REF], covering a typed form of operational correspondence but also type soundness: if P is a well-typed π process, then P f is a well-typed RML expression-see [START_REF] Cano | Session-based Concurrency, Reactively (Extended Version)[END_REF]. We conjecture a similar result for ([•]), under an extension of [START_REF] Vasconcelos | Fundamentals of session types[END_REF] with queues. On the ReactiveML side, we can exploit the typeand-effect system in [START_REF] Mandel | Reactivity of Cooperative Systems -Application to ReactiveML[END_REF] to enforce cooperative programs (roughly, programs without infinite loops). Since • f and ([•]) already produce well-typed, executable ReactiveML expressions, we further conjecture that they are also cooperative, in the sense of [START_REF] Mandel | Reactivity of Cooperative Systems -Application to ReactiveML[END_REF].

Definition 6 (

 6 RML). The set RML of ReactiveML expressions is defined as: v, v ::= c | (v, v) | n | λx.e | process e e, e ::= x | c | (e, e) | λx.e | e e | rec x = v | match e with {c i → e i } i∈I | let x = e and x = e in e | run e | loop e | signal e x : e in e | emit e e | pause | process e | present e? (e) : e | do e when e | do (e) until e(x) → (e) Values v, v , . . . include constants c (booleans and the unit value ()), pairs, names, abstractions, and also processes, which are made of expressions. The syntax of expressions e, e extends a standard functional substrate with match and let expressions and with process-and signal-related constructs. Expressions run e and loop e follow the expected intuitions. Expression signal g x : d in e declares a signal x with default value d, bound in e; here g denotes a gathering function that collects the values produced by

Fig. 3 .

 3 Fig. 3. Derived RML expressions.

Fig. 4 .

 4 Fig. 4. Big-step semantics for RML expressions (selection).

,

  ≡ R , where RMLq is as in Def. 10;

Theorem 2 (

 2 Name invariance and compositionality for {[•]}). Let P , σ, x, and E[•] be an aπ process, a substitution, a variable in aπ , and an evaluation context (cf. Def. 4), respectively. Then: (1) {[P σ]} = {[P ]}σ, and (2) {[E[P ]]} = {[E]} {[P ]} . Theorem 3 (Operational correspondence for ([•])). Given a properly initialized aπ process C[Q, K( k)], it holds that:

  Time is modelled as discrete units, called instants; reactivity arises through signals, which may carry values. In ReactiveML, expression signal x in e declares a new signal x. We use constructs emit s v and await s(x) in e to emit and await a signal s, respectively. Preemption based on signals is obtained by the expression do (e 1 ) until s → (e 2 ), which executes e 1 until signal s is detected, and runs e 2 in the next instant. Moreover, Reac-tiveML can encode the parallel composition of expressions e 1 and e 2 , denoted e 1 e 2 .

	Embedding Sessions in ReactiveML Our first encoding, denoted • f (cf. Def. 14),
	translates session π-calculus processes into ReactiveML expressions; we use substitu-
	tion f to represent names in the session π-calculus using (fresh) signals in ReactiveML.
	Our second encoding, denoted ([•]) (cf. Def. 17), supports an asynchronous semantics.

  then (pause ; P ) else (pause ; Q) (νxy)P f = signal w in P f,{x←w,y←w} * x(y).P f = let rec process repl α β = signal x in do (loop present fα? (emit x ; pause ) : (())) until fα(y, w) → (run β {α←w} ) await x in run (repl α β) in run repl x (process P f

Synchronous communication as in the (session) π-calculus should not be confused with the synchronous programming model of ReactiveML.

Acknowledgements We thank Ilaria Castellani, Cinzia Di Giusto, and the anonymous reviewers for useful remarks and suggestions. This work has been partially sponsored by CNRS PICS project 07313 (SuCCeSS) and EU COST Actions IC1201 (BETTY), IC1402 (ARVI), and IC1405 (Reversible Computation).

Fig. 8. Auxiliary translation from aπ into RMLq (Def. 17).

Definition 16. We define δ(•) as a function that maps aπ processes into RMLq states:

and as δ(P ) = ∅ for every other aπ process.

Definition 17 (Translating

) be a translation where:

-

, every variable in aπ is mapped to the same variable in RMLq.

-

which are translated into RMLq configurations as follows:

where {[•]} : L aπ → L RMLq is in Fig. 8; H( k) is in Def. 15; and δ(•) is in Def. [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF].

Two key ideas in translation ([•]) are: queues local to processes and compositional (queue) handlers. Indeed, communication between an endpoint k and its queues k i , k o proceeds instantaneously, for such queues should be local to the process implementing session k. Queue handlers effectively separate processes/behavior from data/state. As such, it is conceivable to have handlers that have more functionalities than those of H( k). In [START_REF] Cano | Session-based Concurrency, Reactively (Extended Version)[END_REF] we provide an example of a handler more sophisticated than H( k).

Translation ([•]

) is in two parts. First, {[•]} translates non-queue processes: output and input are translated into queuing and dequeuing operations, respectively. Selection and branching are modeled similarly. Translations for the conditional, inaction, parallel, and recursion is as expected. Recursion is limited to a pause-guarded tail recursion in {[•]} to avoid loops of instantaneous expressions and nondeterminism when accessing queues. Second, ([•]) creates an RML configuration by composing the RMLq process obtained via {[•]} with appropriate handlers and with the state obtained from the information in aπ


Hadi Aliakbarpour

Kamrad Khoshhal
email: kamrad@isr.uc.pt

João Quintas
email: jquintas@isr.uc.pt

Kamel Mekhnacha
email: kamel.mekhnacha@probayes.com

Julien Ros
email: julien.ros@probayes.com

Maria Andersson
email: maria.andersson@foi.se

Jorge Dias

HMM-based Abnormal Behaviour Detection Using Heterogeneous Sensor Network

Keywords: Heterogeneous sensor network, LLF (Low level Feature), HBA (Human Behaviour Analysis), HMM (Hidden Markov Model), LMA (Laban Movement Analysis), Crowd analysis, ATM (Automated Teller Machine) security

This paper proposes a HMM-based approach for detecting abnormal situations in some simulated ATM (Automated Teller Machine) scenarios, by using a network of heterogeneous sensors. The applied sensor network comprises of cameras and microphone arrays. The idea is to use such a sensor network in order to detect the normality or abnormality of the scenes in terms of whether a robbery is happening or not. The normal or abnormal event detection is performed in two stages. Firstly, a set of low-level-features (LLFs) is obtained by applying three different classifiers (what are called here as low-level classifiers) in parallel on the input data. The low-level classifiers are namely Laban Movement Analysis (LMA), crowd and audio analysis. Then the obtained LLFs are fed to a concurrent Hidden Markov Model in order to classify the state of the system (what is called here as high-level classification). The attained experimental results validate the applicability and effectiveness of the using heterogeneous sensor network to detect abnormal events in the security applications.

Introduction

Recently, the demand for using automatic surveillance systems has been increasing. Many research areas, such as computer vision, signal processing, voice analysis and sensor fusion and pattern recognition are involved in this type of applications. Work on detection and tracking algorithms for dense crowds can be found in the literature. In [START_REF] Eshel | Homography Based Multiple Camera Detection and Tracking of People in a Dense Crowd[END_REF] a method is suggested for simultaneously tracking all people in a dense crowd using a set of cameras with overlapping fields of view. In [START_REF] Bird | Real time, online detection of abandoned objects in public areas[END_REF] a real-time system for detection of moving crowds is presented. HMM has been used in various applications for behavior recognition, e.g. [START_REF] Shang | Nonparametric discriminant HMM and application to facial expression recognition[END_REF] for facial action recognition and [START_REF] Drews | Crowd behavior under cameras network fusion using probabilistic methods[END_REF] for crowd behavior analysis. Crowd analysis can be used to get an understanding of the crowd as a whole, without any detailed information on individuals in the crowd. Crowd activity provides information which can be used to detect if there are people running or fighting [START_REF] Drews | Crowd behavior under cameras network fusion using probabilistic methods[END_REF]. A deep contribution in the field of human-machine interaction (HMI), based on the concept of LMA (Laban Movement Analysis), is presented by Rett and Dias in [START_REF] Rett | Laban Movement Analysis using a Bayesian model and perspective projections[END_REF]. In their work a Bayesian model is used for learning and classification. The LMA is presented as a concept to identify useful features of human movements to classify human gestures. Frequency-based extracted features are used in a LMA-based approach in our previous work for the sake of behaviour analysis [START_REF] Khoshhal | Probabilistic LMA-based classification of human behaviour understanding using power spectrum technique[END_REF]. Using audio signals for security purposes is proposed in [START_REF] Ntalampiras | An Adaptive Framework for Acoustic Monitoring of Potential Hazards[END_REF]. Using distributed sensor network for the surveillance is investigated and proposed by Aliakbarpour et al. in [START_REF] Hadi Aliakbarpour | A Novel Framework for Data Registration and Data Fusion in Presence of Multi-modal Sensors[END_REF][START_REF] Aliakbarpour | Human Silhouette Volume Reconstruction Using a Gravity-based Virtual Camera Network[END_REF].

A two-staged classification approach, to detect abnormal events in a security scenario, is introduced in this paper. Firstly, a set of low-level-features (LLFs) is obtained by concurrently applying three different classifiers (what are called here as low-level classifiers) on the input data. The low-level classifiers are namely LMA, crowd and audio analysis. Then the obtained LLFs are fed to a concurrent HMM in order to classify the state of the system (what is called here as high-level classification). A network of heterogeneous sensors such cameras and microphone arrays are used in a synergic way to observe the scene.

This paper is arranged as following: Our contribution to sustainability is presented in Sec. 2. Low-level classification is introduced in Sec. 3. A HMM-based classification (here is known as the high level classifier) is discussed in Sec. 4. Sec. 5 is dedicated to the experimental results and eventually the conclusion is presented in Sec. 6.

Contribution to sustainability

In order to protect citizens, property and infrastructure, surveillance systems are increasingly being used. Commonly, these surveillance systems are installed in public spaces, covering large areas, where a great number of people populate the camera's fields of view. Consequently such systems consist often of a large amount of distributed sensors, typically CCTV cameras, monitored by operators in a control room. Since humans possess a limited capacity of driving its focus of attention, it is impossible to the system's operators pay attention to all what is happening in all monitors at a given time. Moreover, to recognizing abnormal or threatening events is a complex cognitive task requiring a focus that humans can uphold for only a short time. Therefore, there is the need for a persistent system capable of making a proactive surveillance. In this paper we introduce a method to detect abnormal situation, in the ATM scenarios, using the observations of a heterogeneous sensor network comprising of cameras and microphone arrays.

Low-level classification

As mentioned, the idea is to apply a two staged procedure in order to conclude whether the scene's state is normal or abnormal. Here the used data is from an exclusive multimodal database, referred as PROMETHEUS database 1 [8]. This database is in support of the development and the evaluation of the algorithms which 1 www.prometheus-FP7.eu. are intended to analyze and identify human actions and behaviors in the context of surveillance using multi-modal approaches. It comprises of various securities scenarios and among them we focused on the ATM ones. Many typical events such as walking, waiting, taking money and some atypical events such as robbery have happened in the ATM scenarios. The intention is to automatically identify and detect the state of the scene in terms of whether a normal or abnormal event is happening.

The scenes are observed by a network of heterogeneous sensors, composed of video cameras, thermal cameras and microphone arrays. Among the heterogeneous data in the database, we selected two modalities: image and sound. Three different low-level classification methods, namely LMA, crowd and audio analysis, have been applied on these data in order to obtain a set of LLFs. Table 1 summarizes the inputs and outputs for each method. As can be seen, two of these methods, the LMA and crowd analysis, have their inputs from applying some preliminary data fusion and tracking algorithms (which are supposed to be available) on the raw data and just the audio analysis one has a direct input from the raw sound signals. For the sake of having a low level classification on the sound signals, the method introduced in [START_REF] Ntalampiras | An Adaptive Framework for Acoustic Monitoring of Potential Hazards[END_REF] has been used. Here we continue to introduce the LMA and crowd analysis methods.

LMA-based human movement classification

LMA is a well-known method to describe and analyze human movements by several components; Body, Space, Shape, Effort and Relationship [START_REF] Zhao | Acquiring and validating motion qualities from live limb gestures[END_REF]. Each component describes human movements by different aspects. Among the different components of LMA, here we have selected Effort component to observe human movements in terms of how motion of human body parts are happening with respect to inner intention (our recent work in [START_REF] Khoshhal | Probabilistic LMA-based classification of human behaviour understanding using power spectrum technique[END_REF]). Effort has four sub-components and each of them has two states; Effort.time (sudden/sustained), Effort.space (direct/indirect), Effort.weight (light/strong) and Effort.flow (bounded/free). In this work, the Effort.time component for two body parts (head and feet) is estimated. Here the interesting movements to classify are standing, walking, running and falling-down. A Bayesian Network (BN), which is a well-known "tool" to deal with uncertainty, has been used for our LMA parameters estimations (to classify different human movements). The BN has three levels; • The lowest level comprises frequency-based features which were achieved from Power Spectrum (PS) technique that applied on acceleration signals of body parts. First four coefficients were collected from PS signal of each body part acceleration signals. Each coefficient has four state possibilities (see [START_REF] Khoshhal | Probabilistic LMA-based classification of human behaviour understanding using power spectrum technique[END_REF]) which are defined by several thresholds. • Middle-level includes LMA parameters, Effort.time component of the body parts.

Crowd analysis

Crowd analysis is used to get an understanding of the crowd as a whole, without any detailed information on individuals in the crowd (see our recent work [START_REF] Drews | Crowd behavior under cameras network fusion using probabilistic methods[END_REF]). The aim is to get an approximate understanding of the activity level of the crowd as well as the size of the crowd. Crowd activity provides information which can be used to detect if there are people running or fighting. In general, normal crowd behavior often corresponds to calm movements, where people are standing or moving slowly through the scene, without making excessive gestures. Abnormal behaviour is instead likely to be accompanied by more rapid movements. The different levels of crowd activity are estimated by optical flow calculations, which estimate the relative motion between consecutive images. If a person is walking quickly, running, or moving his or her arms rapidly, the magnitude of optical flow will be larger compared to the case when a person is moving slowly or standing still. The different levels of crowd activity can be derived by using for example the following approaches:

1. Manually setting the different levels by observing the optical flow under known conditions, i.e. when the different types of events in the scene are known. 2. Applying a more automatic approach for obtaining the levels by using basic statistics (mean value and standard deviation) on relevant training data. The crowd size provides information that can be used for getting warnings of forthcoming fights, attempted robbery and risk for riots. What is considered to be a large or small crowd will differ from case to case. For example, in a city area a large crowd may be 20-25 persons or more. At large sport events, large crowds are probably hundreds or thousands of persons. Fighting and robbery at the ATM means that at least two persons are present on a small area at the same time. The crowd size estimate is obtained by first performing background subtraction to obtain the foreground pixels. We assume prior knowledge of the approximate number of pixels per person, which depends on the distance between camera and crowd. The number of people is then obtained by dividing the total amount of foreground pixels by the number of assumed pixels per person. Also crowd growth rate and crowd density can be of interest to understand the crowd behaviour. Is the crowd growing quickly and/or are the people standing close to each other? Crowd growth rate can be estimated by studying the change in crowd size for a certain reasonable time period. Crowd density can be estimated by relating the crowd size to a specific area in the image. By combining estimates of crowd activity and crowd size, uncertainty in the classification of behavior will be reduced. For example, increased activity (a running person) at an ATM together with the information that there were at least two persons present close to the ATM, will strengthen the view that there have been an attempted robbery.

Concurrent HMM-based classification

For behaviour recognition, we are interested in detecting the current behavior amongst known behaviors (i.e. the behaviour library). For this purpose, we propose to use a concurrent HMM architecture.

Principle. A concurrent hidden Markov model is composed of several hidden

Markov Models, each one describing one class (see Fig. 3-left). To summarize, the concurrent HMM centralizes the on-line update of the behaviour belief and contains:

1. The set of HMMs representing basic behaviour library (one HMM per behaviour); 2. The transition between behaviors model that could be either defined by hand (by an expert), or learnt from annotated data. Hidden Markov Models are used to characterize an underlying Markov chain which generates a sequence of states. The term Hidden in the HMM name comes from the fact that the sequence of states is not directly observable. Instead the states generate an observable sequence. Thus, the output depends on the current state and on previous outputs. These tools are widely used in the field of sound processing [START_REF] Rabiner | A tutorial on Hidden Markov Models and selected applications in speech recognition[END_REF], gene finding and alignment in DNA sequences [START_REF] Pachter | Applications of generalized pair Hidden Markov Models to alignment and gene finding problems[END_REF]. They were introduced by Andre Markov in [START_REF] Markov | An example of statistical investigation of the text eugene onegin concerning the connection of samples in chains[END_REF] and developed in [START_REF] Baum | A maximization technique occurring in the statistical analysis of probabilistic functions of Markov chains[END_REF] HMM are widely employed in the field of computer vision to recognize gesture or human behaviour [START_REF] Biem | A model selection criterion for classification: Application to HMM topology optimization[END_REF]. In these applications, the observation variables are features extracted for video data. The principle of an HMM is presented on Figure • Learning the set of HMM models representing the behaviour library (one HMM per behaviour) using an annotated data set. • Defining the transition matrix between the behaviors. This transition model could be either defined by hand (by an expert), or learnt from an annotated data set. Learning the behaviour transition model is straightforward and consists in computing simple statistics (histograms) of transitions using the annotated data set. Learning the underlying HMM models (a HMM per behaviour) is more complex. It can be divided into two sub-problems:

1.

Finding the optimal number of states N. The optimal number of internal states within the HMMs could be chosen by hand thanks to an expert. In this case no algorithm is needed and the learning of the HMM is reduced to the learning of its parameters. However, since an HMM is a Bayesian Network, a score that allows a compromise between fitting learning examples (D) and the ability of generalization (see the Occam Razor Principle) can be employed to find it automatically [START_REF] Biem | A model selection criterion for classification: Application to HMM topology optimization[END_REF]. For example the classical Bayesian Information Criterion [START_REF] Schwarz | Estimating the dimension of a model[END_REF] that maximizes the likelihood of the data while penalizing large size model can be used:

|) log(| ) ( 2 1 )) , ( log( ) , ( D n nparams n D likelihood D n BIC × × - =
In this case the optimal number of states is given by:

) , ( max arg D n BIC n n = * 2.
Learning the parameters of the HMM given N (i.e., the transition matrix

S P

). The idea is find the parameters that maximize the data likelihood. For this purpose the methods generally employed are the classical EM algorithm (aka Baum-Welch algorithm in the HMM context), or the Iterative Viterbi algorithm.

Recognition. As previously emphasized, the concurrent hidden Markov model is used to recognize on-line or off-line the current behaviors amongst N known behaviors. This is easily performed by finding the HMM M that maximizes

Experiments

As mentioned, the ATM scenarios of PROMETHUS [START_REF] Ntalampiras | Heterogeneous Sensor Database in Support of Human Behaviour Analysis in Unrestricted Environments: The Audio Part The 7th int[END_REF] multimodal database are used in this paper. There are four selected ATM scenes with different durations. The interesting event which we call as abnormal state in this kind of scenario is robbery. Based on the proposed approach the process of event detection has two levels for performing the classification. Firstly, some low-level features are obtained by using three different approaches (see Fig. 3). Then these low-level features are fed to a HMM as a high level classifier in order to estimate the scene's state. Apart of these LLF inputs for the HMM, another parameter which is named as "environment parameter" is also consider for the HMM. The environment parameter is defined as the relative positions of people to the ATM. In the context of the ATM scenario in PROMETHEUS dataset, we defined the robbery state as when the robber waits in ATM's area, approaches a person who is taking money from the machine, steals the money and then rapidly escapes. In the database, there are 139 samples Project PROMETHEUS, www.prometheus-FP7.eu. The authors would like to thank our partners from University of Patras for providing sound data.

Fig. 1 -

 1 Fig. 1-A superimposed view of the ATM scenario when a rubbery is happening.

Fig. 2 .

 2 Fig. 2. LMA-based Bayesian net

Fig. 3 :

 3 Fig. 3: Concurrent Hidden Markov Models (left) HMM model (right)

Fig. 3 -

 3 (right) in which S represents the state variable and O represents the observation ones. In our application, each HMM describes a human behaviour and is learned using a training dataset composed of labeled observation sequences that are low-feature extracted from the different and thanks to three different approaches, namely Laban Movement Analysis (LMA), crowd and audio analysis. Construction/Learning. Constructing a concurrent hidden Markov model consists in:

  the on-line case).

Table 1 :

 1 Inputs and outputs for the different methods in the low-level classification stage.

	Method	Input	Output
	Crowd Analysis	Optical flow from image data	Crowd ratio
	Laban Movement Analysis	3D positions of heads and feet algorithms) (available from tracking	Pr(walking), Pr(running), Pr(falling) and Pr(standing)
	Audio Analysis	Sound signals	LL-ratio

• The highest level is just one node which has the number of interest human movement's states.

Acknowledgment: Hadi Ali Akbarpour is supported by the FCT (Portuguese Fundation for Science and Technology). This work is supported by the European Union within the FP7

corresponding to the normal situations and 8 samples corresponding to the robbery (abnormal) situations. Each sample has a 10 seconds long. Among these samples, 61 samples of normal data and 4 samples of abnormal ones have been randomly selected for HMM learning process and the others (78 samples of normal and 4 samples of abnormal) for HMM classification process.

Here we have implemented different experiments on the data in order to demonstrate the applicability and effectiveness of using heterogeneous data fusion in the proposed manner. Table 2 depicts the result of the HMM-based classifier when the output of each low-level classifier is individually applied to the high-level (final) classifier. Then the experiment is performed when a pair of the low-level-classifier outputs is used for the classification (three possible pair combinations, see Table 3). Eventually all of the low-level classifier's outputs have been fed to the high-level classifier. Table 4 depicts the result of this last case, in which there are the best percentages of the true even detections. It validates the effectiveness of the proposed method for the sake of surveillance applications

Conclusion

Abnormal human behavior detection by using a network of heterogeneous sensors, in some ATM scenarios, has been proposed in this paper. A two-staged classification, divided as low-level-classification and high-level-classification, is used in order to detect the abnormality of the current state of the scene. Here, the interesting abnormal event is defined as happening a robbery near the ATM. The LMA, crowd analysis and audio analysis are the methods which are used in the lowclassification stage. For the sake of high-level classification, a concurrent HMM is applied. The attained experimental results validate both the applicability and efficiency of the proposed method for the sake of surveillance applications.


Filipe Moutinho

Luís Gomes

Paulo Barbosa

João Paulo Barros

Franklin Ramalho
email: franklin@dsc.ufcg.edu.br

Jorge Figueiredo

Anikó Costa

André Monteiro

Petri net based Specification and Verification of Globally-Asynchronous-Locally-Synchronous System

Keywords: GALS, Embedded Systems, Petri Nets, Maude, Verification

This paper shows a methodology for Globally-Asynchronous-Locally-Synchronous (GALS) systems specification and verification. The distributed system is specified by non-autonomous Petri net modules, obtained after the partition of a (global) Petri net model. These modules are represented using IOPT (Input-Output Place-Transition) Petri net models, communicating through dedicated communication channels forming the GALS system under analysis. This set of modules is then automatically translated into Maude code through a MDA approach. As the modules of GALS systems run concurrently, the Maude semantics for concurrent objects is used along with message representation. Finally, as a particular case, the system state space is generated from the Maude specification of the GALS system, allowing property verification.

Introduction

Embedded systems are increasingly present in people's lives, for instance in people's pockets, homes, cars and in industrial machinery. Many embedded systems are synchronous systems implemented in a single device, but there are embedded systems that can not be implemented using the synchronous paradigm, either due to the need of having multiple devices in different physical locations, or due to the simple fact that a single device is not enough to implement the system, or even when it is necessary to use devices containing multiple clock domains.

These systems are Globally-Asynchronous-Locally-Synchronous (GALS). They support features like asynchronous messaging and multiple concurrent synchronous modules with different clock domains. But these features make GALS systems development not a simple task, and with greater challenges (for example the verification of GALS systems components interaction) compared to the development of synchronous systems. This was the environment where was found the research question of this work, which is How to specify, simulate, verify and implement a GALS system described through a set of IOPT Petri net sub-models supported by automatic code generation?

The methodology proposed here to develop GALS systems for embedded systems applications was initially formulated within the FORDESIGN project [START_REF] Gomes | Formal Methods for Embedded Systems Co-design: the FORDESIGN Project[END_REF], which had the objective to center the development effort in the system modeling, relying in a model-base development attitude and taking advantage of automatic code generation tools. However, the FORDESIGN project did not fully consider the development of GALS systems. The chosen modeling formalism was the Input-Output Place-Transition (IOPT) Petri net, a class of non-autonomous Petri nets defined in [START_REF] Gomes | The Input-Output Place-Transition Petri Net Class and Associated Tools[END_REF] that extends the well-known Place-Transition (P/T) Petri net class with inputs and outputs signals and events (among other characteristics).

The Net Splitting Operation proposed in [START_REF] Costa | Petri net partitioning using net splitting operation[END_REF], allowing model partitioning into several components, is here used to split centralized models of GALS systems into GALS components. These components will be interconnected through lossless communication channels with undetermined propagation time for all the messages.

To allow property verification of the GALS systems, modeled by IOPT net models, are performed a set of transformations from the IOPT net representation to Maude specifications [START_REF] Clavel | Maude Manual (Version 2.5)[END_REF]. Those transformations rely on a Model-Driven Architecture (MDA) [START_REF] Omg-Mda | Omg mda guide version 1.0.1. formal doc[END_REF] approach, using IOPT nets and Maude metamodels. The resulting Maude specifications support the verification of several properties.

The reference development methodology fully integrate design automation tools, namely the PNML2C [START_REF]PNML2C: PNML2C -A translator from PNML to C[END_REF] and PNML2VHDL [START_REF]PNML2VHDL: PNML2VHDL -A translator from PNML to VHDL[END_REF] tools, which automatically generate, respectively, C or VHDL code from IOPT net models represented in the PNML format [START_REF] Billington | The Petri Net Markup Language: Concepts, Technology, and Tools[END_REF].

Section 2 briefly presents the technological contribution of the paper to sustainability. Section 3 presents the proposed methodology with the help of a running example that will be used throughout the paper for an easier understanding of the development flow. Section 4 describes the executable semantics of GALS systems. Section 5 briefly explains the GALS System representation in Maude language, and the running example verification. Section 6 gives an overview of some related work. And finally section 7 presents some final remarks.

Contribution to Sustainability

This work aims to contribute to the development of GALS systems in a more automated way relying in the Model-Driven Architecture (MDA) approach. This allows the development of complex systems in less time, while being more reliable and less vulnerable to development bugs, due to the fact that the only development errors that are introduced in the system are the modeling errors; there is no manual code generation, either simulation, verification, or implementation codes. Systems with bugs can cause unwanted effects, as in most cases they need to be replaced, wasting energy and resources.

Proposed Methodology

The development flow proposed to GALS systems behavior verification comprises the following steps (described in Fig. 1): -modeler activities: (1) modeling GALS system through IOPT nets; (2) splitting IOPT nets to obtain an IOPT net for each component of the GALS system; -verifier activities: (3) translation from IOPT net models to Maude models; (4) translation from Maude models to Maude concrete syntax language; (5) specification of system properties to be verified; and (6) properties verification.

Running Example

The following example will be used through the paper to present the proposed methodology steps. The example is a very simplified condominium alarm system, which is used to detect events and control alarms of buildings. If an event occurs in one of the buildings, their alarm along with their neighbor buildings must ring.

In this example there are three buildings in a row, the building "1" has the neighbor building "2", the building "2" has the neighbor buildings "1" and "3", and building "3" has neighbor building "2".

System Modeling

This example was modeled by an IOPT net model, and is presented in Fig. 2. As previously mentioned, the IOPT Petri net is a class of non-autonomous Petri nets that extends the Place-Transition (P/T) Petri net class with inputs and outputs. These can be input and outputs signals and also input and output events. Transition firing depends not only on the net marking, but also on the associated input events as well as the guard expression attached to the transition. Output expressions affecting output signals can be associated with places. When compared to Place-Transition nets, IOPT nets have other specific characteristics, as test arcs and priorities, which are described in [START_REF] Gomes | The Input-Output Place-Transition Petri Net Class and Associated Tools[END_REF].

The example has three input events (ev1, ev2, and ev3) associated with transitions governing the evolution of the IOPT net, and three output signals (alarm1, alarm2, and alarm3) that receive the value "1" when the corresponding place has one or more tokens.

Model Splitting

Considering that the system example will be implemented in a distributed way using three controllers (a controller in each building), the IOPT net model presented in Fig. 2, was divided into the three sub-models presented in Fig. 3, through the Net Splitting Operation. The first step of Net Splitting Operation is the definition of a valid cutting set, which finds a set of nodes with specific characteristics that will be used to divide the original net. The splitting was applied through the nodes T1, T2, and T3, generating the resulting sub-modules interconnected through the transitions T1m/T1slave, T2m/T2slave1/T2slave2, and T3m/T3slave, with associated output events (for instance oet1m) in the master transitions, that will be the input events (for instance iet1m) of slave transitions in other components. In this sense, the distributed execution model is composed by a set of parallel components communicating through a set of events.

Executable Semantics

GALS (Globally Asynchronous Locally Synchronous) systems are composed of several interacting components. Each component is synchronous, which means that its evolution is made at specific instants in time, controlled by a local clock. On the other hand, the global system is asynchronous. As there is no global clock synchronizing the components, each component is evolving at its own clock rate. The interaction between components is made sending messages through communication channels. In this sense, GALS systems have interleaving semantics.

IOPT nets were used in this work to model the whole GALS system, as well as GALS components. The firing of the transitions in one IOPT net (net evolution in one component) is done synchronously at specific instants in time (the synchronized paradigm), normally referred as tics or global clock; this means that, for that component, between these instances, net marking will not change. The external clock or tic defines the moments in which enabled and ready transitions can fire. The enabled transition concept refers to the net marking dependency, as usual, while the ready transition concept is associated with the non-autonomous attributes evaluation. The IOPT nets have maximal step semantics, which means that all transitions that are enabled and ready at a specific instant in time will fire in that instant.

Fig. 4 presents a GALS system composed by three sub-models (components), each of them modeled with IOPT nets, representing the three components of the running example obtained through the net splitting operation (each of the clouds is associated with one sub-model of Fig. 3). Each sub-model will be potentially associated with a component running on an autonomous platform. The interaction between the various components is modeled through a set of events and accomplished through specific communication channels, for example direct connections, connections via asynchronous wrappers, NoC (network-on-chip), or any other type of networks, as common in distributed systems.

From the IOPT net model viewpoint, the border of each of these components is a set of nodes composed only by transitions. However, as far as the synchronous paradigm can not be applied to the whole system, the events used to assure the communication between components were replaced by places, modeling the separation of time instants associated with the firing of a master transition (emission of the output event from one component) and the firing of a slave transition (reception of the input event by the other component). Each component is an IOPT net model with a maximal step execution, but the evolution tics of one component is different from the evolution tics of the other components, supporting the global asynchrony. In this sense, between components there is an interleaving execution semantics, while each component is governed by a maximal step execution semantics (each component is in a distinct execution temporal domain).

From IOPT Models of GALS Systems to Rewriting Logic

Objects in Maude

Maude Language

The Maude language is a declarative language [START_REF] Clavel | Maude Manual (Version 2.5)[END_REF]. The basic programming statements are equations and rules, with simple rewriting semantics. Rules can be applied concurrently, which means that System modules can be highly concurrent and non deterministic. In the Maude language it is possible to support objects and distributed objects interactions with rewrite rules. Objects interactions can be made through messages. Maude modules can be used: (1) as programs; (2) as executable specification; and (3) as models, that can be verified. In this work these modules will be used as models in which systems properties will be verified.

MDA Transformations

The MDA approach is used to make the transformation from IOPT net models to the concrete syntax of Maude language. Two transformations were made: (1) model-tomodel transformation using the IOPT net metamodel proposed in [START_REF] Moutinho | Ecore Representation for Extending PNML for Input-Output Place-Transition Nets[END_REF] and Maude metamodel, and (2) model-to-text transformation to obtain Maude code. Model-tomodel transformations were achieved using ATL transformation language and model-to-text transformations were made using MOFScript (a tool for model to text transformation).

GALS System Representation in Maude Language

GALS components modeled by IOPT nets are translated into Maude concurrent objects that interact through asynchronous messages. These messages represent the interleaving semantics of the Globally Asynchronous part of the GALS systems. Maude code of GALS components obtained through the MDA transformation from IOPT net models have interleaving semantics (which is the naturally Maude semantics), although IOPT nets components have a maximal step semantics. This means that the behavior of this Maude code: (1) has exactly the same behavior of the IOPT net model, if and only if, in the each component IOPT net model at most one transition fires at each execution cycle, or (2) has a consistent behavior with the IOPT net model when, the change of, firing at most one transition per execution cycle over several execution cycles, rather than, firing several transitions in just on execution cycle, do not change the GALS components requirements/properties. In the running example, if the transitions T1m and T2slave1 fires in the same execution cycle or if they fire in two consecutive execution cycles, the system requirements remain unchanged.

The generated Maude code for the running example is composed of 2 modules: PETRI_NET_GALS and PETRI_NET_GALS_RULES, an excerpt of it is presented below. Maude notation is presented in Maude manual in [START_REF] Clavel | Maude Manual (Version 2.5)[END_REF].

PETRI_NET_GALS module has the structure of the IOPT nets, in line 2 is made the inclusion of the CONFIGURATION module, which declares sorts representing concepts of objects, messages, and configurations that will be needed to represent the three IOPT nets, and the communication between them (represented by P7, P8, P9, and P10). In line 16 the three IOPT nets class identifiers are defined.

PETRI_NET_GALS_RULES module contains the transition rules, in line 31 is presented the rule for transition T1m, which removes one token from place P1 and creates one token in P2, and one token in P7, that represents a message going from component 1 (building 1) to component 2 (building 2). AP2) >, O2, O3, ( AP7, AP8, AP9, AP10), S => < petri : Petri1 | m ( AP1, P2 AP2) >, O2, O3, (P7 AP7, AP8, AP9, AP10), "T1m " . 53 endm

Verification

As described in Section 3 about the example: (1) if an event occurs in building "1", the alarms of buildings "1" and "2" should begin to ring; (2) if an event occurs in building "2", the alarms of buildings "1", "2", and "3" should begin to ring; and (3) if an event occurs in building "3", the alarms of buildings "2" and "3" should begin to ring. These are the 3 properties that should be verified. Alarm of building "1" rings if the marking of place P1 is equal or greater than 1, and so on.

The generated Maude code, presented in section 5.3, was used in the Maude system to verify the three mentioned properties. To verify property one, it was checked all the possible final states of the system after event "1" occurs. To do this the associated state space containing all reachable states was generated and analyzed. To generate the state space in Maude, the search command (search < petri1:Oid : Petri1 | m (P1, empty) >, < petri2:Oid : Petri2 | m (P3, empty) >, < petri3:Oid : Petri3 | m (P5, empty) >, (none, none, none, none), "" =>! Any:Net .) was used in the code presented in section 5.3, and to show it the command (show search graph .) was used. It was verified that all possible final states of the system after event "1" occurrence are (P2=1, P3=1, P4=1, P5=1), (P2=2, P4=2, P5=1, P6=1), (P2=1, P3=1, P4=2, P6=1) or (P2=2, P4=3, P6=2). Analyzing them, it can be concluded that the places P2 and P4 have always one or more tokens, which means that alarms of buildings "1" and "2" ring in this situation, and can be concluded that property one is successfully verified. Properties two and three were also successfully verified.

Due to space limitations, it is not possible to present the complete state space, even for such simple example in order to make evident the referred verified properties. Instead, a simplified system composed by buildings 1 and 2 is considered. Fig. 5 presents the partial state space of this simplified system, considering the sub-models of Fig. 3 and Fig. 4 associated with buildings 1 and 2, which means the models with the transitions T1m, T1slave, T2m, and T2slave1, and places P1, P2, P3, P4, P7, and P8. This partial state space has 9 states, presented in Fig. 5, while the full state space has 45 states. Each node of the state space presented in Fig. 5 shows the marking of the relevant places, where the four nodes with P7 and P8 holding no tokens are the ones observed in the initial model of Fig. 2.

Related Work

Since most of the embedded systems circuitry is made of synchronous circuits, they became the starting point in the development of GALS systems. With this in mind, there are several works proposing architectures, property verification, implementations, and prototyping for GALS systems.

Some authors propose a verification approach for GALS systems (e.g. [START_REF] Doucet | A Veri¯cation Approach for GALS Integration of Synchronous Components[END_REF]), taking as starting point the description of the systems' behavior using textual languages, instead of graphical-based descriptions like the ones being proposed in this paper. Other authors use Petri nets to represent GALS systems behavior and to verify its properties (e.g. [START_REF] Dasgupta | Modeling and Performance Analysis of GALS Architectures[END_REF]); however, the methodology does not cover the entire GALS systems development flow, that starts with Petri net models. In [START_REF] Gomes | Formal Methods for Embedded Systems Co-design: the FORDESIGN Project[END_REF], a full development flow for embedded systems was proposed through automatic code generation, from Petri net models, but without attempting to answer the specific questions of GALS systems.

To the best of our knowledge, no works addresses the complete development flow (modeling, simulation, verification, and implementation) of GALS systems through automatic code generation based on non-elementary Petri nets.

Conclusions

The methodology for specification and verification of GALS systems using IOPT nets as modeling formalism was shown to be adequate in the testing phase of this work. In all the validation examples it was possible to model distributed execution of embedded systems as a GALS system using IOPT nets, and to verify systems properties with Maude. Maude code was always automatically generated from IOPT nets through model-to-model and model-to-text transformations.

The main conclusion is that the proposed development methodology has several advantages compared to a development methodology that does not use models. It also takes advantage from the usage of Petri nets as the underlying model of computation, namely (1) the model clearly describes the system's behavior; (2) it is possible to start modeling the system with one centralized model, which is then partitioned into a set of modules, the components of the GALS system; and (3) the system verification and implementation codes are automatically generated from the model, which decreases the development time and the potential errors of manual code generation.

Fig. 1 .

 1 Fig. 1. Activity Diagram to GALS Systems Behavior Verification.

Fig. 2 .

 2 Fig. 2. IOPT model of an oversimplified condominium alarm system.

Fig. 3 .

 3 Fig. 3. IOPT sub-models resulting from the Net Splitting Operation.

Fig. 4 .

 4 Fig. 4. IOPT nets modeling a GALS system.

Fig. 5 .

 5 Fig. 5. Partial state space of the example.

Acknowledgments. This work is supported by the cooperation project funded by Portuguese FCT through the project ref. 4.4.1.00-CAPES, and by Brazilian CAPES through the project ref. 236/09. The first author work is supported by a Portuguese FCT (Fundação para a Ciência e a Tecnologia) grant, ref. SFRH/BD/62171/2009.