Introduction

In this work, systems are seen as black boxes. Their behaviour is only functional, so we will only express functional constraints on them. This kind of constraints is one perfect thing to be formalized, since it is very close to mathematical notions. Moreover, let us precise some important points:

-This work only deals with deterministic systems, for which we are able to describe the set of possible executions. -In this work, time is considered discrete. That allows us to speak about the previous or next instant of an t.

Notations

In the present work, the concatenation of two vectors A and B will be noted

A ⊗ B.

More generally, we will note f ⊗ g : A ⊗ C → B ⊗ D the concatenation of f : A → B and g : C → D.

Preliminary definitions

In this section, we recall the definitions introduced in [3] and reviewed in [4] to formalize the notion of system, a timed extension of Mealy machines to model heterogeneous integrated systems and their integration.

Definition 1 (Type). The notion of type will be the classical "set of values" one.

Time

Time is an underlying, yet very important, point of our formal approach. Indeed, real-life systems are naturally described according to various types of "times". As a result, we need to deal uniformaly with both continuous and discrete times.

While this problem has been shown hard by [2], some solutions have been found in studies like [5] to introduce formal models for mixed discrete-continuous systems. We give here a set of definitions to handle such systems. Informally, as very well expressed in [3], time is "a linear quantity composed of ordered moments, pairs of which define durations".

Definition 2 (Time reference).

A time reference is an infinite set T together with an internal law + T : T × T → T and a pointed subset (T + , 0 T ) satisfying the following conditions:

-upon T + : • ∀a, b ∈ T + , a + T b ∈ T + closure (∆ 1 ) • ∀a, b ∈ T + , a + T b = 0 T =⇒ a = 0 T ∧ b = 0 T initiality (∆ 2 ) • ∀a ∈ T + , 0 T + T a = a neutral to left (∆ 3 ) -upon T : • ∀a, b, c ∈ T, a + T (b + T c) = (a + T b) + T c associativity (∆ 4 ) • ∀a ∈ T, a + T 0 T = a neutral to right (∆ 5 ) • ∀a, b, c ∈ T, a + T b = a + T c =⇒ b = c cancelable to left (∆ 6 ) • ∀a, b ∈ T, ∃c ∈ T + , (a + T c = b) ∨ (b + T c = a) linearity (∆ 7 )

Definition 3 (Time scale). A time scale is any subset T of a time reference T such that:

-T has a minimum m T ∈ T -∀t ∈ T, T t+ = {t ∈ T | t ≺ t } has a minimum called succ T (t)

-∀t ∈ T , when m T ≺ t, the set T t− = {t ∈ T | t ≺ t} has a maximum called pred T (t) -the principle of induction2 is true on T.

The set of all time scales on T is noted T s(T ).

Dataflows

Together with this unified definition of time, we need a definition of data that allows to handle the heterogeneity of data among real-life systems. We rely on the previous definitions to describe data carried by dataflows.

Definition 4 ( -alphabet).

A set D is an -alphabet if ∈ D. For any set B, we can define an -alphabet by B = B ∪ { }.

Definition 5 (System dataset). A system dataset, or dataset, is a pair D = (D, B) such that:

-D is an -alphabet -B, called data behavior, is a pair (r, w) with r : D → D and w : D×D → D such that3 :

• r( ) = (R1) • r r(d) = r(d) (R2) • r w(d, d ) = r(d ) (R3) • w r(d ), d = d (W1) • w w(d, d ), r(d ) = w(d, d )(W2

Systems and integration operators

Given the previous definitions, we are now able to give a mathematical definition of systems. Informally, our definition is very similar to timed Mealy machines with two important differences: the set of states may be infinite and the transfer function transforms dataflows. The key point is to see those systems as black boxes that just behave the way they are supposed to.

Definition 8 (System). A system is a 7-tuple ∫ = (T, X, Y, Q, q 0 , F, δ) where:

-T is a time scale, -X, Y are input and output datasets,

-Q is a nonempty -alphabet 4 of states, -q 0 is an element of Q, called initial state, -F : X × Q × T → Y describes a functional behavior, -δ : X × Q × T → Q describes a state behavior.

Figure 1 illustrates this definition. Example 1. A very basic radiator with an internal thermostat placed in a room can be modeled as a system S = (T, X, Y, Q, q 0 , F, δ) with:

Y(t) Q(t) X(t)-T ∼ N -X = room temperature ∼ R -Y = {heat, nothing} -Q = {q on , q of f } -q 0 = q of f -F(x(t), q(t)) = heat if q(t) = q on ∅ otherwise -δ is a follows: q of f q on x(t) < θ ⊥ x(t) > θ

It is important to understand here that at each time instant of the time scale, the state of the system changes instantly and before F computes the resulting output. At m Ts , the beginning of the time scale, the state of the system is q 0 . But as soon as the first input data arrives, at succ T (m Ts ), the state of ∫ changes so that the functional behaviour ignores q 0 . Figure 2 illustrates this behaviour and we give the following formal definition for timed executions of systems. Definition 9 (Execution of a system). Let ∫ = (T, X, Y, Q, q 0 , F, δ) be a system. Let In ∈ X T be an input dataflow for ∫ and Ĩn = In T . The execution of ∫ on the input dataflow In is the 3-tuple (In, S, Out) where:

-S ∈ Q T is recursively defined by:

• S(m T ) = δ Ĩn(m T ), q 0 , m T • ∀t ∈ T, S(t + ) = δ Ĩn(t + ), S(t), t + where t + = succ T (t) -Out ∈ Y T is defined by: • Out(m T ) = F Ĩn(m T ), q 0 , m T • ∀t ∈ T, Out(t + ) = F Ĩn(t + ), S(t), t + where t + = succ T (t)

In, S and Out are respectively input, state and output dataflows. We note exec(∫ ) the set of possible executions of ∫ .

Definition 10 (Product of systems on a time scale).

Let (∫ i ) i = (T, X i , Y i , Q i , q 0i , F i , δ i ) i be n systems of time scale T. The product ∫ 1 ⊗• • •⊗∫ n is the system T, X, Y, Q, q 0 , F, δ

where:

-X = X 1 ⊗ • • • ⊗ X n and Y = Y 1 ⊗ • • • ⊗ Y n -Q = Q 1 × • • • × Q n and q 0 = (q 01 , . . . , q 0n ) = q 01...n -F x 1...n , q 1...n , t = F 1 (x 1 , q 1 , t), . . . , F n (x 1 , q 1 , t) -δ x 1...n , q 1...n , t = δ 1 (x 1 , q 1 , t), . . . , δ n (x 1 , q 1 , t)

Remark 1. This definition can be extended to systems that do not share a time scale, thanks to a technical operator introduced in [3]. This operator builds a timed-extension of a system, which is a system that has an equivalent inputoutput behaviour as the original system, but on a wider time scale. Figure 3 illustrates this idea.

Definition 11 (Feedback of a system). Let ∫ = T, (D×In, I), (D×Out, O), Q, q 0 , F, δ be a system such that there is no instantaneous influence of dataset D from -I is the restriction of I to In, and O is the restriction of O to Out -F (x ∈ In, q ∈ Q, t) = F (d x,q,t , x), q, t Out -δ (x ∈ In, q ∈ Q, t) = δ (d x,q,t , x), q, t where d x,q,t stands for F ( , x), q, t D . Figure 4 Definition 12 (Abstraction of a transfer function). Let F : X T → Y T be a transfer function. Let A x : X T → Y a Ta be an abstraction for input dataflows and A y : Y T → Y a Ta an abstraction for output dataflows. The abstraction of F for input and output abstractions (A x , A y ) with events E is the new transfer function Definition 13 (Abstraction of a system). Let ∫ = T, X, Y, Q, q 0 , F, δ be a system. ∫ = T a , X a ⊗ E, Y a , Q a , q a0 , F a , δ a is an abstraction of ∫ for input and output abstractions (A x , A y ) if, and only if:

Proceedings of theF a : (X a ⊗ E) T → Y a Ta defined by: ∀x ∈ X T , ∃e ∈ E Ta , F a A x (x T ) ⊗ e = A y F (x)∃A q : Q T → Q a

Ta , for all execution (x, q, y) of ∫ , ∃E ∈ E Ta , A x (x T ) ⊗ E, A q (q), A y (y) is an execution of ∫ . Conversely, ∫ is a concretization of the system ∫ .

A system captures the behavior of a system that can be observed (functional and states behavior, called together systemic behavior ). From this definition, we can start expressing behaviour properties.

Systemic behaviour properties: a formal semantics

The goal of this section is to be able to describe the behaviour of such a system, in order to express properties and constraints on it. To do so, we will define a semantics of systems and provide a formal definition of "properties". The idea here is that systems are described by executions, so we must use timed properties. We will first describe our property syntax language, then our property semantics.

Definition 14 (System property formulas). Let ∫ = (T, X, Y, Q, q 0 , F, δ) be a system. The set P (∫ ) of property formulas over ∫ , similar to LTL6 , is inductively defined as follows.

Here are the atomic formulas, where (x, q, y) ∈ X × Q × Y :

-input(x), which means that the current input of ∫ has to be x -istate(q), which means that the current state of ∫ has to be q -ouput(y), which means that the current output of ∫ has to be y And here are the operators, where (φ, φ 1 , φ 2 ) ∈ P (∫ ) 3 :

-¬φ -φ 1 ∧ φ 2 -

φ, which means that φ has to hold at the next state of the execution -φ 1 Uφ 2 , which means that φ 2 eventually has to hold and until it does, φ 1 has to hold (φ 1 can hold further)

Definition 15 (Other system property formulas). Let ∫ = (T, X, Y, Q, q 0 , F, δ) be a system. Let (φ, φ 1 , φ 2 ) ∈ P (∫ ) 3 .

The previously defined language P (∫ ) can be extended with the following operators:

- -⊥ -φ 1 ∨ φ 2 -φ 1 ⇒ φ 2 7

-♦φ, which means that φ has to hold now or in a future state of the execution -φ, which means that φ has to hold for the entire subsequent execution -φ 1 Rφ 2 , which means that φ 1 has to hold until and including a state when φ 2 holds, which is not forced to happen if φ 1 holds forever P (∫ ) is the syntax of our properties language. It gives us a way to express properties on executions of ∫ . We are now able to define our semantics. The following rules describe the satisfaction of P (∫ ) formulas using only the first set of operators, but such rules could be easily extended to the extended set of operators. Definition 16 (system property satisfaction). Let ∫ be a system. The satisfaction of a P (∫ ) formula φ by an execution e of ∫ , written e φ, is defined according to the following rules:

[AI] (x 0 , , ), . . . input(x 0 )

[AS] ( , q 0 , ), . . . istate(q 0 )

[AO] ( , , y 0 ), . . . In this case, φ is said to be a behaviour constraint on ∫ .

Example 2. Unsing our previous example 1, with θ ⊥ = 15 and θ = 20, here are some behaviour constraints one would want to express on the system:

-∫ ¬♦ istate(q of f ) ∧ output(heat) -∫ ¬♦ input(10) ∧ istate(q of f )

or, even more generally:

-∀θ > θ , ∫ ¬♦ input(θ) ∧ istate(q on )

Computation rules over behaviour constraints

We give here a minimalist set of computation rules to establish proofs about system behaviours. A more advanced set of rules might be needed to ease such proofs.

Proposition 1 (Product of two systems). Let∫ 1 = (T, X 1 , Y 1 , Q 1 , , , ) and ∫ 2 = (T, X 2 , Y 2 , Q 2 , , , ) be two systems. Let (x 1 , x 2 ) ∈ X 1 × X 2 , (y 1 , y 2 ) ∈ Y 1 × Y 2 and (q 1 , q 2 ) ∈ Q 1 × Q 2 . ∫ 1 input(x 1 ) ∫ 2 input(x 2 ) [PI] ∫ 1 ⊗ ∫ 2 input(x 1 ⊗ x 2 ) ∫ 1 output(y 1 ) ∫ 2 output(y 2 ) [PO] ∫ 1 ⊗ ∫ 2 output(x 1 ⊗ x 2 )

Proceedings of the Posters Workshop at CSD&M 2013 ∫ 1 istate(q 1 ) ∫ 2 istate(q 2 ) [PS] ∫ 1 ⊗ ∫ 2 istate((q 1 , q 2 ))

Definition 18 (Composition of two systems). Let ∫ 1 = (T, X 1 , Y 1 , Q 1 , , , ) and ∫ 2 = (T, X 2 , Y 2 , Q 2 , , , ) be two systems such that Y 1 = X 2 . We note ∫ 2 • ∫ 1 the composition of ∫ 1 and ∫ 2 , obtained by "pluging" the output of ∫ 1 to the input of ∫ 2 .

Proposition 2 (Composition of two systems). Let ∫ 1 = (T 1 , X 1 , Y 1 , Q 1 , , , ) and ∫ 2 = (T 2 , X 2 , Y 2 , Q 2 , , , ) be two systems such that T 1 = T 2 and Y 1 = X 2 . Let (x, y, q 1 , q

2 ) ∈ X 1 × Y 2 × Q 1 × Q 2 ). ∫ 1 input(x) [WI] ∫ 2 • ∫ 1 input(x) ∫ 2 output(y) [WO] ∫ 2 • ∫ 1 output(y) ∫ 1 istate(q 1 )

∫ 2 istate(q 2 ) [WS] ∫ 2 • ∫ 1 istate((q 1 , q 2 ))

Conclusion

In this work we built a semantics of systems and provided a formal definition of "properties" as timed behaviour constraints. The next step is to build a more advanced refinement computation language that could let modelers obtain a system from a set of such constraints.