Jean-Pierre Talpin

David Berner

Sandeep Kumar Shukla

Paul Le Guernic

Abdoulaye Gamatié

Rajesh K Gupta

A Behavioral Type Inference System for Compositional System-on-Chip Design

come

Introduction

The design productivity gap has been recognized by the semiconductor industry as one of the major threats to the continued growth of complex system-chips and their applications. System level design methodology that moves from RTL-based design entry into design methods at higher-level of abstraction is essential to manage design complexity. A number of advances in high-level modeling and validation have been proposed over the past decade in an attempt to improve the level of abstraction in system design, most of these enable greater reuse of existing intellectual property (IP) blocks. Design correctness is an important part of this move. Given the complexity of system-level designs, it is important that the composition of system-level IP blocks be guaranteed correct. However, a posteriori validation of component compositions is a difficult problem. Techniques are needed that ensure design correctness as a part of the design process itself. To address this issue, methodological precepts have been developed that separately focus on design reuse and correctness by construction. Both reuse and elevation of abstraction at design entry critically depend on guaranteed design correctness.

To improve the state of the art in component composition from existing IP libraries, we specifically seek to address the following issue: given a high level architectural description (e.g., a "virtual" architecture) and a library of implemented components, how can one automate the selection of implementation of virtual components from the library, and automatically ensure composability of data and behavior? Our approach is based on a high-level modeling and specification methodology that ensures compositional correctness through a type theory capturing behavioral aspects of component interfaces. The proposed system builds upon previous work on scalable design exploration using refinement/abstraction-based design methodologies [START_REF] Talpin | Polychrony for formal refinement-checking in a system-level design methodology[END_REF], implemented in the Polychrony workbench, and on a layered Component Composition Environment, Balboa [START_REF] Doucet | Typing abstractions and management in a component framework[END_REF], which allows specification of SystemC components with mixed levels of structural and behavioral details and high degree of concurrency and timing requirements. Our behavioral type system consists of a minimalist formalism, called the iSTS (implicit synchronous transition systems), akin to a subset of Pnueli's synchronous transition systems [START_REF] Pnueli | Fair synchronous transition systems and their liveness proofs[END_REF]. It is used as a type system to describe the behavior of system components and allow for global model transformations to be performed on the system based on behavioral type information. In [START_REF] Talpin | Behavioral type inference for compositional system design[END_REF], it is equipped with a formal semantics defined in polychronous model of computation [START_REF] Le Guernic | Polychrony for system design[END_REF] and implemented by the Polychrony workbench (available from http : //www.irisa.fr/espresso/Polychrony).

Rationale

To allow for an easy grasp on the proposed behavioral type inference technique, we outline the analysis of a Sys-temC program (Figure 1 of its behavioral type (Figure 1, middle) and the inference of its static abstraction (Figure 1, right). Then we elaborate the notion of proof obligations synthesis by giving a brief outline of the design correctness issues which can be modeled and checked in the framework of our type system. Static single assignment. Figure 1, left, depicts a simple C code fragment consisting of an iterative program that counts the number of bits set to one in the variable idata. While idata is not equal to zero, it adds its right-most bit to an output count variable ocount and shifts it right in order to process the next bit. In the static single-assignment (SSA) representation of the program (Figure 1, second column) all variables (idata and ocount) are read and written once per cycle. Label L2 is the entry point of the SSA block associated with the while loop. The first instruction loads the input variable idata into the register T1. The second instruction stores the result of its comparison with 0 in the register T0. If T0 is false, control is passed to block L3. Otherwise, the next instruction is executed: the variable ocount is loaded into T2, the last bit of T1 is loaded into T3, the sum of T2 and T3 assigned to ocount and the right-shift of T1 assigned to idata. The block terminates with an unconditional branch back to label L2.

Behavioral types.

The SSA intermediate representation of an imperative program represents an otherwise arbitrarily obfuscating C program in a form that can be easily manipulated by an automatic program analyzer. Let us zoom on the block L2 in the example of Figure 1. The behavioral type of the block L2, middle, consists of the simultaneous composition of logical propositions (middle) that form a synchronous transition system. Each proposition is associated with one instruction: it specifies its invariants. In particular, it tells when the instruction is executed, what it computes, when it passes control to the next statement, when it branches to another block.

On line 1 for instance, we associate the instruction T1 := idata to the proposition x L2 ⇒ T1 := idata. In this proposition, the variable x L2 is a boolean that is true iff the block of label L2 is being executed. Hence, the proposition says that, if the label L2 is being executed, then T1 is equal to idata. Otherwise, another proposition may hold. In the present case, all propositions are conditioned by x L2 to mean that they hold when block L2 is being executed.

The extent of a proposition is the duration of a reaction. A reaction can be an arbitrarily long period of time provided that it is finite and that every variable or register changes its value at most once during that period. For instance, consider the instruction if T0 then L3. It is likely that label L3 will, just as L2, perform some operation on the input idata. Therefore, its execution is delayed until after the current reaction. We refer to x L3 as the next value of the state variable x L3 , to indicate that it will be active during the next reaction. Hence, the proposition x L2 ⇒ T0 ⇒ x L3 says that control will be passed to L3 at the next reaction when control is presently at L2 and when T0 is true. The instructions that follow this test are conditioned by the negative ¬T0, this means: "in the block L2 and not in its branch to L3".

Static abstraction.

We have seen that every instruction of an SSA program could be associated with a proposition to render its control-flow and data-flow behaviors. This representation provides a formal and expressive way to model, analyze, optimize and verify the behavior of ordinary Sys-temC programs. To ease both optimization and verification of such programs based on that representation, we abstract it over its control flow, characterized by boolean relations between clocks, and its data flow, characterized by scheduling relations between signals. Let us first define some terminology. A clock x is associated with a signal x.

The signal x corresponds to the flow of the successive values of a variable, sampled by the discrete periods of time that we call reactions. The clock of x denotes that set of periods or instants. On Figure 1, right, all operations on integers reported in the behavioral type are abstracted by boolean relations between clocks and by scheduling relations. This is in fact sufficient information to reconstruct the entire control and data flow graphs of the program. All information abstracted from this view essentially consists of computational instructions with which we could decorate this graph to regenerate the original program.

For instance, the instruction T0 = (T1! = 0) is abstracted by the type x L2 ⇒ T1 = T0 . It means: "when the block L2 is executed, T0 is present iff T1 is present". The scheduling constraint x L2 ⇒ T0 → x L3 additionally says that "x L3 cannot happen before T0 at L2". Indeed, one first needs to examine the status of T0 before to branch to L3. The type associated with the block L2 uses the clocks denoted by the booleans x L2 , T0 and ¬T0. Each clock denotes a branch in the control-flow graph of the block L2. The other clocks, e.g. T1, denote the presence of data. They are partially related to the "label" clocks x L2 , T0 and ¬T0. Typed modules. Section 5 develops the use of the information provided by the behavioral type inference system to perform design correctness checks. The most salient feature of the behavioral type system is yet the capability to reduce compositional design correctness verification to the validation of synthesized proof obligations. It is presented in the context of the inference system proposed for the SystemC module system, Section 4.

As an example, consider a class whose virtual fields are two clocks x and y, and a procedure f . It defines an interface, named m 0 , and will be used to type another class. Next, assume an explicit behavioral type declaration #TYPE(f, Q) which associates f with a description of its behavior: the proposition Q (a denotation of all possible implementations satisfying an expected functionality).

class m 0 { virtual sc clock x, y; virtual void f () {} #TYPE(f, Q) }; template class m 1 #TYPE(m 1 , m 0 ) SC MODULE(m 2 ) { SC CTOR(m 2 ) { SC THREAD(m 1 .f ) sensitive x } }; class m 3 { sc clock x, y; void f () { pgm} #TYPE(f, P ) }; m 2 m 3 m 4 ;
Next, we associate the interface m 0 with the class parameter m 1 of a template class m 2 . The interface m 0 now gives a behavioral type to the method f in the class parameter m 1 expected by the module m 2 . Indeed, the template class m 2 uses the class parameter m 1 , that implements m 0 , to launch a thread m 1 .f sensitive to x. The behavioral type Q, which gives an assumption on the behavior of m 1 .f , is required to provide a guarantee on the behavior of the module m 2 , produced by the template class.

Proof obligations. Let m 3 be a candidate parameter for the template class m 2 . It structurally implements the interface m 0 , because it provides the clocks x and y and defines the method f by the program pgm. Using the type inference technique previously outlined, the program pgm is associated with a proposition P that describes its behavioral type, and the class m 3 be decorated with the corresponding type declaration #TYPE(f, P ). Finally, let m 4 be the class defined by the instantiation of the template m 2 with the actual parameter m 3 . To check the compatibility of the actual parameter m 3 with the formal parameter m 0 , we need to establish the containment of the behaviors denoted by the proposition P (the behavioral type of the actual parameter) in the denotation of the proposition Q, the type abstraction declared in m 0 . This amounts to check that P implies Q. This proof obligation can either be implemented using model checking (if P and Q are dynamic interfaces) or using SAT checking, if Q is a static interface, by calculating the static abstraction P of P and by verifying that P implies Q.

A polychronous type system

We now give an informal outline of the type system that will support and materialize the polychronous model of computation and type, and sign the behavior of SystemC programs and classes. The key principles put to work in this notation are essentially borrowed to Pnueli's STS [START_REF] Pnueli | Fair synchronous transition systems and their liveness proofs[END_REF] and its syntax to Dijkstra's guarded command language, we call isthe iSTS (i for implicit). In the iSTS, a process consists of simultaneous propositions that manipulate signals. A signal is an infinite flow of values that is sampled by a discrete series of instants or reactions. An event corresponds to the value carried by a signal during a particular reaction.

An example. The system of equations below puts together the main features of the behavioral type system. It describes the behavior of a counter modulo 2, noted P (= def means "is defined by"), through a set of simultaneous propositions, labeled from (1) to (3).

P def = ¬s 0 (1) | | x ⇒ s = ¬s (2) | | s ⇒ ŷ (3)
Proposition (1) is an invariant. It says that the initial value of the signal s, denoted by s 0 , is false. This is specified by the proposition ¬s 0 (or s 0 = 0). Proposition (2) is a guarded command. It says that if the signal x is present during a given reaction then the value of s is toggled. The left-most part of the sentence, the proposition x, is a condition or a guard. It denotes the clock of x. It is true if the signal x is present during the current reaction. The rightmost part of the sentence, the proposition s = ¬s, is a transition. The term s refers to the next value of the signal s.

The proposition s = ¬s says that the next value of s is the negation of the present value of s. Proposition (3) is another guarded command. It says that if s is true then y is present. Notice that, in proposition (3), the guard expects the signal s to hold the value 1 but that its action does not actually specify the value of the signal y: it simply requires it to be present. Proposition (3) is hence an abstraction: a proposition that partially describes the properties of the system under consideration without implying a particular implementation. To implement a function or a system, this proposition needs to be compositionally refined by another one, saying what value y should hold at all time (i.e. when present). To | y 0 = 0 . Notice that the iteration specified by the proposition Q is not guarded. This means that it is an invariant that describes the successive values of the signal y in time but not the particular time samples at which the signal y should occur. The composition of Q with P has the effect of synchronizing the signal y in Q to the clock s in P : to the time samples during which the signal s holds the value true. This composition is called a refinement: the system obeys the specification denoted by the initial proposition P and is constrained to further satisfy the additional conditions implied by Q.

The notation introduced so far holds necessary and sufficient ingredients to specify the behavior of multi-clocked synchronous systems. Pnueli's original STS notation features two additional notions essentially geared towards verification by model-checking: one is choice P ∨ Q, the other explicit absence ⊥. Both can be modeled in the iSTS. An order of execution can be imposed to a proposition by its refinement with a scheduling constraint, noted y → x. Then, x = y is an abstraction of x = y | | y → x where y → x informally means that "x cannot happen before y". In doing so, we refine the time scale, from one in which x and y happen simultaneously, to a more precise one in which one observes that x cannot happen before y. In the remainder, we adopt the syntax x := y borrowed to Signal for an assignment of y to x:

(x = y | | y → x).
Formal syntax of the type system. The formal syntax of propositions in the behavioral type system is defined by the inductive grammar P . A propositon or process P manipulates boolean values noted v ∈ {0, 1} and signals noted

x, y, z. A location l refers to the initial value x 0 , the present value x and the next value x of a signal. A reference r is either a value v or a signal x.

(reference)

r::=x | v (location) l ::= x 0 | x | x (clock) e, f ::=0 | x = r | e ∧ f | e ∨ f | e \ f | 1 (process) P, Q::=1 | l = r | x → l | e ⇒ P | (P | | Q) | P/x
A clock expression e is a proposition on boolean values that, when true, defines a particular period in time. The clocks 0 and 1 denote events that never/always happen. The clock x = r denotes the proposition: "x is present and holds the value r". Particular instances are: the clock x= def (x = x), which stands for "x is present"; the clock x= def (x = 1) for "x is true", and the clock ¬x= def (x = 0) for "x is false".

Clocks are propositions combined using the logical combinators of conjunction e∧f , to mean that both e and f hold, disjunction e ∨ f , to mean that either e or f holds, and symmetric difference e \ f , to mean that e holds and not f . A process P consists of the simultaneous composition of elementary propositions. 1 is the process that does nothing. The proposition l = r means that "l holds the value r". The proposition x → l means that "l cannot happen before x".

The process e ⇒ P is a guarded command. It means: "if e is present then P holds". Processes are combined using synchronous composition P | | Q to denote the simultaneity of the propositions P and Q. Restricting a signal name x to the lexical scope of a process P is written P/x.

Behavioral types for SystemC modules

We are now equipped with the required mathematical framework and formal methodology to address the modeling of GALS architectures described using SystemC. This model is described in terms of a type inference system and extended to the structuring elements of SystemC in terms of a module system. This framework allows to give a behavioral signature of the component of the system, compositionally check the correct composition of such components to form architecture, to optimize the described software elements from the imposed hardware elements by, first, detaching the formal model from the functional architecture description and, second, using the model to regenerate an optimized software matching the requirements of the execution architecture. As a by-product, the association of types with SystemC programs provides a formal denotational semantics implied by the interpretation of types in the polychronous model of computation.

Formal syntax of SystemC core. We start with the definition of the core of the SystemC syntax relevant to the present study. A system consists of the composition of classes and modules sys, Declarations dec associate locations x with native classes or template class instances m m * and procedures with a name f and a definition pgm. For instance, int x defines an integer variable x while sc signal bool x defines a boolean signal x. We assume x to denote the name of a variable or signal and to be possibly prefixed as m :: x by the name of the class it belongs to. We assume the relation ≤ to denote C++ sub-typing (e.g., bool ≤ num, int ≤ num).

The formal grammar of SystemC programs, Figure 2, is represented in static single-assignment intermediate form akin to that of the Tree-SSA package of the GCC project [START_REF] Novillo | Tree SSA, a new optimization infrastructure for GCC[END_REF]. SSA provides a language-independent, locally optimized intermediate representation (Tree-SSA currently accepts C, C++, Fortran 95, and Java inputs) in which languagespecific syntactic sugar is absent. SSA transforms a given programming unit (a function, a method or a thread) into a structure in which all variables are read and written once and all native operations are represented by 3address instructions x = f (y, z). A program pgm consists of a sequence of labeled blocks L:blk . Each block consists of a label L and of a sequence of statements stm terminated by a return statement rtn. In the remainder, a block always starts with a label and finishes with a return statement: stm 1 ; L:stm 2 is rewritten as stm 1 ; goto L; L:stm 2 . A wait is always placed at the beginning of a block: stm 1 ; wait v; stm 2 is rewritten as stm 1 ; goto L; L:wait v; stm 2 . Block instructions consist of native method invocations x = f (x * ), lock monitoring and branches if x then L. Blocks are returned from by either a goto L, a return or an exception throw x. The declaration catch x from L 1 to L 2 using L 3 that matches an exception x raised at block L 1 activates the exception handler L 3 and continues at block L 2 .

Example 1

To outline the construction of the intermediate representation of a SystemC program, let us reconsider the example of Section 2 and detail the method that counts the number of bits set to 1 in a bit-array epc.data (Figure 3). The method consists of three blocks. The block labeled L1 waits for the lock epc.lock before initializing the local state variable idata to the value of the input signal epc.data and ocount to 0. Label L2 corresponds to a loop that shifts idata right to add its right-most bit to ocount until termination (condition T0). In the block L3, ocount is sent to the signal epc.count and epc.lock is unlocked before going back to L1. 4, is defined by induction on the formal syntax of pgm. To define it, we assume that the finite set L f of program labels L defined in a given method f respects the order of appearance in the text: Example 2 Let us zoom on the block L2 of the ones counter (Figure 3). On the first line, for instance, we associate the instruction T1 = idata of block label L2 to the proposition x L2 ⇒ T1 = idata. In this proposition, the new variable x L2 is a boolean that is true iff the label L2 is being executed. So, the proposition says that, if the label L2 is being executed, then T1 is always equal to idata. If not, then another proposition may hold. In our case, all subsequent propositions are conditioned by x L2 meaning that they hold when L2 is being executed. Next, consider the instruction if T0 then L3. It is likely that label L3 will, just as L2, perform some operation on the input idata. Therefore, we delay its execution until after the current reaction and refer to x L3 as the next value of the state variable x L3 , to indicate that it

Behavioral type inference. The type inference function

I[[pgm]], Figure
L 1 < L 2 means that L 1 occurs before L 2 . To each block of label L ∈ L f , the function I[[pgm]] associates an input clock x L , an immediate clock x imm
(1) I[[L:blk ; pgm]] =I[[blk ]] xL∨x imm L L | | I[[pgm]] (2) I[[stm; blk ]] e L =let P e1 = I[[stm]] e L in P | | I[[blk ]] e1 L (3) I[[if x then L 1 ]] e L = G L (L 1 , e ∧ x) e∧¬x (4) I[[x = f (y * )]] e L = E(f )(xy * e) e (
L = e ∧ (x = x ) ⇒ ŷ | | e \ ŷ ⇒ x L ŷ (7) I[[goto L 1 ]] e L =(e ⇒ x exit L | | G L (L 1 , e)) (8) I[[return]] e L =(e ⇒ (x exit L | | x exit f )) (9) I[[throw x]] e L =(e ⇒ (x exit L | | x)) where G L (L 1 , e) = if S L (L 1 ) then e ⇒ x imm
L1 else e ⇒ x L1 and E(f

)(xyze) = e ⇒ (ŷ ∧ ẑ ⇒ (x | | y → x | | z → x)) I[[catch x from L to L 1 using L 2 ]] e L = G L (L 2 , x ∧ x exit L ) | | G L2 (L 1 , x exit L2 )
Figure 4. Type inference will be active during the next reaction. Hence, the proposition x L2 ⇒ T0 ⇒ x L3 says that control passes to L3 at the next reaction when control is presently at L2 and when T0 is true. The instructions that follow this test are conditioned by the negative ¬T0, this means: "in the block L2 and not in its branch to L3".

Figure 4 defines the behavioral type inference system. Rules (1-2) are concerned with the iterative decomposition of a program pgm into blocks blk and with the decomposition of a block into stm and rtn instructions. In rule (2), the input clock e of the block stm; blk is passed to stm. The output clock e 1 of stm becomes the input clock of blk .

The input and output clocks of an instruction may differ. This is the case, rule (3), for an if x then L 1 instruction in a block L. Let e be the input clock of the instruction. When x is false then control is passed to the rest of the block, at the output clock e ∧ ¬x. Otherwise, control is passed to the block L 1 , at the clock e ∧ x.

There are two ways of passing control from L to L 1 at a given clock e. They are defined by the function G L (L 1 , e): either immediately, by activating the immediate clock x imm L1 , i.e., e ⇒ x imm L1 ; or by a delayed transition to L 1 at e, i.e., e ⇒ x L1 . This choice is decided by the auxiliary function S L (L 1 ). It checks whether the block L 1 can be executed immediately after the block L. By definition, S L (L 1 ) holds iff L 1 > L (L 1 is after L in the control flow) and defs(L 1 ) ∩ defs(L) = ∅ (the set of variables defined in L and L 1 are disjoint).

Example 3 In Example 1, defs(L1) = defs(L2) =

{ocount, idata} and defs(L3) = {count, lock}. Hence, going from L1 to L2 requires a delayed transition because both L1 and L2 define ocount and idata. Conversely, going from L2 to L3 can be done immediately since L3 does not define ocount or idata.

Rule (4) is concerned with the typing of native and external method invocations x = f (y * ). The generic type of f is taken from an environment E(f ). It is given the name of the result x, of the actual parameters y * and of the input clock e to obtain the type of x = f (y * ). On the right, the generic type of 3-address instructions x = f (y, z) at clock e is given by E(f )(xyze). The wait-notify protocol (rules (5 -6)) is modeled using a boolean flip-flop variable x. The notify method, rule (5), defines the next value of the lock x by the negation of its current value at the input clock e. The wait method, rule (6), activates its output clock ŷ iff the value of the lock x has changed at the input clock e: e ∧ (x = x ) ⇒ ŷ. Otherwise, at the clock e \ ŷ, the control is passed to L by a delayed transition e \ ŷ ⇒ x L .

Example 4 Consider the wait-notify protocol at the blocks labeled L1 and L3 in the ones counter. The type of the wait instruction defines the output clock ŷ if L1 receives control at the clock x L1 , and if the value of lock has changed (proposition lock = lock ). If so, at the clock ŷ, ocount and idata are initialized and the control is passed to the block L2 by G L1 (L2, ŷ). Otherwise, at the clock x L1 \ ŷ, a delayed transition to L1 is scheduled:

x L1 \ ŷ ⇒ x L1 .
code type

x L1 ∧ (lock = lock )⇒ŷ x L1 \ ŷ⇒x L1 . . . ŷ⇒x L2 . . . ôcount ∧ x L3 ⇒ ĉount x L3 ⇒lock = ¬lock x L3 ⇒x L1
All return instructions, rules (7 -9), define the output clock x exit L of the current block L by their input clock e. This is the right place to do that: e defines the very condition upon which the block actually reaches its return statement. A goto L 1 instruction, rule [START_REF] Rajamani | A behavioral module system for the π-calculus[END_REF], passes control to block L 1 unconditionally at the input clock e by G L (L 1 , e). A return instruction, rule [START_REF] Talpin | Polychrony for formal refinement-checking in a system-level design methodology[END_REF], sets the exit clock x f to true at clock e to inform the caller that f is terminated. A throw x statement in block L, rule (9), triggers the exception signal x at the input clock e by e ⇒ x. The matching catch statement, of the form catch x from L to L 1 using L 2 passes the control to the handler L 2 and then to the block L 1 upon termination of the handler. This requires, first, to activate L 2 from L when x is present, i.e., G L (L 2 , x ∧ x exit L ), and then to pass the control to L 1 upon termination of the handler. Extension to method calls. The type inference scheme defined for wait, notify and operations, rules (4 -6) can be extended to handle externally defined method calls in a modular and compositional way, as depicted next. Consider a method f with formal parameters x 1..m (whose data-types are not displayed) and a result of type m, rule (a). Let y be an exception raised by the definition pgm of f and escaping from it. The type of f consists of a lambda abstraction whose arguments are the inputs x 1..m , the entry clock x f , the exit clock x exit f , the return value y f and the exception y. It is used to parameterize the proposition P , which corresponds to pgm, with respect to these arguments. The lambda abstraction is instantiated in place of a method invocation L : x 0 = f (x 1..m ), rule (b), which needs to be placed at the beginning of a block (assuming that this block can take several transitions before termination). To model the method call, one just needs to activate the entry clock x f of the method at the input clock e.

Completion of the state logic. The encoding of

(a) I[[m f (x 1..m ) raises y{ pgm }]] = λx 1..m x f x exit f y. I[[pgm]] | | x f ⇒ x min L f /L f (b) I[[L : x 0 = f (x 1..m )]] e L = e ⇒ (E(f )(x 1..m exy) | | e \ (ŷ ∨ x) ⇒ x L ) e∧x (c) I[[return x]] e L = (e ⇒ (x exit L | | x exit f := x))
The output signal x is used to carry the value of the result. Its clock determines when the method has reached the corresponding return statement (rule (c)). When the method terminates, the exit clock of the method call is defined by e ∧ x. Otherwise, if the exception y is raised, a corresponding catch statement handles it. If f has not finished at the end of the transition (at the clock e \ (ŷ ∨ x)), a delayed transition to L is performed e \ (ŷ ∨ x) ⇒ x L in order to resume its execution at the next transition.

A behavioral module system. We define a module system starting from the behavioral type system of Section 4.

The type T of a module m consists of an environment E, that associates fields f and x with types, of a type P that denotes the behavior of its constructor, and of a proof obligation C. The type T 1 → T 2 denotes a template class that produces a module of type T 2 given a parameter of type T 1 .

A proof obligation is a conjunction of propositions of the form P ⇒ Q. A proof obligation P ⇒ Q is incurred by the instantiation of a template class, whose formal parameter has type P and by an actual class parameter, of type Q.

(type) x in the constructor is associated with the behavior E(f ) of the method f it forks and with the type xf ⇐ x, meaning that x triggers f . Type inference for modules. Rule (e) processes a sequence of module declarations sys 1 ; sys 2 . We write

T ::= E, P, C | T → T (context) E ::= [] | E[x : m] | E[f : P ] | E[m : T ] (obligation) C ::= 1 | P ⇒ Q | C ∧ C
E 1 , P 1 , C 1 E 2 , P 2 , C 2 = E 1 E 2 , P 1 | | P 2 , C 1 ∧ C 2
to merge the types of sys 1 and sys 2 . Whereas processing is sequential, the composition of the behavioral type P 1 | | P 2 is synchronous. Rule (f ) first obtains the type T 1 = E 1 , P 1 , C 1 of its class fields. Then, in the environment E extended with that of the class fields E 1 , the body new ; pgm of the constructor is processed to obtain its type T 2 . The type of the module becomes m

• (T 1 T 2 ). The notation m • E, P, C = [m : E], P, C (resp. m • (T 1 → T 2 ) = T 1 → (m • T 2 )
) defines the type of the class m from the type E, P, C of its class fields.

Rule (g) determines the type of a template class m 2 whose formal parameter is a class m 1 that implements the virtual class m. The virtual class m provides the type, and hence the expected behavior, of the formal parameter name m 1 . It is obtained from the environment E by m • T = E(m). The body of the template (i.e. the field declarations dec of the class m 2 ) is type-checked with the environment E extended with the association of m 1 to the type of the class fields E 1 declared in m. This yields the type m 2 • T 2 of the class. The type of the template is defined by associating m 2 with the type (m 1 • T 1 ) → T 2 (and hence m 1 with the type T 1 ). Rule (h) performs the instantiation m 2 m x of a template class m 2 with an actual parameter m to define the class name x. The type (m Proof obligation synthesis. The resolution R(T 1 , T 2 ) of sub-typing constraints is defined by induction on the structure of the pair (T 1 , T 2 ). It reduces to the proof of a conjunction of propositions of the form P 1 ⇒ P 2 . If P 2 is stateless (i.e. it defines no state transitions) then the problem reduces to checking satisfaction of the boolean proposition P1 ⇒ P 2 (where P1 stands for the stateless abstraction of P 1 , e.g., the right-most columns of figure 6). If P 2 is statefull then the problem reduces to verifying that P 1 ⇒ P 2 is an invariant of P , the type of the program, by using modelchecking techniques. Both problems can be expressed and decided in the Polychrony workbench by encoding behavioral types in Signal.

1 • T 1 ) → T 2 (a) I[[dec 1 ; dec 2 }]] E = let E 1 , P 1 , C 1 = I[[dec 1 ]] E in E 1 , P 1 , C 1 I[[dec 2 ]] EE1 (b) I[[m x]] E = [x : m], τ, 1 (d) I[[SC THREAD(f ) sensitive x]] E = [], E(f ) | | (x f ⇐ x), 1 (c) I[[void f () {pgm}]] E = [f : I[[pgm]] E ], τ, 1 (e) I[[sys 1 ; sys 2 ]] E =let E 1 , P 1 , C 1 = I[[sys 1 ]] E in E 1 , P 1 , C 1 I[[sys 2 ]] EE1 (f ) I SC MODULE(m) { dec; SC CTOR(m) {new ; pgm}} E =let E 1 , P 1 , C 1 = I[[dec]] E and T 2 = I[[new ; pgm]] EE1 in m • ( E 1 , P 1 , C 1 T 2 ) (g) I template class m 1 #TYPE(m 1 , m) class m 2 {dec} E =let m • T = E(m) and E 1 , , = m 1 • T and T 2 = I[[dec]] EE1 in [m 2 : (m 1 • T 1 ) → T 2 ], τ, 1 (h) I[[m 2 m x]] E =let (m 1 • T 1 ) → T 2 = E(m 2 ) and m • T = E(m) in x • (T 2 [m 2 .m/m 1 ]) [], τ, (R(T 1 [m 2 .m/m 1 ], T [m 2 .m/m])) )
R(E 1 → T 1 , E 2 → T 2 )⇔R(E 2 , E 1 ) ∧ R(T 1 , T 2 ) R(E 1 [x : t 1 ], E 2 [x : t 2 ])⇔R(E 1 , E 2 ) ∧ (t 2 ≤ t 1 ) R(E 1 [f : P 1 ], E 2 [f : P 2 ])⇔R(E 1 , E 2 ) ∧ (P 2 ⇒ P 1 ) R(E 1 [m : T 1 ], E 2 [m : T 2 ])⇔R(E 1 , E 2 ) ∧ R(T 1 , T 2 ) R( E 1 , P 1 , C 1 , E 2 , P 2 , C 2 )⇔R(E 1 , E 2 ) ∧R(P 1 , P 2 ) ∧R(C 1 , C 2 )

Applications

We have introduced a type system allowing to model the control and data flow graphs of a given imperative program in SSA intermediate form and demonstrated that the expressive capability of the type system's semantics matched that of de-facto standard design languages (e.g. SystemC) and as well as that of related multi-clock synchronous formalisms (e.g. Signal). As such, applications of the proposed type system encompass optimization and verification issues en-countered in related system design methodologies, yet with the following features that merit a highlight.

Scalability. Just as the theory of interfaces automata [START_REF] De Alfaro | Interface theories for component-based design[END_REF], types allow for a scalable level of abstraction to be automatically obtained starting from the type inferred from a SystemC module using a simple formalism. Behavioral types share with interface automata the capability to define static interfaces (boolean relations) and dynamic interfaces (a transition system). Behavioral types allows to relate a given proposition P to a more abstract one, Q, in several ways: a transition e ⇒ x = y can be abstracted by a clock relation between e, x and ŷ; a bound signal x in P/x can be abstracted by any proposition Q not referencing it and containing P . These examples are instances of a more generic abstraction pattern. In general, checking a user-specified abstraction Q consistent with the type P inferred from a given program amounts to the satisfaction of the containment relation [[P ]] ⊆ [[Q]] (i.e. the denotation of P is contained in the denotation of Q). If P is a stateless interface, this amounts to the satisfaction of boolean equations. Similarly, checking that a statefull interface Q is an abstraction of a process P amounts to verifying that Q simulates P by model-checking.

Modularity. The main advantage of formulating a behavioral type system for SystemC is the formal foundation it offers to investigate modular and compositional design methodologies using separate compilation techniques. For instance, suppose that the declared type P of a SystemC class template provides sufficient information about its formal parameter for its body to be checked controllable and compiled. One may then provide it with an actual class parameter, of type Q, satisfying Q ⇒ P , without having the burden of fully instantiating the template code and recompile its code for that given instance.

Design checking. The proposed type system allows to easily formulate properties pertaining on common design errors the analysis of which has been the subject of numerous related works. Most of these approaches consist x 1 := when x L1 when (lock = lock ) x L1 ::= when not x 1 default x L1 idata::= data when x 1 ocount::= 0 when x 1

x L2 ::= when x 1 T1:= idata$1 when x L2 T0:= (T1 = 0) when x L2 x L3 ::= when T0

x 2 := when not x L3 default x L2 T2:= ocount$1 when x 2 T3:= T1 when x 2 ocount::= T2 + T3 when x 2 idata::= (T1 1) when x 2 x L2 ::= when x 2 count::= ocount when x L3 lock::= not lock when x L3 x L1 ::= when x L3

x f ˆ=x L1 ˆ= x L2 ˆ= x L3 x L1 := x L1 $1 init true x L2 := x L2 $1 init false
x L1 :=true when (not x 1 default x L1 default x L3 ) default false x L2 :=true when (x 1 default x 2 ) default false x L3 :=true when T0 default false of proposing an ad-hoc type system for analyzing a specific pattern of design errors: race conditions, deadlocks, threads termination; and in a given programming language: Java, C, SystemC. By contrast, our behavioral type system provides a unified framework to perform both static verification via satisfaction checking or dynamic verification via model checking of behavioral properties of embedded systems described using imperative programming languages. The inference technique itself is language independent and the semantical peculiarities of language-specific runtime features and libraries can be modeled in the polychronous model of computation and its supportive type system.

Termination. One common design error found in embedded system design is the unexpected termination of a thread due to, e.g., an uncaught exception. The termination of the infinite loop of a thread f can be expressed by the property x exit f = 1. Unexpected termination can hence be avoided by model-checking the property that the opposite is an invariant of f : P |= x exit f = 0.

Deadlocks. Another common design error is a wait statement that does not match a notification and yields the thread to block. Let x L1...n be the clocks of the blocks L 1...n in which a lock x is notified. Waiting for x at a given label L eventually terminates if P |= x L ∧ ¬(∧ n i=1 x Li ) = 0.

Race conditions. Similarly, concurrent write accesses to a variable x shared by parallel threads can be checked exclusive by considering the input clocks e 1,..n of all write statements x = f (y, z) by verifying that P |= (e i ∧(∨ j =i e j )) = 0, ∀i = 1, ..n.

Example 5

For instance, consider checking exclusion between the transitions of the ones counter. The type P of the counter implies the equations x L2 = (ŷ 1 ∨ ŷ2 ) and x L1 = x L3 . Verifying exclusion between them amounts to proving that (ŷ 1 ∨ ŷ2 ) ∧ x L3 = 0 is an invariant of P . By construction of P , we have: ŷ1 = x L1 ∧ (lock = lock ), ŷ2 = x L2 \ T0 and x L3 = T0. The property follows by observing that T0 = x L2 .

Design exploration. Just as the multi-clocked synchronous formalism Signal it is based upon, our type system allows for the refinement-based design methodologies considered in [START_REF] Talpin | Polychrony for formal refinement-checking in a system-level design methodology[END_REF] to be easily implemented. Checking the correctness of the refinement of an initial SystemC module, of type P , by its upgraded version, of type Q, amounts to verifying that the final type Q satisfies the assumptions made by the initial specification. In the spirit of the refinementchecking methodology proposed in [START_REF] Talpin | Polychrony for formal refinement-checking in a system-level design methodology[END_REF], this can be implemented by checking the refinement Q to be finitely flow preserving with respect to the initial design P . In general, Q may differ from P by the insertion of a protocol between two components of P , by the adaptation of the services provided by P with a new functionality implemented in Q.

Along the way, one may abstract from the type Q the signals and state variables introduced during the refinement in order to accelerate verification. In most cases, such upgrades may be checked incrementally, by statically checking the containment relation between the stateless abstractions of P and Q.

Implementation in the Polychrony workbench. The Polychrony workbench supports the synchronous multiclocked data-flow programming language Signal in which the translation of the behavioral type system into Signal is easily defined. Thanks to the polychronous model of computation, the SystemC scheduler, used to interleave the execution of threads, does not have to be specified. Indeed, SystemC scheduling amounts to determining a fixed-point to inconsistently propagated signal values using the notion of δcycle, until a fixed-point is reached. Fixed-point of δ-cycles relate to instants in the synchronous semantics using the notion of Kantor metrics of Lee et al. [START_REF] Lee | A framework for comparing models of computation[END_REF]. By contrast, the polychronous model of computation relies on the notion of synchrony to denote this fixed-point directly. Its implementation makes use of type-based scheduling information to determine a static scheduling of elementary instructions.

Related works and conclusions

The capture of the behavior of a system through a type theoretical framework relates our technique to the work of Rajamani et al. [START_REF] Rajamani | A behavioral module system for the π-calculus[END_REF], and many others, on abstracting highlevel and concurrent specifications, e.g. the π-calculus, by using a formalism, e.g. Milner's CCS, in which, primarily, checking type equivalence, e.g. bisimulation, is decidable.

Our contribution contrasts from related studies by the capability to capture scalable abstractions of the type-checked system. In our type system, scalability ranges from the capability to express the exact meaning of the program, in order to make structural transformations and optimizations on it, down to properties expressed by boolean equations between clocks, allowing for a rapid static-checking of design correctness properties (as demonstrated in the examples of Section 5, especially Example 5). Our system allows for a wide spectrum of design abstraction and refinement patterns to be applied on a model, e.g. abstraction of states by clocks, abstraction of existentially quantified clocks, hierarchic abstraction, in the aim of choosing a better degree of abstraction for faster verification.

We share the aim of a scalable and correct-byconstruction exploration of abstraction-refinement of system behaviors with the work of Henzinger et al. on interface automata [START_REF] De Alfaro | Interface theories for component-based design[END_REF]. Our approach primarily differs from interface automata in the data-structure used in the Polychrony workbench: clock equations, boolean propositions and state variable transitions express the multi-clocked synchronous behavior of a system. Compared to an automata-based approach, our declarative approach allows to hierarchically explore abstraction capabilities and to cover design exploration with the methodological notion of refinement along the whole design cycle of the system, ranging from the early requirements specification to the latest sequential and distributed code-generation [START_REF] Talpin | Polychrony for formal refinement-checking in a system-level design methodology[END_REF][START_REF] Le Guernic | Polychrony for system design[END_REF].

The main novelty in our approach is the use of a multiclocked synchronous formalism to support the construction of a scalable behavioral type inference system for the de facto standard system-design language SystemC, and the materialization of a companion refinement-based design methodology imposed through the strong typing policy of a module system, that reduces compositional design correctness verification to the validation of synthesized proof obligations. The proposed type system allows to capture the behavior of an entire system-level design and to re-factor it, allowing to modularly express a wide spectrum of static and dynamic behavioral properties, and to automatically or manually scale the desired degree of abstraction of these properties for efficient verification. The type system is presented using a generic and language-independent intermediate representation. It operates transformations implemented in the platform Polychrony, to perform refinement-based design exploration and directly yields to verification tools using SAT checking and model checking allowing for an efficient verification of expected design properties and an early discovery of design errors.

1 (xFigure 1 .

 11 Figure 1. From a SystemC program to a behavioral types and its abstraction

(Figure 2 .

 2 Figure 2. Abstract syntax for SystemC this end, one could for instance compose the counter P with the proposition Q= def y = y + 1 || y 0 = 0 . Notice that the iteration specified by the proposition Q is not guarded. This means that it is an invariant that describes the successive values of the signal y in time but not the particular time samples at which the signal y should occur. The composition of Q with P has the effect of synchronizing the signal y in Q to the clock s in P : to the time samples during which the signal s holds the value true. This composition is called a refinement: the system obeys the specification denoted by the initial proposition P and is constrained to further satisfy the additional conditions implied by Q.The notation introduced so far holds necessary and sufficient ingredients to specify the behavior of multi-clocked synchronous systems. Pnueli's original STS notation features two additional notions essentially geared towards verification by model-checking: one is choice P ∨ Q, the other explicit absence ⊥. Both can be modeled in the iSTS. An order of execution can be imposed to a proposition by its refinement with a scheduling constraint, noted y → x. Then, x = y is an abstraction of x = y | | y → x where y → x informally means that "x cannot happen before y". In doing so, we refine the time scale, from one in which x and y happen simultaneously, to a more precise one in which one observes that x cannot happen before y. In the remainder, we adopt the syntax x := y borrowed to Signal for an assignment of y to x: (x = y | | y → x).

Figure 2 .

 2 A class declaration class m {dec} associates a class name m with a sequence of fields dec. It is optionally parameterized by a class with template class m 1 . To enforce a strong typing policy, we annotate the class parameter m 1 with #TYPE(m 1 , m 2 ) to denote the type of m 1 with the virtual class m 2 . A module SC MODULE(m) is a class that defines an architecture component. Its constructor SC CTOR(m) {new ; pgm} allocates threads (e.g. SC THREAD(f )) and executes an initialization

Figure 3 .

 3 Figure 3. Translation of the SystemC thread of the EPC into SSA form

L

  and an output clock x exit L . The clock x L is true iff L has been activated in the previous transition (by posting the event x L ). The clock x imm L is set to true to activate the block L immediately. The clock x exit L is set to true when the execution of block L terminates. The default activation condition of a block of label L is the clock x L ∨ x imm L (equation (1) of Figure4). The block L is executed iff the proposition x L ∨ x imm L holds, meaning that the program counter is at L. Otherwise, it is set to 0.For a return instruction or a block, the type inference function returns a type P . For a block instruction stm, the type inference function I[[stm]] e1 L = P e2 takes three arguments: an instruction stm, the label L of the block it belongs to, and an input clock e 1 . It returns the type P of the instruction and its output clock e 2 . The output clock of stm corresponds to the input clock of the instruction that immediately follows it in the sequence of the block.

5 )( 5 )( 6 )

 556 I[[notify x]] e L = e ⇒ (x = ¬x) e I[[notify x]] e L = e ⇒ (x = ¬x) e I[[wait x]] e

  Figure 4 requires all entry clocks x L , x imm L and x f to be simultaneously present when the f is being executed. Each signal x L holds the value 1 iff the block L is active during a transition currently being executed. Otherwise, x L is set to 0. This default setting of the entry clocks requires a completion of the next-state logic by considering, for all L ∈ L f , the proposition e L ⇒ x L implied by the inferred type P = I[[pgm]] and define the default rule by x f \ e L ⇒ ¬x L . Completion is identical for the immediate and exit clocks x imm L and x exit L of the block L. We write x f \ e L ⇒ ¬x L where e L = def (e |P |= e ⇒ x L ).

  The type inference function for modules, I[[sys]] E , Figure 5, assumes a type environment E that associates names with types. We write E(x) for the type of the location x and E(m.x) = F(m)(x) for the path m to x iff E(m) = F, P, C . Type inference for declarations. Rule (a) sequentially processes the declarations dec in a module. Class field declarations contribute to building the type T of a module: rule (b) associates the location x with the type name m in the class-field [x : m], rule (c) associates the procedure f with the class-field [f : P ]. The type τ denotes a program that does nothing. It is neutral by composition. In rule (d), the initialization of a thread SC THREAD(f ) sensitive

Figure 5 .

 5 Figure 5. Type inference for declarations and modules of the template class m 2 and the type m • T of the actual parameter m are obtained from the supplied environment E. Type matching between T and T 1 requires the resolution of a sub-typing between T 1 [m 2 .m/m 1 ] and T 2 [m 2 .m/m]. The term T 1 [m 2 .m/m 1 ] stands for the substitution of the name m 1 by the concatenation m 2 .m in T 1 . The resolution of the type matching constraints reduces to the synthesis of the proof obligation C by the algorithm R. If C is satisfied, then the type of the location x is T 2 [m 2 .m/m 1 ].

Figure 6 .

 6 Figure 6. Model of the EPC in Signal

  The completion of the state-logic is implemented by the aggregation of partial state equations. Notice that L1 and L2 are always activated by a delayed transition, whereas L3 is always immediate when T0 holds.

	Example 6 As an example, embedding the ones counter
	into Signal, Figure 6, consists of emulating control by par-
	tial equations and of wrapping computations using typed
	pragmas statements. This embedding allows to operate
	global architectural transformations on the initial program,
	such as hierarchization or distributed protocol synthesis,
	using the Polychrony platform or perform both static (SAT-
	checking) or dynamic (model-checking) verification of its
	design properties, whose spectrum is outlined next.


INTRODUCTION

One of the most important objectives for the maintenance managers is to balance the maintenance action costs with the investment cost. There is an intensive research to provide the most appropriate strategies for organizing a set of maintenance actions generally based on complex degradation models to optimize a decision criterion. These models usually consider different maintenance actions from the "as good as new" replacement by an identical item, imperfect maintenance which restores the item to an acceptable condition and minimal or "as bad as old" repair. They do not allow us to take into account the appearance of new technology with lower operating and maintenance costs, smaller failure rates, higher quality and output rates. This information is important for managers to decide the replacement investment plan. On the other side, the models devoted to the optimization of the investment planning with the introduction of the technological change (TC) are generally based on the observations of the economical performance of the maintenance process. The proposed models do not consider the diversity of maintenance decisions tackled by the deteriorationbased maintenance models.

These reasons motivate us to provide an appropriate model to meet the operational and strategic requirements. This model is developed to organize both the maintenance and replacement decisions for a continuously deterioration system, under technological evolution.

Most of the references considering the influence of technology change are strictly economicaloriented [START_REF] Bethuyne | The timing of technology Adoption by a cost-minimizing firm[END_REF][START_REF] References Bean | Equipment replacement under Technological change[END_REF][START_REF] Elton | On the optimality of an equal life policy for equipment subject to technological improvement[END_REF][START_REF] Goldstein | A dual machine replacement model: A Note on planning horizon procedures for machine replacements[END_REF][START_REF] Goldstein | Replacement of technology when a new technological breakthrough is expected[END_REF], Hritoneko & Yatsenko 2007, 2008a, b, 2009, Huisman & Kort 2004Nair 1995[START_REF] Nair | Indentifying technology Horizons for the strategic investment decisions[END_REF][START_REF] Mauer | Investment under Uncertainty: The case of replacement investment decisions[END_REF][START_REF] Torpong | A paradox in equipment replacement under technological improvement[END_REF], 2007, Rajagopalan 1999). Their approach are based more on the modeling of the maintenance process through cost functions such as evolution of the operating-maintenance cost instead of the traditional failure indicators such as the degradation or failure rate models. Thanks to these models, the managers can decide the best time for replacement investment of equipment under technological evolution but do not consider the maintenance strategies as well as the impact of technology change on it.

The present work continues in the direction introduced by articles [START_REF] Borgonovo | A Monte Carlo methodological approach to plant availability modeling with maintenance, aging and obsolescence[END_REF], Clavareau & Labeau 2009a, b, Dogramaci & Fraiman 2004[START_REF] Hopp | Maintenance and replacement policies under technological obsolescence[END_REF][START_REF] Karsak | An overhaul-replacement model for equipment subject to technological change in an inflation-prone economy[END_REF][START_REF] Michel | Monte Carlo optimization of the replacement strategy of components subject to technological obsolescence[END_REF][START_REF] Mercier | Optimal replacement policy for obsolete components with general failure rates submitted to obsolescence[END_REF]) that take into account the failure characteristics of the equipment in the replacement problem under technological development. We construct a model that allows us to decide whether to imperfectly maintain, to replace with a higher technology model currently available on the ABSTRACT: The requirement of equipment improvement in order to satisfy the safety and reliability of system motivates the development of technology. The presence or expectation of technologically better equipment will influence managerial decisions on whether to invest in the maintenance of current equipment, invest in replacement with an equivalent model, replacement with a higher technology model currently available on the market, or wait for a potentially even better technology to appear in the near future. Hence, the consideration of technological change is a very important aspect for maintenance and replacement decisions. This paper aims to define a model that allows us to gain insight into how maintenance/replacement policies will be influenced by the expectation of future technology. We then use stochastic dynamic programming (i.e., Markov decision process) to solve for the optimal maintenance and replacement policy of the equipment as a function of performance and cost. Finally, we illustrate the problem through several numerical examples.

market, or wait for a potentially even better technology to appear in the near future. The technology evolution is modeled by a non-homogenous Poisson process and the effect of a new technology is measurable through the degradation characteristics. We also consider that performance of equipment in use will stochastically degrade over time due to deterioration while its accrued profit and maintenance cost will stochastically decrease and increase respectively. The objective of this paper is to maximize revenue over a given planning period horizon. The revenue is defined here as the difference of the incomes and the outcomes. The incomes are the profit, a function of the associated degradation level, and the salvage value in case of replacement which is increasing in the expected mean residual life and proportional to the purchase price of new identical item.

The outcomes are the different maintenance costs and the purchase price in case of replacement with a new technology. A discrete time non-stationary Markov Decision Process (MDP) formulation is proposed to determine the optimal action plan. This paper is structured as follows: In Section 2, a related literature is presented to motivate the present work. Section 3 is devoted to the mathematical formulation. In Section 4, the performance of our model is discussed through numerical examples. Finally, a conclusion and future work are discussed in Section 5.

RELATED LITERATURE

There are few articles that consider the maintenance replacement problem under technological development with degradation performance. The articles of Clavareau & Labeau (2009a, b), [START_REF] Michel | Monte Carlo optimization of the replacement strategy of components subject to technological obsolescence[END_REF], [START_REF] Mercier | Optimal replacement policy for obsolete components with general failure rates submitted to obsolescence[END_REF] examine preventive, corrective replacement strategies of N identical components. However, because of the complexity of the system, they must simplify the technological evolution model. They consider a single new technology that has already appeared on the market with deterministic parameters. These assumptions are very limited because the technology develops rapidly and continuously. In addition, they are interested only in finding the optimal policy to replace obsolete equipments by new type, without considering whether the replacements is necessary. In our model, to attach special importance to both the continuation and the flexibility of technological change, we simplify the model by examining single equipment such as articles [START_REF] Borgonovo | A Monte Carlo methodological approach to plant availability modeling with maintenance, aging and obsolescence[END_REF][START_REF] Hopp | Maintenance and replacement policies under technological obsolescence[END_REF][START_REF] Dogramaci | Replacement decisions with maintenance under uncertainty: an imbedded optimal control Model[END_REF].

We formulate a discrete time non-stationary Markov Decision Process to determine the optimal maintenancereplacement policy. The similar model with non-stationary technological appearance's probability in time was proposed by [START_REF] Nair | Modeling strategic investment decisions under sequential technological change[END_REF][START_REF] Nair | Indentifying technology Horizons for the strategic investment decisions[END_REF]. However, in these papers, the author only considers replacement problem, not examining decision to maintenance as our model. Karsark & Tolga (1998) integrate overhaul policy into replacement problem. With geometric technological evolution model, they formulate a discrete time Markov decision process to determine an optimal overhaulreplacement policy which maximizes the expected present worth over a finite horizon time. But they also study this problem from manager's point of view, not taking into account failure rate or deterioration process of machines. Considering of parametric performance represented by a Markovian deterioration process, [START_REF] Hopp | Maintenance and replacement policies under technological obsolescence[END_REF] also utilize MDP algorithm to dealing the equipment replacement problem under technological change. However, recall that they only consider the equipment replacement problem while our work also examines the decision of maintenance. On the other hand, unlike [START_REF] Hopp | Maintenance and replacement policies under technological obsolescence[END_REF] reviewing unique challenger, we study a technological sequence.

To model sequential technological evolution, we combine the geometric model and uncertain apparition model of technology. The geometric technological evolution model is presented by [START_REF] Borgonovo | A Monte Carlo methodological approach to plant availability modeling with maintenance, aging and obsolescence[END_REF], [START_REF] Torpong | A paradox in equipment replacement under technological improvement[END_REF], [START_REF] Karsak | An overhaul-replacement model for equipment subject to technological change in an inflation-prone economy[END_REF]), Hritoneko & Yatsenko (2007, 2008a, b), [START_REF] Bethuyne | The timing of technology Adoption by a cost-minimizing firm[END_REF]. But except [START_REF] Borgonovo | A Monte Carlo methodological approach to plant availability modeling with maintenance, aging and obsolescence[END_REF], the rest study the problem without parametric degradation. They utilize the geometric model to form the cost functions in vintage equipment or in time. Unlike these articles, we present technology change by the improvement of the expected deterioration rate. Moreover, our profit or maintenance cost functions are only dependent on degradation state. As the expected degradation rate of equipments is improved over technology generation, accrued profit and maintenance cost will be dependent on technology generation.

In addition, we also consider non-stationary likelihood of new technology's apparition over time. Thereby, we overcome the disadvantages of the geometric model proposed by [START_REF] Borgonovo | A Monte Carlo methodological approach to plant availability modeling with maintenance, aging and obsolescence[END_REF]. In that article, the failure rate decreases exponentially over time, i.e. at any time, a machine can be replaced by new one which operates better with its reliability parameters determined at that time. In reality, this assumption is unreasonable because technical characteristics of the equipment can't always be changed over time. It changes only at the concurrent instant of a new technological generation. Recall that [START_REF] Nair | Modeling strategic investment decisions under sequential technological change[END_REF][START_REF] Nair | Indentifying technology Horizons for the strategic investment decisions[END_REF]) also considers the nonstationary probability of the appearance of new technologies. But in his model, Nair focuses on the problem of capital investment decisions due to technological change rather than physical deterioration of equipment. To simplify its exposition, he also don't consider salvage values while we establish the reasonable salvage value function which depends on its mean residual life and the purchase price of identical technology at this time.

MODEL FORMULATION

Maintenance problem

Consider a repairable machine that operates continuously from the new state, X = 0, until a failure threshold, ζ. A machine is characterized by its expected deterioration rate. In the failure state, denoted m, the machine continues to operate but unprofitably. To reveal the deterioration level, periodic inspections are performed. The inter-inspection interval, τ, defines the decision epochs.

We assume that only one new technology can appear in a decision interval, τ. We introduce

1 1   k i
p , the non stationary probability that technology k+1 appears in the interval τ given the latest available technology at decision epoch i is k. The difference in the technologies k and k+1 is modeled by an improvement factor on the expected instantaneous deterioration rates.

Let (x, k, j) be the system state at the beginning of the i th decision epoch with observed deterioration level x when technology j is used and the technology k, k ≥ j, is available. Then, the maintenance decisions are restricted to:

1) Do nothing (DN): The machine continues to deteriorate until next decision epoch and generates a profit g(x). Note that g(x) is the accrued profit within a period, depends only on the deterioration state at the beginning of that period. This assumption is not very restrictive in case where the decision period is sufficiently small and the decreasing rate of the profit function in deterioration state is not very fast.

2) Maintain (M) which allows to restore the machine in a given deterioration level, max(0, x-d) where d models the maintenance efficiency. An increasing maintenance cost in the deterioration, c M (x), is incurred and as we assume that the maintenance time is negligible, then, in the next decision interval, the machine deteriorates from the level x-d and generates a profit g(x-d).

3) Replace (R) the equipment with the latest available technology k. The replacement time is also negligible. The cost of such a replacement is given by the difference between the purchase price of the new machine c i,k and the salvage value b i,j (x). The purchase price is an increasing function of technology and decreasing over time. The salvage value is proportional to the purchase price of technology j and decreasing in the remaining lifetime. In the i th decision period after the replace-ment, the new machine generates a profit g(0). Note that as the deterioration rates of new technological machine, the purchase price can be estimated. This is realistic in case where the technical parameters and specifications of futures designs may be know beforehand.

In case of failure, the do nothing action is still allowed but the profit in the next decision epoch is assumed to be negative g(m) < 0.

Decision criteria formulation

In this paper, we use a non-stationary MDP formulation to find the optimal maintenance-replacement policy to maximize the expected discounted valueto-go over the finite horizon time denoted by V π (s). If the last decision period is N, at decision epoch N+1, we do not make any decision and the maximum expected discounted value-to-go from the decision epoch N+1 over the infinite horizon is V N+1 (s) = 0 ( S s   : state space of system). Let V i (x,k,j) denote the maximum expected discounted value from the decision epoch i,

(k ≤ i) to the last epoch N. Then, V 1 (s) = V π (s). (x,k,j)} R (x,k,j) DM (x,k,j) {DN (x,k,j) V i i i i , , max  (1)
where DN i , M i , R i are alternately choice to do nothing, to maintain and to replace at decision epoch i th .

We have:

          ) 1 , { ' ] , [ ' 1 )] , ' , ' ( ) , , | , ' , ' ( [ ) ( ) , , ( k k k x x i i i j k x V j k x j k x p x g j k x DN   (2) ) , }, , 0 (max{ ) ( ) , , ( j k d x DN x c j k x M i M i     (3) ) , , 0 ( ) ( ) , , ( , , k k DN x b c j k x R i j i k i i     (4) λ: discount factor; λ  [0, 1].

Transition probabilities

To compute the transition probabilities, we propose to discretize the deteriorating state of machine as follows. Let z denote the discrete deterioration state at the beginning of the current decision period. z is the first value of N X discrete intervals of length l on [0, ζ] (which ζ is the failure threshold of the machine). That is to say, if the deterioration state (x) at the beginning of current decision period belongs to the intervals ([0, l[, [l, 2l[, [2l, 3l[, ..., [(N X -1)l, ζ[), we approximate x by z {0, l, 2l, 3l ... (N X -1)l} and when the deterioration state (x) at the beginning of current decision period is exceed the failure threshold (x ≥ ζ), we use m to present failure state of the machine. The deterioration state of the machine (x) is approximated by z, z  {0, l, 2l, 3l ... (N X -1)l, m}. Then, after preventive maintenance, the deterioration state is reduced by a determined amount of deterioration units d. The transition probability is:

' 1 ) | ' ( ) , , | ' , ' , ' ( k i j i p x x p j k x j k x p   (5)
where x'  {z, z+l , …, (N X -1)l, ζ}; k' {k, k+1}

Recall that the deterioration state of the machine at the next decision epoch depends only on its deterioration state at the current epoch decision and the technological generation of this machine, denoted by p j (x'|x); and ' 1 k i p  is the appearance probability of the next technological generation (k+1) at the next decision epoch (i+1) with k' = k+1 or inversely, it is the non-appearance probability with k'= k.

dy y f x x p l z z z z j j ) ( ) | ' ( ' '      (6)
with z, z '  {0, l, 2l, 3l … (N X -1)l} and f j (y) is the probability density function of the deterioration process of the machine's generation j th within the decision period τ. Similarly,

dy y f x m p z j j ) ( ) | (      (7)

NUMERICAL EXAMPLES

In this section, we present numerical examples to illustrate the performance of our model.

Input parameters

The appearance probability of new technology

We define the appearance probability of new technology k+1 at decision epoch i+1, given the latest available technology at decision epoch i is k, as a time increasing function:

) 1 ( 1 1 k i k i p       (8)
δ is the factor that reflects the non-appearance probability of next generation (k+1) at next decision epoch (i+1) when the latest available technology at the current epoch i is k and k  i. The smaller δ is, the greater appearance probability is. And ε is the factor characterized the increasing rate of the appearance probability of new technology over time; ie. if the technological generation k+1 is not appear at decision epoch i+1, then it can appear at the next decision epoch (i+2) with probability 1 -δε given the appearance probability of (k+1) at (i+1) is 1 -δ. We have: δ, ε  [0, 1].

Deterioration process

We consider the machine whose degradation process is modeled by the Gamma distribution: Gamma processes are often used to model the equipment's degradation [START_REF] Van Der Weide | Gamma process and peaks-over-threshold distributions for time-dependent reliability[END_REF][START_REF] Van Noortwijk | A survey of the application of gamma processes in maintenance[END_REF].

In any decision period, the increments of deterioration X j (i + 1) -X j (i) are independent, identical, and follow the stationary Gamma distribution with shape parameter α j τ (recall that τ is length of a decision period) and scale parameter β. The probability density function of the deterioration process of the machine's generation j in decision period τ is:

x j j j j e x x f             1 ) ( ) ( ( 9
)
where β is a constant and a discussion for the improvement of α j is given in the next paragraph.

Impacts of the technological evolution

As we have assumed, the technological evolution aims to improve degradation characteristics, and specifically the expected degradation rate. In case of stationary gamma processes, this expected degradation rate is directly proportional to the shape parameter α j . We model the impact of the technological evolution with the following decreasing exponential geometric function:

b ae j j     ) 1 (   (10)
where κ, a, b are constants; j ≥ 1.

Due to technological development, the deterioration rate of the machine is improved. It is convergent to the critical value, b, but the deterioration could not be excluded. We choose arbitrarily κ, a, b such as values in Table 1.

Additionally, under technological evolution, the purchase price of a new machine is assumed to be decreasing over time and normally increasing over technological generation:

1 1 1 , 1 ,    k i k i u v c c ( 11
)
where c 1,1 is the purchase price the first of technological generation at the first decision epoch; v is a constant, characterizing the decrease of purchase price over time (v ≤ 1) and u is constant, characterizing the change of the purchase price over technological generation. We choose arbitrarily c 1,1 , v, u such as values in Table 1, then c i,k is given in Table 2. We assume the salvage value is a function of the current purchase price of this technology at this decision epoch, and the Mean Residual Lifetime (MRL).

According to the degradation assumptions, if x is the observed state, we define the MRL(x) as the expected number of decision epoch from the current decision epoch until the failure. In case of stationary gamma processes, the mean deterioration rate on a decision epoch is constant and equals to α j τ/β. Hence, we have:

) ( ) ( x x MRL j       . ( 12
)
Then, we propose the following function for the salvage value,

 x ϵ [0, ζ] ))] ( exp( 1 [ ) ( , , x rMRL hc x b j i j i    ))] ( exp( 1 [ , x r hc j j i         (13)
h, r are constant.

The profit and maintenance cost function

We know that the machine will operate less efficiently when its deterioration state is greater. Therefore, the expected accrued profit function in a decision period τ is decreasing by deterioration state and the greater the deterioration state is, the faster the decreases of the profit function is. To reflect this nature, we use a decreasing concave function of deterioration state x to characterize the accrued profit. On the contrary, the greater the deterioration state is, the faster the increase of the maintenance cost function is. Therefore, we use an increasing convex maintenance cost function. The optimal policy for the Example 1 is given in Table 3. For each decision epoch i, with the used technology j, given the generation k is the latest available technology, the decision matrix defines the optimal maintenance decision according to the current deterioration x:

) exp( ) ( 1 0 x r r c x c c M      (15)  x ϵ [0, ζ]; c 0 , r c are constant.
Do nothing if x ϵ [x 1 , x 2 ), maintain if x ϵ [x 2 ,
x 3 ) and replace with the new technology if x ϵ [x 3 , x 4 ].

Table 3. The optimal policy in Example 1, N = 5

i k, j Do Nothing [x 1 , x 2 ) Maintenance [x 2 , x 3 )
We find that the optimal policy for Example 1, given in Table 3 has some basic properties:

1) The maintenance threshold (x 2 ), i.e. the first time where the optimal policy prescribes to maintain across deterioration state x, depends only on the technological generation of the used machine j. Consider, for example, at decision epoch i = 3, the used technology j = 1, for which the optimal policy prescribes maintenance from the deterioration state x 2 = 3.7 despite the latest available technology k = 1, 2, or 3. Moreover, the greater the used technology is, the higher the threshold is, because deterioration rate is improved under technological development. For example, at i = 3, k = 3, this threshold is: x 2 = 3.7; 4.3; 4.5 for the used technology j = 1, 2, 3 respectively.

2) The replacement threshold (x 3 ) is nondecreasing in the difference between the latest available technology and the used technology because the purchase price is increasing over technological generation. For example, at decision epoch i = 3, when the latest available technology is k = 3, the replacement threshold is 9.9; 9.1; 8.5 for the technology used is j = 1, 2, 3 respectively. Certainly, this threshold depends also on used technological generation (j). It is non-decreasing in the used technology j. For example, at the decision epoch i = 3, when the used technology (j) is also the latest technology available (k), the replacement threshold is 8.3; 8.3; 8.5 for j = k = 1, 2, 3 respectively. These properties are maintained even if the finite horizon N is large enough. Consider, Example 2 with the input parameters as Example 1: the optimal policy for the first three decision epochs in planning horizon N = 20 is given in Table 4. Recall that technological development is characterized by the improvement of the deterioration rate and the change of the purchase price c i,k . Now, we consider the influence of these parameters on the optimal maintenance-replacement policy.

Note that the characterization of purchase price is represented by equation: c i,k = c 1,1 v i-1 u k-1 where u is parameter that reflects directly the change of purchase price under technological development. When u > 1, the purchase price is increasing in technological generation, inversely, u < 1 this is the case where the technological improvement contributes to reduce the purchase price, and u = 1 is the case where the technological change does not influent on the purchase price.

As illustrated by the numerical examples in planning horizon N = 20, with u = 0.95, 1 and 1.05, consider the first three decision epochs (Table 5), we find that at the first decision epoch, the smaller u is, the higher the replacement threshold (x 3 ) is. x 3 = 7.7; 7.5; 7.3 respectively. The firm tends to keep the machine used for waiting the appearance of new technology. In the case where the new technology was available on the market, the firm tends to replace earlier when u is smaller. For example, at decision epoch i = 2, given j = 1 and k = 2, the replacement threshold is 7.3, 6.9, 6.5 for u = 1.05, 1, 0.95 respectively.

Specially, in the obsolete case, when the firms decide to replace early, the optimal policy can be non-monotone with respect to the DN and DM across deterioration x for given k, j. For example, with u = 0.95, at decision epoch i = 2, for k = 2, j = 1, the optimal policy prescribes do nothing until x = 2.5, maintain from x = 2.5 to 4.7 and then do nothing again at x = 4.7 until 6.5 (Table 6). Now, we will consider how the improvement of the deterioration rate influences the optimal policy. Recall that the shape parameter of stationary Gamma function of deterioration process is represented by the decreasing exponential geometric function (equation 10); where κ characterizes directly the improvement of the deterioration rate.

We implement numerical examples in planning horizon N = 20 with κ = 0.4, 1, 1.5 and obtain the results in Table 7. We find that when j = k, the replacement threshold is non decreasing in κ. Specially, at the first decision epoch, the replacement threshold is increasing in κ, because the firms tend to replace later for waiting the new technology when the improvement of deterioration rate is more efficient (κ is increasing). Consider, at i = 1, the shape parameter of the first technological generation is the same as in the case where κ = 0.4, 1, 1.5, then, the replacement threshold is 7.3, 7.5, 7.7, respectively. The case where the obsolete problem appears (j < k) is more complex. The replacement threshold is nonmonotonic in κ. For example, at i = 3, the replacement threshold is decreasing in κ, for (k = 2, j = 1) or for (k = 3, j = 1), but it is increasing in κ for (k = 3, j = 2).

Moreover, this parameter (κ) influences also on the maintenance policy such as: the increase of the maintenance threshold (x 2 ) in j > 1 and the appearance of the non-monotone property with respect to the DN and DM across deterioration x for given k, j. As illustrated by Table 8, with κ = 1.5, at decision epoch i = 2, for k = 2, j = 1, the optimal policy prescribes do nothing until x 2 = 1.5, maintain from x = 1.5 to 5.9 and then do nothing again from x = 5.9 to 6.3. [0, 1.5) [1.5, 7.5) [7.5, 20] 2, 1 2, 2

CONCLUSION

In this paper, we proposed a model that allows us to consider both the investment and the maintenance problem of the stochastic deterioration system under the technological development. It determines the maintenance strategy from the operator's point of view, based on parametric performance of system. In addition, it allows the manager to take into account the necessary information of technology change to decide the best time for replacement investment of equipment as well as to consider the impact of technological evolution on the maintenance strategies.

We have considered a lot of assumptions and parameters in our model to tackle the complexity of the decision environment for the maintenance managers. We have assumed that technological evolution is stochastic and the impact of a new technology can be measured not only from an economical point of view but also on the system deterioration performance. This high number of parameters is also due to our choice of integrating a quite well-advanced maintenance strategy (condition-based repair and replacement policy) to ensure the "local" optimality, i.e. independently on the technical change opportunity, in the strategic decision context.

We then used stochastic dynamic programming (i.e., discrete non-stationary Markov decision process) to solve for the optimal maintenance and replacement policy of the equipment as a function of performance and cost. And finally, we presented numerical examples to illustrate performance of our model and to consider the influence of the parameters characterized the technological development on the optimal maintenance-replacement policy. Some proposed assumptions can be seen as limitations of our model. The uncertainty in the technological evolution, e.g., is just considered in the time of appearance of a new generation but the associated purchase cost and the deterioration improvement are deterministic. In fact, these can be stochastic and difficult to capture.

The future work could reflect the stochastic characterization of these parameters. Furthermore, the stochastic efficiency of the imperfect maintenance action could also be included in our model or the conception of technology horizon N such that the initial optimal decision would be invariant even if more than N technologies wear to appear in future, could be consider .



  x ϵ [0, ζ]; g 0 , r g are constant.

Table 1 .

 1 The input parameters for the Example 1

	Appearance prob-	δ	ε
	ability		0.8	0.96
	Profit & Discount	g 0	r g	λ
	factor		213.2 1.2	0.8
	Maintenance	&	d	c 0	r C	ζ
	Failure threshold	1.4	3.322 0.178 20
	Deterioration		β	a	b	κ	N X
	process		2.22	3	0.4	0.4	100
	Salvage value &	h	r	c 1,1	v	u
	Purchase price		0.8	0.4	100	0.98	1.05

Table 2

 2

	i	c i,1	c i,2	c i,3	c i,4	c i,5
	1	100
	2	98	102.9
	3	96.04	100.84	105.88
	4	94.12	98.83	103.77 108.95
	5	92.24	96.85	101.69 106.78	112.11
	4.2 Analysis from numerical experiments
	4.2.1 Basic properties of the optimal policy.

. The purchase price for the Example 1 of the technology k at decision epoch i, N = 5.

Table 4 .

 4 The optimal policy for the first three decision epochs in planning horizon N = 20.

	i	k, j	Do Nothing	Maintenance
			[x 1 , x 2 )	[x 2 , x 3 )
	4.2.2 Influence of the technological improvement pa-
	rameter on the optimal policy

Table 5 .

 5 The replacement threshold for the first three decision

	epochs in planning horizon N = 20 with u = 0.95; 1; 1.05
	i	k, j	u = 0.95	u = 1	u = 1.05
	1	1, 1	7.7	7.5	7.3
	2	1, 1	7.7	7.5	7.1
		2, 1	6.5	6.9	7.3
		2, 2	7.1	7.1	7.1
	3	1, 1	7.7	7.5	7.1
		2, 1	6.5	6.9	7.1
		2, 2	7.1	7.1	7.1
		3, 1	5.5	6.5	7.5
		3, 2	6.1	6.5	7.5
		3, 3	6.7	6.9	7.3

Table 6 .

 6 The optimal policy for the first three decision epochs in the planning horizon N = 20 with u = 0.95

	i	k, j	Do Nothing Maintenance Replacement
	1 1, 1	[0, 1.5)	[1.5, 7.7)	[7.7, 20]
	2 1, 1	[0, 1.5)	[1.5, 7.7)	[7.7, 20]

Table 7

 7

		. The dependence of the replacement threshold on κ in
	planning horizon N = 20
	i	k, j	κ = 0.4	κ =1	κ =1.5
	1	1, 1	7.3	7.5	7.7
	2	1, 1	7.1	7.5	7.5
		2, 1	7.3	6.5	6.3
		2, 2	7.1	7.3	7.3
	3	1, 1	7.1	7.3	7.5
		2, 1	7.1	6.5	6.3

Table 8 .

 8 The optimal policy for the first three decision epochs in the planning horizon N = 20 with κ = 1.5

	i	k, j	Do Nothing Maintenance Replacement
	1 1, 1	[0, 1.5)	[1.5, 7.7)	[7.7, 20]
	2 1, 1