Mickaël Kerboeuf
email: mickael.kerboeuf@irisa.fr

Jean-Pierre Talpin
email: jean-pierretalpin@irisa.fr

Encapsulation and Behavioral Inheritance in a Synchronous Model of Computation for Embedded System Services Adaptation

Keywords: synchronous programming, process calculi, encapsulation, reuse and behavioral inheritance

Because it encourages the incremental development of software and the reuse of code by abstracting away implementation details, object orientation is an intuitive and sensible way to conceive large software out of existing application components and libraries. In practice, however, object-orientation is most of the time applied and used with sequentiality in mind. This practice may sometimes be conceptually inadequate for, e.g., control-dominated reactive system components.

We address this issue by proposing a process calculus that melts the paradigm of synchronous programming to key object-oriented features: encapsulation and behavioral inheritance with overriding by means of specific algebraic concurrency combinators. This framework provides support for the reuse of components and, more specifically, for the adaptation of embedded systems with new services.

Cast in the context of a strict interpretation of the synchronous hypothesis, the proposed model supports a static interpretation of inheritance: overriding is resolved at compile-time (or link-time) and inheritance combinators are translated into primitive synchronous ones. This compilation technique puts object-orientation to work in a syntax-oriented model of synchronous concurrency that naturally supports the incremental, refinement-based design of concurrent systems starting from encapsulated and reused application components.

The benefits of our approach are illustrated by a concrete and practical example: the adaptation of services to a plain old telephone service specification.

Introduction

Object-orientation favors an incremental development of sequential software by taking into account the structural and behavioral refinement of program components using the concept of inheritance. Object-orientation enables the reuse of program libraries by abstracting away implementation details from the necessary information contained in an interface, a signature, a type. A few object-oriented concepts, materialized by a small set of operators, with a clear and formal semantics, provide effective solutions for the design of large sequential software.

Moving to the design of concurrent systems, however, the picture is not that satisfactory. It is indeed a very challenging issue to give an object-oriented account to concurrency that meets the same degree of simplicity as for sequential software.

The synchronous hypothesis is an efficient approach to the design of concurrent and controldominated software. Synchrony consists of assuming that communications and computations are instantaneous during the successive execution steps of a system. Making this hypothesis is beneficial to system design. It allows the designer to focus on the logics of the system, characterized by synchronization and causal relations between events, and abstract away timing issues until a latter stage of system design (until its mapping on a given architecture).

We propose a new calculus of synchronous processes that supports the incremental, objectoriented design of synchronous system components. This model consists of a core algebraic formalism, akin to Pnueli's synchronous transition systems [START_REF] Pnueli | Fair synchronous transition systems and their liveness proofs[END_REF], that melts the paradigm of synchronous programming to the notions of encapsulation and of inheritance with overriding, borrowed to object-oriented programming. The classical notion of class is introduced as an abstract parameterized and encapsulated process. An object is an instance of a class. An inheritance operator is defined at the class level. It refines the behavior of an initial class with a special class that corresponds to the notion of wrapper. A concurrent behavioral inheritance operator is defined in terms of synchronous composition by introducing a technique of renaming or rewriting. This intuitive and syntax-oriented approach offers flexible implementation possibilities: it can both been used to interpret behavioral inheritance in the context of a functional architecture consisting of process signatures and components, it can be used to combine, compile and optimize concurrent objects, it can be used to link and load separately compiled modules. In conclusion, it fully supports incremental design, reuse and encapsulation of objects for the component-based engineering of concurrent software.

Overview

In section 2, we first give a brief overview of the synchronous paradigm before introducing the core algebraic model of implicit synchronous transition systems (Ists). Section 3 gives the syntax and semantics of object orientation of this model: it is extended with http://www.irisa.fr/prive/talpin (Jean-Pierre Talpin).

a mechanism for encapsulation, and with synchronous behavioral inheritance. A technique for performing a static resolution of behavioral inheritance is then presented. The benefits of this approach are probed and illustrated in section 4 by considering the concrete and practical example of the adaptation of services of a Pots: a plain old telephone service.

2 A synchronous approach for the design of reactive systems

Synchrony and asynchrony

Synchrony and asynchrony are fundamentally different concepts in nature. Asynchrony is traditionally relevant for reasoning on distributed algorithms and for modeling non-determinism, failure, mobility. It meets a natural implementation by networked point-to-point communication. Synchrony is more commonly viewed as specific to the design of reactive systems and digital circuits. In this context, timeless logical concurrency and determinism are suitable hypotheses.

Time prevails in an asynchronous design as communication and computation times need to be taken into account at every level of the system under design. The absence of a common reference of time requires one to manage the local execution context of each application component and maintain the expected global behavior of the system. In this process, non-determinism incurred by asynchronous interactions increases the number of possible sequences of interleaved events. This makes the proof of suitable invariants (safety properties, absence of live-locks or dead-locks) harder.

By contrast, a synchronous design hypothesis consists of assuming that communications and computations are instantaneous between the successive execution steps of a system. Making this hypothesis is beneficial for design. It allows the designer to focus on the logics of the system, characterized by synchronization and causal relations between events, and abstract away timing issues until a later stage of the design (its deployment on a given architecture).

In the synchronous approach of concurrency, time is abstracted from computations and communications. As computing takes no time, the behavior of a computational unit can be seen as a sequence of simultaneous events, ordered by causal relations. As communication takes no time, a message from a unit to another is sent and received at the same logical instant. Thus, synchrony offers a global view of the interaction in a system where the only notions relevant to verification are simultaneity of events or causal precedence between events. Back to the real world, where physical time has to be taken into account, the synchronous hypothesis can be validated by checking that the program reacts rapidly enough to perceive the events in suitable order, or by checking the so-called property of endochrony. This property expresses that a unique sequence of interleaving events can be inferred from the synchronous specification, regardless of the delay induced by each event.

Synchronous languages

Synchrony imposes a discretization of the behavior of a system: a synchronous specification is a sequence of instantaneous reactions to events. Imperative synchronous languages like Statecharts [START_REF] Harel | Statecharts: a visual formalism for complex systems[END_REF] or Esterel [START_REF] Berry | The Esterel synchronous programming language: design, semantics, implementation[END_REF] focus on the sequence of events. Declarative (data-flow) synchronous languages such as Lustre [START_REF] Halbwachs | The synchronous data-flow programming language Lustre[END_REF] or Signal [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF] focus on the elementary reactions: a program handles streams of values, the signals. During a given execution step, each signal is either "present" or "absent" (but a computation is never "in progress").

Building upon previous work on casting the synchronous multi-clocked model of computation of Signal into notions of process calculi [START_REF] Talpin | Model checking robustness to desynchronization[END_REF], we define an algebraic model of implicit synchronous transition system, which we call Ists, akin to Pnueli's synchronous transition systems (Sts, [START_REF] Pnueli | Fair synchronous transition systems and their liveness proofs[END_REF]), where absence is explicit (for verification purposes) and to the Signal modeling language, where absence is implicit.

A calculus of synchronous processes

The Ists formalism aims at supporting the introduction of new concurrency concepts to ease the compositional modeling of reactive systems starting from a minimal set of constructs.

Ists borrows an operator of non-deterministic choice between behaviors from Sts [START_REF] Pnueli | Fair synchronous transition systems and their liveness proofs[END_REF] in order to support a structural equivalence relation which enables syntax-oriented behavioral reasoning on processes. Ists differs from Sts by letting absence be an implicit (non syntactic) notion in the model (as in Signal). The equivalence between Signal and the Ists is shown in [START_REF] Kerboeuf | Orientation objet d'un calcul de processus synchrones[END_REF].

In the remainder of this section, we first give an informal overview of the Ists centered around an example. Then, its formal syntax and operational semantics are detailed. They are summarized in appendix A.

Overview of the Ists formalism

In Ists, a synchronous process consists of a set of relations or partial equations on signals.

A signal is identified by a name x which, at any logical instant of time (each transition), either carries a value v (and then we say that this signal is present), or not (and we say that it is absent, making use of the special mark ⊥ to denote this absence). The clock of a signal x (denoted by x) is the set of instants when this signal is present.

Each elementary equation or transition relation of a process specifies a relation between the values of its input and output signals.

For instance, (z=x + y) is a primitive addition process. It relates the the integer input signals x and y to the integer output signal z. The values carried by x, y and z, but also their clock x, ŷ and ẑ, are related: x, y and z are present at the same time, and when x and y carry the values c and d, then z carries the value c + d. Usual operators on numbers and booleans are provided. Identity (or assignment) is simply written (y=x).

Guards are primitive processes. They enable to trigger reactions or transitions under certain conditions. However, they do not define any output signal. For instance, the guard (when x) (resp. (when not(x))) is active only if the boolean input signal x carries the value true (resp. false). The guard (event x) is less restrictive. It is active only when the input signal x is present.

The silent process, denoted by 1, enables stuttering: it is active when all signals are absent. State transitions are implemented by the primitive process (y=(pre c) x). The function (pre c) defines a register which initially contains the value c. When the input signal x is present with the value d, the value c is sent along the output signal y, the value d is stored in the register and the process becomes (y=(pre d) x).

The synchronous composition of two processes p and q is written p | q. The transition of p | q is performed by the simultaneous transition of p and q and with the same context (by context, it is meant that, if p assumes any signal x present with a value v or absent, then q should simultaneously make the same assumption during its transition). Non-deterministic choice is written p+q. It consists of choosing to execute either p or q during a given transition. Restriction p/x is used to limit the scope of a signal x to the process p.

Example 1 Let balance be a process that implements a voting balance counter, i.e. it counts the number of times a signal x is true minus the number of times it is false. The balance is written:

balance def = 1 +   (m=(pre 0) n)    (when x) | (n=m+1) + (when (not x)) | (n=m-1)       /m
At the top-level, the balance consists of a choice between a process activated when x is present, and the silent process, to enable stuttering. If x is present, there are two possible transitions.

The first transition is triggered if (and only if )

x is true (it is guarded by when x). Simultaneously (i.e. by synchronous composition), m takes the previous value of n (initially 0) and n takes the value of m + 1. The second transition is triggered iff x is false (it is guarded by when (not x)). If so, the balance count n is decremented.

The balance receives the input x and defines the output n. The signal m is used to calculate the current value of n given its previous one. It is defined locally. A possible sequence of values of the signals x, m and n in time can be depicted by considering the following possible trace of the execution of balance:

input: x ff ff tt ⊥ ff tt tt tt . . . local : m 0 -1 -2 ⊥ -1 -2 -1 0 . . . output: n -1 -2 -1 ⊥ -2 -1 0 1 . . .
When x is false (value ff ), the reaction guarded by when (not x) is triggered. When x is true (value tt), the reaction guarded by when x is triggered. When x is absent (mark ⊥), the silent reaction guarded by 1 is triggered. Notice that the signals m, n and x are synchronous: they are all absent or present at the same time.

Formal syntax

We now introduce the syntax of Ists more formally. To do so, a few notational conventions used along the article are in order. Let A be a set and a ∈ A. We write A k for the set of sequences of length k ∈ N of elements of A. We write A * for k∈N A k . A sequence of any length is denoted by ã ∈ A * , and we write (a 1 , . . . , a k ) ∈ A k for a sequence of length k.

We write Z and B = {tt, ff } for the domains of integers and booleans and C = B + Z for the set of constants. We consider an infinite countable sets of signals x, y ∈ X and functions f, g ∈ F (we assume X and F disjoint:

X ∩ F = ∅).
A process p in Ists consists of elementary transitions (y=(pre c)x) and simultaneous equations on signal names (ỹ=f x) combined using synchronous composition p | q and non-deterministic choice p+q. The sequences ỹ and x of signals required and defined in an equation (ỹ=f x) can be empty (to capture guards, constants and silence), and the empty sequence is denoted by (). Restriction p/x is used to limit the scope of a signal x to the process p.

p, q ::= ỹ=f x (equation)

| y=(pre c)x (transition) | p | q (composition) | p+q (choice) | p/x (restriction) c, d ∈ C = B + Z (constant) f, g ∈ F (function) x, y ∈ X (signal) (x 1 , . . . , x k ) ∈ X k (sequence)
x ∈ X * = k∈N X k

Operational semantics of synchronous processes

The operational semantics of Ists consists of a set of axioms and rules that define the possible transition of a process by induction on its syntax. We first introduce the algebraic laws of Ists.

We write fv(p) and dv(p) for the set of free and defined names of a process p. Informally, a name x is free (resp. defined) in p if it occurs unbound in an action (resp. unbound and is an output signal of a base process) of p. We write p[x/y] for the substitution of y by x in p and dom S for the domain of a substitution S. The operational semantics of a process p is defined by the relation p e -→ q. It defines the possible transitions e of a process from an initial state p to a final state q. The term e represents the events that are present in the environment of the process at the instant at which the transition takes place. It is constructed by induction on the term p by combining events from every sub-term of p. An event is defined by the association of a signal x to a value c in e, written x → c. It denotes the value c carried by the signal x at the (logical) instant denoted by e. A signal x can alternatively be regarded as absent (i.e. x is absent iff x ∈ dom e). e, f ∈ E = X C * (environment)

fv(ỹ = f x) = ỹ ∪ x dv(ỹ = f x) = ỹ fv(p+q) = fv(p | q) = fv(p) ∪ fv(q) dv(p+q) = dv(p | q) = dv(p) ∪ dv(q) fv(p/x) =
Rule (eqv) takes into account the syntactic recombination of processes. Rule (or) is the choice rule. It allows a transition from p+q to r+q with e if a transition from p to r with e is possible (resp. from q, by rule (eqv)). Rule (let) implements the scope restriction of a name x in a process p. We write e x for the context e outside of the scope of x (x ∈ dom e x , for all x).

(eqv)

p ≡ p e -→ q ≡ q p e -→ q (or)

p e -→ r p+q e -→ r+q (let) p e -→ q p/x e x -→ q/x
Rule (and) implements synchronous composition. It stipulates that the simultaneous transitions from p to p with e and from q to q with f are valid iff e and f agree on the assignment to all signals shared by p and q, as defined by the side-condition. More precisely, a signal x shared by p and q (x ∈ fv(p) ∩ fv(q)) must be simultaneously present or absent in both p and q (x ∈ dom e ⇔ x ∈ dom f ) and, when present (x ∈ dom e ∩ dom f ), with the same value (e(x) = f (x)).

(and)

p e -→ p q f -→ q p | q e ∪ f ----→ p | q iff ∀x ∈ fv(p) ∩ fv(q),      (x ∈ dom e ⇔ x ∈ dom f ) ∧ (x ∈ dom e ∩ dom f ⇒ e(x) = f (x))
Axiom (com) defines the meaning of primitive functions (and, in extenso constants). At a given transition, an equation (ỹ=f x) relates the values d ∈ C * carried by the sequence of input signals x to the values c ∈ C * carried by the sequence of output signals ỹ according to a (possibly partial) function f . A partial map δ defines how primitive functions (e.g. identity, equality or boolean and integer functions) relates these values:

δ : F (C * C * ) ∀f ∈ dom δ, ∃k, k s.t. δ(f ) : C k C k
If a function f does not return any output value (i.e. δ(f ) : C k C 0 ), f implements a guard, such as when and event. In this case, we write (when x) for (()=when x). If f does not require any input value (i.e. δ(f ) : C 0 C k ), f implements a constant signal, like true and false, which stands for the boolean constants tt and ff . In this case, we write (x=true) or (x=tt) for (x=true ()). The silent process 1 is defined by the function which neither defines any output signal nor requires any input signal (i.e. δ(f ) : C 0 C 0 ). We just write 1 instead of (()=1 ()).

δ(+) = {((c,c ) → (d)) | (c,c ,d) ∈ Z 3 ∧ d = c+c } δ(id) = {((c) → (c))|c ∈ C} δ(=) = {((c,c) → (tt))|c ∈ C} ∪ {((c,c ) → (ff ))|c = c } δ(event) = {((c) → ()) | c ∈ C} δ(when) = {((tt) → ())} δ(true) = {(() → (tt))} δ(false) = {(() → (ff ))} δ(1) = {(() → ())}
The side condition of (com) makes the use of δ explicit. It stipulates that the transition across (ỹ=f x) is possible with e iff e is defined for (and only for) ỹ and x, and if the values carried by ỹ and x satisfy δ(f ). Notice that e : X C * , and hence, we write e(x) for the sequence (e(x 1 ), . . . , e(x n )) where (x 1 , . . . ,

x n ) = x. (com) (ỹ=f x) e -→(ỹ=f x) iff dome = x ∪ ỹ ∧ δ(f )(e(x)) = e(ỹ)
¿From the axiom (com), the transition of guards, constants and silence can easily be deduced.

(z=x+y)

x → c, y → d z → c+d ----------→(z=x+y) 1 ∅ ---→ 1 x=tt x → tt ----→ x=tt x=ff x → ff -----→ x=ff when x x → tt ----→ when x event x x → c ----→ event x
Notice that (when x) and (x=tt) have the same behavior. However, (when x) only uses the signal x (it is a control structure) whereas (x=tt) defines the signal x (it is an assignment).

Example 2 To manifest the preemption capability of choice and composition in the Ists let us consider a choice expression where a signal

x only appears in one of the alternatives: p ≡ y=x + y=0 and put the expression p in a context p | q such that q ≡ x=1. By definition of the rule (or), either y=x or y=0 react, assuming an environment e 1 such that dom e 1 = {x, y} and e 1 (y) = e 1 (x) or producing an environment e 2 such that dom e 2 = {y} and e 2 (y) = 0. By definition of the rule (com), q reacts by emitting the value 1 along x, producing dom f = {x} and f (x) = 0. Let us consider the possible combinations of these two expressions by the rule (and). We need to respect the side-condition of that rule, which stipulates that x, the signal shared by p and q, is present in e iff it is in f . The only choice is e = e 1 : the presence of x in the context q has preempted the reaction y=0 in the expression p. Had p been the expression ((y=x + 1) + (y=x -1)) then choice in the context q would have been non-deterministic, allowing either the left or right alternative to be fired.

Axiom (pre) defines the transition that corresponds to evaluating y=(pre c)x. The syntactic update performed in the axiom allows to load the initial value c in the output signal y and to simultaneously store the value d carried by the input signal x.

(pre) (y=(pre c)x)

x → d, y → c ---------→(y=(pre d)x)
A summary of the syntax and the operational semantics of Ists is given in appendix A.

Related models

The synchronous interaction model in the Ists is primarily related to synchronous formalisms. It essentially differs from related process calculi such as Sccs [START_REF] Milner | Communicating and Concurrency Prentice-Hall International[END_REF] in the role played by absence.

For instance, consider the Sccs process: ā×(a+ b). If the event ā occurs, the term on the right has the choice to fire a (and communicate), or to fire b. In the Ists, only the first transition is possible (for the same reason as for example 2): the action b can only be chosen if a (the other arm of the choice) is absent. This difference reflects the role of absence in synchronous formalisms. Another example is the process balance: the transition by 1 is possible only if x is absent. Indeed, if x is absent, then 1 is the only term that can be triggered, since all other terms assume the presence of x. In other words, the absence of x is the triggering event for the silent transition 1.

Object-orientated aspects

In the previous section, we presented the Ists formalism and the synchronous hypothesis on which it is founded. In this section, we define its encapsulated version, Objective Signal, and then further augment it with a behavioral inheritance operator. To begin with, the principles of our synchronous object orientation are explained. Then, encapsulation and inheritance in Objective Signal are presented.

Motivations and principles

We essentially aim at defining formal methods enabling the reuse of objects and classes by employing an inheritance mechanism. This mechanism allows to adapt the behavior of a class or an object from the outside, without having to rewrite its implementation. Some important features of the object-oriented paradigm such as polymorphism, first-class objects and dynamic object creation are absent from our model. Their combination to a synchronous model of computation would raise issues, such as dynamic memory management, that are hardly compatible with the requirements of synchronous processes to execute within bounded (a priori predicted) space and time. We hence focus on the more fundamental merits of the object-oriented approach to provide means to favor the reusability of components and investigate the addition of encapsulation and inheritance mechanisms in a synchronous framework.

Objects and synchronous behaviors

An object is usually defined by a set of methods and attributes. Formally, an object is often represented by a record: an ordered and labeled collection of methods and attributes. The values associated to the attributes of an object represent its state. Methods enable to read and/or write the state of an object. The environment of an object is itself composed of several objects.

In conventional approaches to concurrent object-oriented programming, method calls are asynchronous. As an example, the next figure shows the interaction of an object, that defines the attribute mem and a method y, with its environment, which provides the method x.

Calling y (step 1) triggers a call of x (step 2), performs an update of mem when x answers (step 3), and returns the last value of mem (step 4). The main departure of our framework from asynchronous models to concurrent objectorientation lies in the synchronization relations between an object and its environment: a defined signal can only be called (i.e. it is present and its value can be fetched) under some conditions and by some stimulus. The synchronization relations of an object are given by the clocks of the signals it involves. Remember that the clock of a signal denotes the instants at which the signal is present or triggered. Yet, notice that to conform with the synchronous paradigm, the call (i.e. the trigger) of a signal and its answer (i.e. its reaction) are simultaneous (computation and communication take no time).

The next figure illustrates the interaction between a process (y=(pre c) x) and its environment. The picture on the right is a reformulation of the figure on the left which makes the analogy to the asynchronous interaction explicit. The object-oriented representation of a synchronous process is a record that contains the signals it defines. At first glance, we need to add an encapsulation mechanism to that structure, in order to create abstract processes (classes). The defined signals of a synchronous process p are characterized by clocks (sets of triggering instants) and by the values they carry.

Next, we add inheritance (in the aim of supporting reuse and overriding). For the defined signals of an object, overriding implies the capability of modifying the result of the signal as well as its clock. Notice that synchronous composition and choice already (partially) achieve this requirement. Choice allows to extend a process with a new behavior (i.e. the definition and the clock of a signal) and synchronous composition allows to constrain a signal with new synchronization relations.

Still, we need to be able to reset the values carried by a signal. To this end, we introduce an asymmetric synchronous composition over classes, that enables to override the definition of a signal and to use its previous definition via the classical notion of super-variable.

Inheritance and static resolution

The Ists formalism, extended with encapsulation and inheritance, aims at melting object orientation, concurrency and synchronous data-flow within a same formal framework. However, perfect synchrony incurs strong specification requirements, notably on the resources of the system (memory size, computation time), which need to be bounded. For that reason, it is for instance not possible to recursively use a signal without introducing a delay between each recursive call or to dynamically allocate new resources at runtime. However, the topology of interaction being known statically enables to check precisely and efficiently the system safe.

Hence, in Objective Signal, the creation of an object (using a classical "new" class instantiation statement), builds the object from the model of the class and activates it. As a consequence, inheritance needs to be resolved statically, which may seem quite restrictive. However, our aim is less about defining a new model of execution (with resource allocation) and more on defining a suitable model for the specification of system behaviors using encapsulation and providing reusability.

Related works

The object-orientation of concurrent calculi has been a widely investigated topic. In [START_REF] Pierce | Concurrent Objects in a Process Calculus Proceedings Theory and Practice of Parallel Programming[END_REF], Pict, an object-oriented concurrent language founded on the π-calculus, is presented. It implements very powerful features like encapsulation, dynamicity and mobility, but its mechanism for reusability does not implement an inheritance mechanism taking into account compositional and structural modification of systems. In [START_REF] Fournet | Inheritance in the Join Calculus[END_REF], a static and syntactic-oriented inheritance mechanism is defined for the Join-Calculus [START_REF] Fournet | The Reflexive CHAM and the Join-CalculusProceedings of the 23rd ACM Symposium on Principles of Programming Languages[END_REF].

Objective Signal relates to that approach by adding a similar, syntax-oriented, mechanism to a synchronous formalism. Different approaches to reactive and synchronous concurrent objects have also been proposed in [START_REF] Boussinot | Two Semantics for a Language of Reactive Objects Research report n[END_REF][START_REF] Boussinot | Reactive Objects Research report n[END_REF], which do not enables the overriding of the behaviors of objects.

Instead of adding object-oriented features to a synchronous or asynchronous concurrent formalism (such as the π-calculus or the Ists), some further related works have investigated the extension of object-oriented formalisms with concurrency. Most of the approaches considered in this field are founded on the object-oriented calculus impς of Abadi and Cardelli [START_REF] Abadi | A Theory of Objects[END_REF], featuring classes, inheritance, prototyping, dynamic creations, subtyping and method specialization. In [START_REF] Gordon | A Concurrent Object Calculus: Reduction and Typing Proceedings High-Level Concurrent Languages[END_REF], concς is defined to encompass concurrent objects by including concurrency operators borrowed to the π-calculus. In [START_REF] Flanagan | Object Types against Races Proceedings International Conference on Concurrency Theory[END_REF], concς is further extended with a calculus of dependent types to analyze and avoid race conditions in concurrent specifications (i.e. the simultaneous access to the same ressource). The synchronous paradigm on which Objective Signal is founded does not aim at matching the expressive capability of concς yet casts encapsulation and behavioral inheritance in a (synchronous) framework were design errors such as race conditions can easily be analyzed and detected.

Encapsulation

Overview of encapsulation in Objective Signal

o = new [C] .       (x=C.x+1) | (y=self.x-1)    /x    o ;    (o .x=o.x+1) | (o .y=o .x-1)    /o .x
The renaming of signals and paths is achieved by a syntactic operator bind o σ which selectively applies a substitution σ to the class parameters that appear on the right hand-side of equations (signal calls), and changes each defined signal x into a path o.x. Here, the name o corresponds to the name of the current instance. We write o.ỹ for the tuple (o.y 1 , . . . , o.y n ) where (y 1 , . . . , y n ) = ỹ.

bind o σ (p a | q a ) = bind o σ (p a ) | bind o σ (q a ) bind o σ (p a +q a ) = bind o σ (p a )+bind o σ (q a ) bind o σ (p a /x) = (bind o σ (p a ))/o.x bind o σ (ỹ=f ñ) = (o.ỹ=f (ñσ))

Operational semantics

We define the operational semantics of the encapsulated processes p. The core operational semantics of Ists remains unchanged: we just need to additionally take instantiated paths o.x into account (instead of simply signal names x). Thus, an environment e is now a partial function from paths to constants:

e, f ∈ E = (O × X ) C * (environment)
The creation of a class instance occurs at run time, when a reaction containing an object definition is triggered. We need to introduce a rule for that purpose.

C resettable balance def = [C] .   1 +   (m=(pre 0) self.n)    (when C.x) | (n=self.m+1) + (when (not C.x)) | (n=self.m-1)       /m    & [C ] . [] .        1 + (n=super.n) +        (event super.n) | (event C .r) | (n=0)              

As its syntax suggests, inheritance & is basically a sort of oriented (and non commutative) synchronous composition. There are two parts in the interface of a wrapper. The first part ([C ] in the example) enables to reuse the parameters of the initial class ([C] of C balance ). The second part possibly introduces new parameters ([] in the example: no new parameters).

Stuttering is still enabled by the wrapper (reaction 1). The second reaction (n=super.n) is enabled if and only if r is absent: it can be triggered in a context that provides values for (and only for) n and super.n (recall example 2). In particular, the presence of r (referenced in the third reaction of the process) inhibits the reaction (n=super.n). Hence, if r is absent, the second reaction is triggered and the previous version of n prevails.

The third reaction specifies that n provides 0 instead of super.n when r, provided the class by C (alias C) is present. We introduce a renaming scheme to merge C balance and its wrapper into a unique base class. C resettable balance is then equivalent to the following class:

C resettable balance ≡ [C] .                                     1 +   (m=(pre 0) self.n)    (when C.x) | (n n n =self.m+1) + (when (not C.x)) | (n n n =self.m-1)       /m 1 + (n=self.n n n ) +        (event self.n n n ) | (event C.r) | (n=0)                          /n n n                  
Renaming in the initial class and the wrapper is selective. The signal n is overridden. In order to enable the coexistence of its initial definition and its new one within a same structure, n is changed into a new name n n n (whose scope is restricted), only where it is initially defined.

Where n is only used (in the definition of m), n remains unchanged. Thus, the signal m still maintains a delayed version of (the new version of) n.

The reactions added by the wrapper are also adapted. The previous references to the "super" signal n are changed into references to the "self " signal n n n . Notice that it is not possible to extend the initial behavior just by adding a reaction outside the scope of m, because when n is reset to 0, m must register it. It is therefore not possible to achieve the modification without inheritance, or without breaking the encapsulation.

To create an instance of the modified class, we must extend its environment with the signal r.

Consider the following process:

C env def = []. 1 + (x=tt)+(x=ff ) | (r=tt)+1 resettable balance = new C resettable balance (env) | env = new C env () A possible
input : r ⊥ tt ⊥ ⊥ ⊥ tt ⊥ ⊥ . . . private : m 0 -1 0 ⊥ 1 0 0 1 . . . private : n n n -1 -2 1 ⊥ 0 1 1 2 . . . public : n -1 0 0 0 1 ⊥ 0 0 0 0 1 2 . . .

Formal syntax

The definition of a wrapper uses the parameters self and super. They respectively refer to the whole modified class and to the initial class modified by the wrapper. Among the other parameters of a wrapper, it is necessary to distinguish between the parameters that are already used in the initial class (first part of the interface), and the new parameters introduced by the wrapper (second part of the interface). In the previous example, the wrapper reuses the parameter C of balance. Thus, as expected, the signals x and r are provided by the same object. We could have specified a new parameter in the second part of the interface in order to let the signals r and x be provided by potentially different classes.

[ Cr ].[ C].[p a ] (wrapper)

Wrappers can be considered as a general form of class. Indeed, a base class can be seen as a wrapper which neither uses the parameters of the initial class ( Cr = ()), nor the reference super in its definition:

[ C].[p a ] def = [].[ C].[p a ] and ∀x ∈ X , super.x / ∈ fv(p a ) (base class)
The following syntax extends second level (classes) of the encapsulated Ists with wrappers and inheritance:

C ::= [ Cr ].[ C].[p a ] | C&C (class) p a , q a ::= p a | q a | p a +q a | p a /x | ỹ=f ñ | y=(prec)n (abstract process) n ::= C.x (abstract path) C ∈ M ⊃ {super, self} (class parameter)

A spatial version of the method lookup algorithm

In classical object oriented programming languages like SmallTalk, the semantics of inheritance is given by the method lookup algorithm. When a method is called, its definition is looked up in the receiving class. If it is not found, the search starts again in its super class. When a method uses another method of the same class (reference to this) the search starts in the current class. When a method of the overridden class is called, the search start in the super class. In Objective Signal, a class C can be built incrementally using inheritance:

C def = C 1 &C 2 & . . . &C n
The call of a signal x initially (and only) defined in C 1 triggers a signal lookup mechanism based on the same classical principle of object-oriented programming. However, thanks to the synchronous hypothesis, the signal lookup is synchronous to the call! Thus, the temporal iteration of the classical method-lookup algorithm is replaced by a spatial one. We introduce a syntactic operator called lookup which aims at deploying the classes C 1 . . . C n in a unique base class.

Along the way, the defined signals and their different overridden versions coexist after a specific renaming. This renaming is achieved by using a substitution mechanism and a selective application operator L. Let C 1 be a base class and p a its definition. Let C 2 be a wrapper and q a its definition. If a signal x of C 1 (i.e. x ∈ dv(p a )) is overridden in C 2 (i.e. x ∈ dv(q a )), the occurrences of x in p a are replaced with a fresh name. This renaming is achieved by the following substitution:

β paqa :      dom β paqa = dv(p a ) ∩ dv(q a ) ∀x ∈ dom β paqa , xβ paqa = x / ∈ dv(p a ) ∪ dv(q a )
However, this substitution must be selectively applied. Indeed, the calls must remain unchanged, and now, they refer to the new version of the signal. For that purpose, we use the following operator:

L β ( p a | q a ) = L β (p a ) | L β (q a ) L β ( p a +q a ) = L β (p a )+L β (q a ) L β (p a /x) = L βx (p a ) /x L β (ỹ=f ñ) = (ỹβ)=f ñ
A wrapper can modify another wrapper. The syntactic operator lookup unifies the interfaces of two base classes (and/or wrappers) and applies L on them. In the result, the overridden (i.e. renamed) signals are restricted locally.

lookup    [ Cr1 ] . [ C1 ] . [p a ] & [ Cr2 ] . [ C2 ] . [q a ]    = [ Cr1 ] . [ C1 C2 ] .       L βp aqa (p a ) | q a [ Cr1 C1 / Cr2 ][self.(xβ paqa )/super.x]    /im β paqa   
The initial class (which can itself be a wrapper as well) uses the parameters C1 and reuses the parameters Cr1 . The last ones refer to the parameters of the class that the wrapper is supposed to modify. C1 and Cr1 can be reused (via the alias Cr2 ) in the wrapper of the wrapper. In the result, Cr1 remains unchanged. The parameters C1 of the initial class and the parameters C2 of the wrapper refer to the classes used in the top-level class. Then, they both appear in the interface of the result. The initial definitions p a and q a are synchronously composed. L βp aqa is applied on p a to rename overridden definitions but not their calls. In q a , the parameters of the initial class Cr1 C1 replace the corresponding parameters Cr2 in the wrapper. The previous versions of overridden signals super.x are replaced by their new names xβ paqa in the global component, now referred to as self. All these new names (im β paqa ) are restricted to the definition of the new class.

Most of the time, the modified class is not a wrapper and its wrapper does not introduce any new parameter. In this case, Cr1 = () and C2 = (). The wrapping of this class naturally yields to another base class with the same interface (as in the previous example C resettable balance ):

lookup    [ C1 ] . [p a ] & [ Cr2 ] . [ ] . [q a ]    = [ C1 ] .       L βp aqa (p a ) | q a [ C1 / Cr2 ][self.(xβ paqa )/super.x]    /im β paqa   
On more complex classes, the lookup operator is applied recursively. Base classes and base wrappers are kept unchanged by it.

lookup ( C&C ) = lookup ( lookup(C)&lookup(C ) ) lookup(C) = C (with C: base class)

Operational semantics

To define the rule for the resolution of inheritance at runtime, we upgrade the rule (inst) by adding the renaming mechanism on the given class C. The rule can be applied only if the result of lookup is a base class.

(inst)

lookup(C) = [ C].[p a ] bind o [o õ/self C] (p a ) e -→ p o = new C(õ) e -→ p
A summary of the syntax and the operational semantics of Objective Signal is given in appendix B

Static resolution of naming

The formalism upon which our object-oriented language is built is first-order: the object network's topology doesn't evolve during execution. Thus, it is possible to detect synchronization constraints between different system components statically. Hence, it is possible to detect and resolve inheritance statically. We introduce a compilation technique from a Objective Signal process p to a base Ists process JpK that preserves behavioral equivalence. The translation consists of globally applying the operators lookup and bind on p and of performing a substitution σ : (O × X ) → X in order to change instantiated paths into original signal Consider the process p : o = new C(õ) and suppose that p e -→ q. Rule (inst) applies and initiates the following proof sequence:

p e -→ q ⇔ lookup(C) = [ C].[p a ] ∧ bind o [o õ/self C] (p a ) e -→ q rule (inst) ⇔ lookup(C) = [ C].[p a ] ∧ r bind o [o õ/self C] (p a ) z eσ --→ JqK induction ⇔ lookup(C) = [ C].[p a ] ∧ r o = new [ C].[p a ](õ) z eσ --→ JqK translation scheme ⇔ Jo = new lookup(C)(õ)K eσ --→ JqK ⇔ Jo = new C(õ)K eσ --→ JqK translation scheme ⇔ JpK eσ --→ JqK definition of p
Consider the process (p | q) and suppose that (p | q) e -→ p . Rule (and) applies and provides the following proof sequence:

(p | q) e -→ p ⇔ p e 1 --→ p 1 ∧ q e 2 --→ p 2 ∧ e = e 1 ∪ e 2 ∧ p = (p 1 | p 2 ) ∧ ∀m ∈ fv(p) ∩ fv(q), (m ∈ dom e 1 ⇔ m ∈ dom e 2 ) ∧ (m ∈ dom e 1 ∩ dom e 2 ⇒ e 1 (m) = e 2 (m))
rule (and)

⇔ JpK e 1 σ ---→ Jp 1 K ∧ JqK e 2 σ ---→ Jp 2 K ∧ e = e 1 ∪ e 2 ∧ p = (p 1 | p 2 ) ∧ ∀m ∈ fv(p) ∩ fv(q), (m ∈ dom e 1 ⇔ m ∈ dom e 2 ) ∧ (m ∈ dom e 1 ∩ dom e 2 ⇒ e 1 (m) = e 2 (m))
induction According to the translation scheme,

Jp K = Jp 1 | p 2 K = Jp 1 K | Jp 2 K.
By application of σ, we have:

eσ = e 1 σ ∪ e 2 σ
Using the fact that fv(JpK) = fv(p)σ, and by application of the above induction hypothesis, we obtain that, for all x ∈ fv(JpK) ∩ fv(JqK),

(x ∈ dom e 1 σ ⇔ x ∈ dom e 2 σ)
and also

(x ∈ dom e 1 σ ∩ dom e 2 σ ⇒ e 1 σ(x) = e 2 σ(x))
Now, by definition of the rule (and), we obtain: This section aims at considering a real-world case-study that was pertinently suggested in [START_REF] Caillaud | A Semantics Backbone for UML Dynamic Diagrams Irisa[END_REF] to advocate the benefits of object-oriented synchronous approach to the design of distributed reactive systems in Uml. We use the Uml specifications from [START_REF] Caillaud | A Semantics Backbone for UML Dynamic Diagrams Irisa[END_REF] (figures 1, 3 and 2) to support our case study, showing the benefits of the notion of encapsulation and of the operator of behavioral inheritance provided by our synchronous model of computation.

(p | q) e -→ p ⇔ (JpK | JqK) eσ --→ Jp K rule (and) ⇔ (Jp | qK) eσ --→ Jp K translation scheme

Specification

The Plain Old Telephone Service

The Uml class diagram of figure 1 depicts a simplified telecommunication system comprising terminals, subscriber-line management and network: a so-called "plain old telephone service" (POTS). The Telephone class is characterized by id, the number of the current instance, and by peer, the number of the called instance. Its methods implement the basic use of a telephone by a user (offhook, onhook and dial) and by the network (call, hangup, established and progress). The state diagram of figure 3 describes the behavior of a telephone. The two main sub-states of the diagram describe the behavior of a telephone when it is activated by the network (state "called"), or by the user (state "calling"). In both cases, a new incoming call implies a hangup message to the caller. Also in both cases, the telephone is set back into its initial state ("idle") when the user hangs up (onhook). The state diagram of figure 2 describes the behavior of a basic network. An incoming message (call, hangup, established and progress) of a telephone identified by "u" is simply routed toward the corresponding telephone identified by "v".

unique unique unique unique call(u,v) / progress(u,v) / established(u,v) / hangup(u,v) / telephone[v].call(u) telephone[v].progress(u) telephone[v].established(u) telephone[v].hangup(u) Fig. 2.

Service adaptation: call forward on busy

Suppose that we wish to upgrade the POTS with a forwarding service ("call forward on busy"). It enables to forward an incoming call to a given number when the phone is busy instead of just returning a hangup message to the caller. Such a service adaptation implies the modification of Telephone and Network.

In the remainder of this section, we describe the expected modifications of the initial specification (depicted in figures 4, 5 and 6), and then we show how the inheritance operator achieves these modifications without breaking encapsulation.

There is a new attribute called fwd in Telephone. It contains the predefined number to which a call has to be forwarded when the user is busy. New methods forward in Telephone and Network implement the "call forward on busy" service. In Telephone, when the user dials a number, there is now a third state transition (toward "forwarded"). It corresponds to the answer forward(v, w) of the network. In this case the telephone dials itself the number w.

For that purpose, it uses the attribute selfdial (in state "forwarded") exactly as the parameter v of call(v) in state "dialing". The class Network is also modified to take into account a new incoming message forward. This message is a request from "u" for forwarding the caller "v" to "f". This request is routed by the network toward the corresponding telephone "v". The figures 4, 5 and 6 show these modifications. In figure 5, the highlighted parts in gray point out the modifications. Two hangup messages have been preserved (boxed labels) when the user hangs up (onhook).

Synchronous adaptation

We obviously wish to achieve the service adaptation without breaking encapsulation, i.e. without rewriting Network and Telephone. We investigate the synchronous adaptation of Telephone using the inheritance mechanism shown in the previous section. First, we briefly describe the translation of a Statechart to an encapsulated Objective Signal process.

Statecharts encoding

For more readability, we do not take into account the "AND" super-states. Thus, a reaction of the system corresponds to a unique transition within the global Statechart. The behavior specified by a Statechart can then be described in Objective Signal by a choice between several transitions. last state=(pre i) self.state Activated states For each state a (base state or not), we introduce a signal from a that is synchronous with state. It indicates whether a is activated (or contains an activated substate) just before a transition. In the case of a basic state, we just have to check last state. In the case of a super-state, we use a logical "OR" between the sub-states: Historic The transition to the special (history) state H is encoded by a signal h a that is synchronous with state, for each state a. If a is activated, then h a is updated by last state. Otherwise, the previous value of h a is kept unchanged thanks by using a delayed version zh a of h a.

Current state

Labels of transitions

The labels of the transitions correspond to synchronous constraints (signal calls) and to definitions of local signals.

Jc/c K = Jc; c K = JcK | Jc K
The definition of a variable is encoded by the definition of a local signal, and the call of a method encoded by the definition of its parameters. The translation of guards is straightforward.

Jx := f (ỹ)K = (x=f ỹ) Jm(ỹ)K = (ỹ=m) J[ condition ]K = (when condition)

Call forward on busy

We focus on the translation of Telephone and its upgrade via inheritance. Assume that p tel is the abstract behavior of the Telephone built using the translation scheme previously presented. Then, the class Telephone has the following interface:

Telephone def = [user, net].[p tel ]
The parameters user and net stand for the instance of User and Network required by the class diagram of figure 1.

Now, let us define the wrapper CallForward of Telephone to implement service adaptation without breaking encapsulation. We need to introduce the new state "forwarded". Thus, the signal state needs to be overridden. As in the example of the balance, the signal last state now maintains a delayed version of the new version of state. The wrapper is a choice between the initial behavior and the new transitions to and from the state "forwarded". In the following definition of CallForward, we only make the transition from "dialing" to "forwarded" explicit. The other transitions have a similar encoding:

CallForward def = [user, net].[].                               + . . .                         
This wrapper overrides the signal state. The first branch of the choice allows to reuse the previous behavior of Telephone, only when the signals introduced in the other choices of the wrapper, namely forward, are absent. When forward is present, the new definition of state prevails (preemption). In this case, the last state must be "dialing" and the new state is "forwarded". The interface of CallForward holds the parameters user and net, which correspond to the same parameters as in the Telephone. Finally, the modification of Telephone by CallForward is simply achieved as follows:

NewTelephone def = Telephone&CallForward 5 Conclusion
There has been a lot of work aiming at combining object orientation and concurrency, especially within the framework of practical object-oriented languages like Eiffel [START_REF] Meyer | Systematic Concurrent Object-Oriented Programming ISE[END_REF][START_REF] Atkinson | Object-Oriented Reuse, Concurrency and Distribution[END_REF]. However, our work aims at combining the notions of encapsulation and of inheritance found in objectoriented programming to a concurrency model that supports formal methods for modeling, verification and valid code generation purposes. To this end, many different approaches have already been considered for introducing object-oriented concepts in algebraic models of concurrency . In [START_REF] Pierce | Concurrent Objects in a Process Calculus In Proceedings Theory and Practice of Parallel Programming[END_REF], Pierce and Turner introduce a simple object-based programming style in Pict, an implementation of the π-calculus. In Pict, objects are units of concurrency composed of several communicating agents. Objects in Pict aim at structuring a system, like modules (yet without functors). They encompass mobility but do not implement inheritance or overriding. A type-based notion of behavioral refinement of processes in Pict is obtained by superimposing a type inference system with subtyping to the process calculus. In [START_REF] Fournet | Inheritance in the Join Calculus[END_REF], Fournet et al. propose an object-oriented extension of the join-calculus. A class-based inheritance mechanism is introduced that avoids the inheritance anomaly. In [START_REF] Boussinot | Two Semantics for a Language of Reactive Objects Research report n[END_REF][START_REF] Boussinot | Reactive Objects Research report n[END_REF], Boussinot and Laneve introduce an object-based reactive language. A notion of global instants is introduced. The same method cannot be executed more than once in the same instant. It is possible to clone an object, to add a method to an object and to rename a method. These operations implement a "derivation" mechanism rather than a "behavioral inheritance" mechanism stricto senso. For instance, if a modified object uses a currently overridden method, it still uses the previous version of this method.

In conclusion, we have introduced a new paradigm to express the essence of encapsulation and inheritance in a synchronous concurrent modeling framework. We introduced Ists and Objective Signal, an extended version of Ists build upon this paradigm. Reusability of components is achieved by an encapsulation mechanism. A static interpretation of inheritance allows a natural formulation of behavior refinement where overriding is taken into account.

The proposed model supports a compile-time resolution of inheritance: overriding is interpreted statically and the inheritance combinator is translated into a primitive synchronous constructs. The benefits of our approach are illustrated by the adaptation of services to a plain old telephone service specification.

A Implicit synchronous transition systems

A.

  answer d y : asynchronous answer c mem : y() : aux := mem; mem := x(); return aux; environment In a synchronous approach of concurrency, computation and communication take no time. From an external point of view, a process p of Objective Signal is characterized by the signals it defines. The state of p corresponds to the initial values c of delay equations (y=(pre c) x) occurring in p. The state of the object is modified iff a signal defined by such an equation is present.

  environment object object x carries d y carries c at the same time (y = (pre c) x) ( y = (pre c) x) environment call of y, when it is present x : synchronous answer d y : synchronous answer c synchronous call of x

Example 3

 3 Processes p in Objective Signal are encapsulated within classes C. A class gives the generic definition of an object that can be instantiated by providing its initial state. In the definition of a class, a defined signal x (i.e. which appears on the left hand-side of an equation) is provided by the class. A signal y, which appears on the right hand-side of an equation, is a signal call or signal fetch. The class which provides this signal is identified by a parameter C ∈ M. Thus, signal calls are prefixed by class parameters: C.y.A class definition is parameterized by all the classes it uses. Among them, a special class parameter self refers to the current instance of the class. The class C balance is an encapsulation of the process balance. The initial definition is encapsulated within a structure which specifies its interface: [C] is the class parameter which provides the signal x used by the balance. The special parameter self refers to the class C balance itself (which provides the signals n and m). The scope of m is restricted to the definition of the class. m is a private signal.(pre 0) self.n)    (when C.x) | (n=self.m+1) + (when (not C.x)) | (n=self.m-1)The class C balance can only be instantiated if it is given an effective parameter that provides the signal x. Objects are identified by names o ∈ O and are created by the construct o = new C(õ) where C is a class (e.g. C balance ) and o the name of the instance. Thus, o corresponds to the parameter self. The sequence õ provides the effective parameters required by C (e.g. C). Objects o, o in Objective Signal behave like processes in Ists. They are combined using synchronous composition o | o and choice o+o . For instance, the following object is composed of two sub-objects. The first one (named balance) is an instance of the class C balance . Its creation requires an object env which provides the signal x. balance and env are connected by synchronous composition.C env def = [].[1+(x=tt)+(x=ff )] balance = new C balance (env) | env = new C env ()3.2.2 Formal syntaxWe formally introduce the encapsulated Objective Signal. There are two grammars in this extended formalism. The first rule correspond to Ists processes p where instantiated behaviors can be specified. The second rule C corresponds to class definitions where abstracted behaviors can be specified.The first rule extends the grammar of Ists with the class instantiation statement o = new C(õ) presented in the previous example. As the target of a signal call x is an object o, signal names x ∈ X now appear as instantiated paths o.x ∈ (O × X ).p, q ::=p | q | p+q | p/m | m=f m | m=(prec)m | o = new C(õ) (instantiated process) m ::= o.x (instantiated path) o ∈ O (object name)Classes C consist of an interface where class parameters are declared, and an abstract behavior p a is defined (for "abstract p"). In these abstract behaviors, signal names x ∈ X on the right hand-side of equations are replaced by abstract paths C.x ∈ (M × X ). An abstract path C.x denotes the call to a signal x of the class parameter C. The path self.x refers to the signal x of the current class. A signal name x appearing on the left hand-side of an equation is a defined signal. It implicitly refers to the abstract path self.x. C ::= [ C].[p a ] (class) p a , q a ::= p a | q a | p a +q a | p a /x | ỹ=f ñ | y=(prec)n (abstract process) n ::= C.x (abstract path) C ∈ M self (class parameter) The notations for the free and defined signals of processes (fv(p) and dv(p)) are extended to objects and classes in order to take paths p a into account. In the remainder, we exclusively consider classes that are well-formed, i.e. classes [ C].[p a ] such that C.x ∈ fv(p a ) ⇒ C ∈ C. Notice that, in the grammar p, some non-instantiated classes may coexist with instantiated ones. When a reaction containing an object declaration o = new C(õ) is triggered, a new instance of C (i.e. a process that corresponds to the definition p a ) is created. Names and paths of the original definition are substituted by the effective parameters õ and o . In the following example, abstract paths are substituted by instantiated paths.

  Finally, the parameters C and C are unified in the global structure under the name C. The signals x and r are now provided by the same class C.

Fig. 1 .

 1 Fig. 1. Class diagram of the POTS 4 Case study: the Plain Old Telephone Service

Fig. 3 .

 3 Fig. 3. State diagram of class Telephone

Fig. 4 .

 4 Fig. 4. Class diagram of the modified POTS

Fig. 5 .Fig. 6 .

 56 Fig. 5. State diagram of the modified class Telephone

  = (self.last state = a) from a = (self.from b ∨ self.from c) Initial states For each state a, we introduce a signal init a that is synchronous with state. It carries the name of the starting sub-states: a init a = self.init b

  a=(pre a) self.h a)    (h a=self.last state) | (when self.from a) + (h a=self.zh a) | (when(not self.from a)) Transitions A transition labeled by c from a to b corresponds to an update of state. If the target of the transition is the history state H, the new state is h b. This transition is guarded by JcK, the encoding of the label c.

  self.from a) | JcK | (state = self.init b) a c H (when self.from a) | JcK | (state = self.h b)

Syntax A. 1 . 1 A. 2 A[

 112 Kernelp, q ::= ỹ=f x (equation) | y=(pre c)x (transition)| p | q (composition) | p+q (choice) | p/x (restriction) c, d ∈ C = B + Z (constant) f, g ∈ F (function) x, y ∈ X (signal) (x 1 , . . . , x k ) ∈ X k (sequence) x ∈ X * = k∈N X k A.1.2 Derived processes Algebraic laws fv(ỹ = f x) = ỹ ∪ x dv(ỹ = f x) = ỹ fv(p+q) = fv(p | q) = fv(p) ∪ fv(q) dv(p+q) = dv(p | q) = dv(p) ∪ dv(q) fv(p/x) = fv(p) \ {x} dv(p/x) = dv(p) \ {x} p/y≡(p[x/y])/x ( * ) p/x/y≡p/y/x p | q/x≡(p | q)/x ( * ) p | (q | r)≡(p | q) |r p+(q+r)≡(p+q)+r p+q/x≡(p+q)/x ( * ) p+q≡q+p p | q≡q | p p | 1≡p+p ≡ p p/x≡p ( * ) A.3 Operationnal semantics A.3.1 Environment and predefined functions e, f ∈ E = X C * (environment)δ : F (C * C * ) (predefined functions) ∀f ∈ dom δ, ∃k, k s.t. δ(f ) : C k C k δ(+) = {((c,c ) → (d)) | (c,c ,d) ∈ Z 3 ∧ d = c+c } δ(id) = {((c) → (c))|c ∈ C} δ(=) = {((c,c) → (tt))|c ∈ C} ∪ {((c,c ) → (ff ))|c = c } δ(event) = {((c) → ()) | c ∈ C} δ(when) = {((tt) → ())} δ(true) = {(() → (tt))} δ(false) = {(() → (ff ))} δ(1) = {(() → ())} -→ p | q iff ∀x ∈ fv(p) ∩ fv(q), dom e ⇔ x ∈ dom f ) ∧ (x ∈ dom e ∩ dom f ⇒ e(x) = f (x)) (com) (ỹ=f x) e -→(ỹ=f x) iff dome = x ∪ ỹ ∧ δ(f )(e(x)) = e(ỹ) (pre) (y=(pre c)x) x → d, y → c ---------→(y=(pre d)x) A.3.3 Axioms derived from (com) (z=x+y) x → c, y → d z → c+d ----------→(z=x+y) 1 ∅ ---→ 1 x=tt x → tt ----→ x=tt x=ff x → ff -----→ x=ff when x x → tt ----→ when x event x x → c ----→ event x B Objective Signal B.1 Syntax p, q ::= p | q | p+q | p/m | m=f m | m=(prec)m | o = new C(õ) (instanciated process) m ::= o.x (instanciated path) o ∈ O (object name) C ::= [ Cr ].[ C].[p a ] | C&C (class) p a , q a ::= p a | q a | p a +q a | p a /x | ỹ=f ñ | y=(prec)n (abstract process) n ::= C.x (abstract path) C ∈ M ⊃ {super, self} (class parameter) B.2 Operationnal semantics B.2.1 Renaming operators bind o σ (p a | q a ) = bind o σ (p a ) | bind o σ (q a ) bind o σ (p a +q a ) = bind o σ (p a )+bind o σ (q a ) bind o σ (p a /x) = (bind o σ (p a ))/o.x bind o σ (ỹ=f ñ) = (o.ỹ=f (ñσ)) β paqa = dv(p a ) ∩ dv(q a ) ∀x ∈ dom β paqa , xβ paqa = x / ∈ dv(p a ) ∪ dv(q a ) 34 L β ( p a | q a ) = L β (p a ) | L β (q a ) L β ( p a +q a ) = L β (p a )+L β (q a ) L β (p a /x) = L βx (p a ) /x L β (ỹ=f ñ) = (ỹβ)=f ñ lookup  Cr1 ] . [ C1 ] . [p a ] & [ Cr2 ] . [ C2 ] . [q a ] L βp aqa (p a ) | q a [ Cr1 C1 / Cr2 ][self.(xβ paqa )/super.x]   /im β paqa   lookup(C&C ) = lookup ( lookup(C)&lookup(C ) ) lookup(C) = C (with C: base class) B.2.2 Rule for class instanciation (inst) lookup(C) = [ C].[p a ] bind o [o õ/self C] (p a ) e -→ p o = new C(õ) e -→ p B.3 From Objective Signal to Ists Jo = new C(õ)K = Jo = new lookup(C)(õ)K r o = new [ C].[p a ](õ) z = r bind o [o õ/self C] (p a ) z J m = f m K = ( mσ = f m σ) Jp | qK = JpK | JqK Jp+qK = JpK + JqK Jp/mK = JpK /(mσ)

  We now complete the definition of Objective Signal with an inheritance operator over classes. Using the notion of wrapper class, this construct allows to synchronously add new signals to a class and to refine or adapt existing ones, compositionally. When a signal defined in the wrapper is also defined in the class it is applied to, the new definition prevails. Still, it is possible to refer to the initial one thanks to the super-class: the parameter super.

It simply applies the renaming mechanism on the definition p a of a class. The name o of the created object is substituted to the parameter self. The effective parameters õ are substituted to the class parameters C. (inst) bind o [o õ/self C] (p a ) e -→ p o = new [ C].[p a ](õ) e -→ p 3.3 Inheritance 3.3.1 Overview of Objective Signal Example 4 We wish to modify the class C balance in order to incorporate a reset signal r (provided by the class that defines x). The signal r can be invoked only if x is present. It is used to reset the balance to 0. The state of C balance is managed by a private signal m. Implementing this upgrade without inheritance would break encapsulation. Using inheritance, it amounts to adding a wrapper (on the right hand-side) to the initial class as follows:

  State diagram of class Network

			call(u) / peer := u;
			user.ring(); network.progress(id,peer)	called
		idle	user.stopring() hangup(u) [u=peer] /	ringing
	offhook()		onhook() /	offhook() /
	/		network.hangup(id,peer)	network.established(id,peer)	call(u) /
	user.dialtone()			established	H	network.hangup(id,u)
			onhook()	hangup(u) [u=peer] /
				user.busytone()
		onhook() /
	onhook() /	network.hangup(id,peer)	hangup
	calling	dial(v) / network.call(id,v); hangup(v); user.busytone()	H	network.hangup(id,u) call(u) /
		not_busy
	dialing		established(u)	busy
	dial(v) /		[u=peer] /		hangup(u) [u=peer] /
	peer := v;		user.stopaudiblering()	user.busytone()
	network.call(id,v)		progress	established
	progress(v)
	user.audiblering()

  The signals state and last state carry the name of the current state and the name of the last state. The clock of these synchronized signals defines the rate of the whole process. We only consider the name of the current activated basic states (e.g. "progress") and not the nesting super states (e.g. "not busy" or "calling"). This is allowed since only one basic state can be activated at a time (in the absence of "AND" super-states). Thus, state is present at each transition, and last state is defined as follows (i stands for the initial

		call(u) / peer := u;
		user.ring();
		network.progress(id,peer)
		hangup(u) [u=peer] /	ringing
		user.stopring()
	offhook()	onhook() /	offhook() /
	/	network.hangup(id,peer)	network.established(id,peer)
	user.dialtone()		established	H
			hangup(u) [u=peer] /
			user.busytone()
	onhook() /
	network.hangup(id,peer)	hangup
	dial(v) /
	peer := v;
	network.call(id,v)
	progress(v)
	user.audiblering()

We implemented a prototype compiler from Objective Signal to Signal based on the translation schemes from Objective Signal to Ists (presented in this paper) and from Ists to Signal (presented in [14]). The use of enhanced features of Signal (like modules to implement encapsulation), and the direct production of executable code from an executable Ists specification are promising prospects.

As the same syntactic operators are used, we naturally obtain the following result:

Proof sketch The proof, detailed in [START_REF] Kerboeuf | Orientation objet d'un calcul de processus synchrones[END_REF], is by induction on the structure of synchronous systems. The rules of the Ists and its object-oriented version are quite similar, modulo renaming by σ.

Let us consider the base case p : m = f m and suppose that p e -→ q. Rule (com) applies and requires q to have the form m = f m and e be such that dom e = m ∪ m and δ(f )(e( m )) = e( m). Let σ : (O × X ) → X be the substitution specified by the translation scheme. We have that:

Using this substitution on instanciated paths, we obtain:

where dom eσ = mσ ∪ m σ ⊂ X . According to the translation scheme, we have: JpK eσ --→ JqK.

The case of the base process (m = (pre c) m ) is similar. In cases where processes are composed of several (structurally) simpler processes, we just need to invoke an induction hypothesis. We detail such induction steps for the case analysis of the synchronous composition (p | q) and of the class instanciation (o = new C(õ))