Clocks Model for Specification and Analysis of Timing in Real-Time Embedded Systems Iryna Zaretska1 , Galyna Zholtkevych1 , Grygoriy Zholtkevych1 and Frédéric Mallet2 1 V.N. Karazin Kharkiv National University, School of Mathematics and Mechanics, 4, Svobody Sqr., 61022, Kharkiv, Ukraine zar@univer.kharkov.ua,{galyna,g}.zholtkevych@gmail.com 2 Université Nice Sophia Antipolis, AOSTE Team Project (INRIA/I3S), INRIA Sophia Antipolis Méditerranée, 2004 rte des Lucioles (Lagrange L-043) BP93, F-06902 Sophia Antipolis Cedex, France frederic.mallet@unice.fr Abstract. Problems concerning formal semantics for Clock Constraint Specification Language (CCSL) are considered in the paper. CCSL is intended for describing logical time models for real-time embedded sys- tems and the language is a part of UML profile for MARTE. There exist two approaches to introduce a denotational semantics for CCSL. A pure relational subset of CCSL is defined in the paper. The notion of time structure with clocks is introduced to refine describing denotational se- mantics for this CCSL subset, which authors called RCCSL. Semantic properties of RCCSL have been studied. Theorem about coincidence se- mantics of RCCSL for the two approaches is proved. Keywords. Embedded system, real-time system, time modelling, time structure, clock constraint, formal specification Key terms. ConcurrentComputation, FormalMethod, SpecificationPro- cess, VerificationProcess, MathematicalModeling 1 Introduction Nowadays, the growth of using distributed real-time systems (including embed- ded systems) [4] is the developing trend for Information and Communication Technology. There are two reasons for such growth: first, the physical limit for processor acceleration is reached, and, second, using mobile and cloud technolo- gies are explosively expanded. The impossibility to continue over-clocking of a processor leads to using a multi-core system, which is parallel and distributed. A complex consisting of a computational cloud and an ensemble of mobile de- vices is a parallel and distributed system too. Moreover its structure is not fixed. 476 I. Zaretska, G. Zholtkevych, Gr. Zholtkevych and F. Mallet Each of the cases requires using different kinds of multiprocessing architectural and software solutions [3]. Therefore, providing correct working of such systems requires more research in the area. Mathematical modelling of systems makes possible to develop formal specifi- cations and methods of their analysis as a base for trustworthy system construct- ing. There are a lot of approaches to modelling multiprocessor systems. First of all, the following ones should be noticed: CSP of C.A.R. Hoare [8], π-calculus of R. Milner [11], abstract state machine model [5], and processing algebra [14]. This paper is devoted to formal methods for an important subclass of mul- tiprocessing distributed systems, namely, real-time embedded (RTE) systems. These methods are closely connected with the UML profile for MARTE (Mod- elling and Analysis of Real-Time and Embedded systems) [2, 15]. In the context of the MARTE approach UML [16, 17] is used to build engineering models of a developing system. But the UML notation does not support detailed description of interactions for joining components into a united RTE system. A very com- mon way to specify conditions for the system integrity is through the Object Constraint Language (OCL) [12]. However, no facilities for specifying temporal constraints are provided by the OCL standard. The Clock Constraint Specifica- tion Language (CCSL) [2] was defined in an annex of MARTE as a way to build logical and temporal constraints on model elements. CCSL is intended to describe the temporal ordering of interactions between components of a distributed software system. It focuses on the ordering of event occurrences, but not on their chronometric characteristics. It relies on a logical time model inspired by the work on synchronous systems and their polychronous extensions. The denotational semantics for basic constructions of CCSL is given in [10]. It is based on the notion of a time structure with clocks, other approach [1] defines an operational way to compute runs for CCSL specifications. The main contribution of this paper is a demonstration that the relationship of semantics consequence based on time structures as models of constraints and semantics consequence based on time structures associated with runs are only equivalent for a subset of CCSL, which we call RCCSL. 2 Syntax of Pure Relational CCSL In the paper we restrict ourself to a very simple sublanguage of CCSL, which we call the pure relational CCSL (RCCSL). Syntax of this subset is given here using EBNF [6]. clock constraint = clock relation, {’,’, clock relation}; clock relation = clock reference, sign of clock relation, clock reference; sign of clock relation = ’subclocking’ | Clocks Model for Specification and Analysis of Timing ... 477 ’exclusion’ | ’coincidence’ | ’cause’ | ’precedence’; clock reference = ? any element of clock set ?; Below we use the next notation for symbols of clock relations (see Table 1). Table 1. Symbols of clock relations Relation name Relation symbol subclocking ⊂ exclusion # coincidence = cause 4 precedence ≺ These five binary relations on a clock set C are determined as logical primi- tives for CCSL in [1]. Defining semantics for RCCSL is one of the paper objectives. Following the paper [10], we define the denotational meaning for a set of clock constraints as some class of time structures expanded by a classification for event occurrences. The next section is devoted to describing such structures. 3 Time Structure with Clocks Let consider a set of event occurrences, which is below denoted by I. Elements of the set I are called instants. Some pairs of instants denotes instant pairs, whose elements are ordered in time: i1 4 i2 is denoted the fact ”an instant i1 causes an instant i2 ” or equivalently ”an instant i1 cannot occur later than an instant i2 ”, where i1 , i2 ∈ I. This relation is called ’cause’. It is naturally to suppose that cause is a pre-order. As known [7, section 1.3], each pre-order can be decomposed uniquely into the union of two relations such that the former is a strict order (it is denoted bellow by ’≺’ and called a precedence) and the latter is an equivalence (it is denoted bellow by ’≡’ and called a coincidence). These relations are connected by the next property: for any instants i1 , i01 , i2 , i02 ∈ I the validity of i1 ≡ i01 , i2 ≡ i02 , and i1 ≺ i2 implies (1) truth of i01 ≺ i02 . 478 I. Zaretska, G. Zholtkevych, Gr. Zholtkevych and F. Mallet Moreover, if we have a strict order and an equivalence on the same set and these relations satisfy (1) then their union is a pre-order. Now, we can introduce the notion of a time structure for formalising our understanding a set of instants. Definition 1. Let (I, 4) be a pair of a set and a pre-order on this set respec- tively. Denote by ≺ the strict order corresponding to the pre-order 4. The pair (I, 4) is called a time structure if the next property (the property of cause finite- ness [13]) holds: the set {i0 ∈ I | i0 ≺ i} is finite for all i ∈ I. (2) Definition 1 is based on the corresponding definition in [10]. One can compare them with the definition of a time structure in [13]. Difference consists in a possibility of modelling an instant coincidence. Note that Definition 1 specifies the set of instants and some time relations on it but it does not determine any classification of instants in compliance with their sources. Therefore, in the following [2] we introduce such a classification by adding a finite set of instant sources called clocks and by mapping the set of instants into this clock set. Definition 2. Let (I, 4) be a time structure, C be a finite set of clocks, and π : I → C be a map then the quadruple (I, 4, C, π) is called a time structure with clocks if the next property holds: for any clock c ∈ C and i1 , i2 ∈ π −1 (c) the validity of i1 6= i2 implies truth of i1 ≺ i2 ∨ i2 ≺ i1 , (3) i.e. π −1 (c) is linearly ordered by the restriction of the cause. If c ∈ C then the set π −1 (c) is usually denoted by Ic . It can be considered as an event stream generated by the source associated with the clock c. From Definition 1 and Definition 2 the next fact follows immediately. Proposition 1. Let (I, 4, C, π) be a time structure with clocks then 1. Ic is well-ordered by the strict order ≺ for all c ∈ C; 2. ordinal type of Ic for any c ∈ C is less or equal to ω, where ω is the first infinite ordinal. Proof. Firstly note that property (3) implies linear ordering Ic for an arbitrary c ∈ C. Further, suppose that A is some non-empty subset of Ic for an arbitrary c ∈ C, i is some element of A. If for all i0 ∈ A the statement i ≺ i0 ∨ i = i0 is true then inf A = i ∈ A. If there exists i0 ∈ A such that i0 ≺ iTthen the set A(i) = {i0 ∈ A | i0 ≺ i} is not empty. It is evident that A(i) = A {i0 ∈ Ic | i0 ≺ i}. This equality and the property of cause finiteness (2) imply finiteness of A(i). So, taking into account Clocks Model for Specification and Analysis of Timing ... 479 property (3) we can conclude that A(i) is a finite linearly ordered set. Hence, there exists i∗ ∈ A(i) such that i∗ = inf A(i). It is evident that inf A = inf A(i) = i∗ ∈ A(i) ⊂ A. Thus, inf A ∈ A and Ic is well-ordered. The supposition that ordinal type of Ic for some c ∈ C is greater than ω is inconsistent with the property of cause finiteness (2). t u Corollary 1. Any instant i ∈ I is uniquely determined by the pair (π(i), idx(i)), which is an element of the set C × N. Here, idx is a map from I into N such that idx(i) = |{i0 ∈ Iπ(i) | i0 ≺ i}| + 1, where the number of elements in a set A is denoted by |A|. The designation TC is used below to refer to the class of time structures with C as a set of clocks. Remark 1. One can show that this class is a set but we do not do it in the paper. 4 Denotational Semantics for RCCSL Usually, a denotational semantics can be considered as the theory of models for the corresponding language. We shall use time structures with clocks as models for describing meaning of clock constraints. 4.1 Some General Notes One can identify a class of event occurrences of the same type with a set of instants for some clock in the process of specifying interactions between compo- nents of distributed parallel systems. Such an identification is provided by fixing a set of clocks C and describing rules of interacting system components. These rules divide the set TC into two subsets: the subset of time structures satisfying the constraints and the set of time structures contradicting them. Taking into account the specification of RCCSL one can say that a clock constraint is a finite set of clock relations. If the set of clock relations determining the constraint is denoted by C then the fact ”the time structure T ∈ TC satisfies the constraint C” can be written as T |= C. More precisely, T |= C means that for each C ∈ C the clause T |= C is true. Further, for a constraint C, JCK denote the following set {T ∈ TC | T |= C}. The first important problem is the consistency problem for the constraint. The rigorous problem formulation has usually the form: Problem 1 (Consistency Problem). For a constraint C check that the set JCK is not empty. 480 I. Zaretska, G. Zholtkevych, Gr. Zholtkevych and F. Mallet The second important problem is the semantic consequence for the constraints. The rigorous problem formulation has the next form: Problem 2 (Semantic Consequence Problem). For a constraint C and a clock relation r check that JCK ⊂ JrK (or in the another notation C r). Below we use the notation {C} for the set of clock relations that form the constraint C. It is easy to see that the next properties of the relationship are true. Proposition 2. The next properties are satisfied: 1. if a constraint C and a clock relation r satisfy the condition r ∈ {C} then C r; 2. if constraints C1 and C2 and a clock constraint r satisfy the next condition C1 r0 for all r0 ∈ {C2 } and C2 r are true then C1 r is true. Proof is omitted t u To complete defining the denotational semantics for RCCSL we should determine the meaning of basic clock relations. 4.2 Subclocking This relation is intended for specifying a requirement to synchronize each instant of one clock with some instant of an other clock. In this case the first clock is called a subclock of the second clock. More precisely, let c0 , c00 ∈ C and T ∈ TC then T |= c0 ⊂ c00 means that there exists a strict monotonic map h : Ic0 → Ic00 such that i ≡ h(i) for any i ∈ Ic0 . Proposition 3 (Trivial Subclocking). For each c ∈ C the clause c ⊂ c is true. Proof is trivial t u Proposition 4 (Transitivity Law for Subclocking). For each c0 , c00 , c000 ∈ C the clause c0 ⊂ c00 , c00 ⊂ c000 c0 ⊂ c000 is true. Proof. Let hc00 c0 : Ic0 → Ic00 , hc000 c00 : Ic00 → Ic000 be strict monotonic maps pro- viding the validity of the clauses T |= c0 ⊂ c00 and T |= c00 ⊂ c000 respectively for some T . It is easy to see that the map hc000 c00 ◦ hc00 c0 provides the validity of the clause T |= c0 ⊂ c000 t u 4.3 Exclusion This relation is used for specifying the mutual exclusion for two events. More formally, let c0 , c00 ∈ C and T ∈ TC then T |= c0 # c00 means that for any i0 ∈ Ic0 , i00 ∈ Ic00 the coincidence i0 ≡ i00 is false. Clocks Model for Specification and Analysis of Timing ... 481 Proposition 5 (Irreflexivity Law for Exclusion). For each c ∈ C the equal- ity Jc # cK = ∅ is true. Proof is trivial t u Proposition 6 (Symmetry Law for Exclusion). For each c0 , c00 ∈ C the clause c0 # c00 c00 # c0 is true. Proof is trivial t u 4.4 Coincidence This relation describes synchronization of two event sources. More precisely, let c0 , c00 ∈ C and T ∈ TC then T |= c0 = c00 means that there exists a strict monotonic bijection h : Ic0 → Ic00 such that i ≡ h(i) for any i ∈ Ic0 . Proposition 7 (Trivial Coincidence). For each c ∈ C the clause c = c is true. Proof is trivial t u Proposition 8 (Symmetry Law for Coincidence). For each c0 , c00 ∈ C the clause c0 = c00 c00 = c0 is true. Proof. Let h : Ic0 → Ic00 be a strict monotonic bijection providing the validity of the clause T |= c0 = c00 for some T and h−1 be its inverse map. Suppose that i0 , i00 ∈ Ic00 , i0 ≺ i00 , and h−1 (i0 ) 6≺ h−1 (i00 ) then either h−1 (i0 ) = h−1 (i00 ) or h−1 (i00 ) ≺ h−1 (i0 ). But the first alternative contradicts to bijectivity of h, and the second alternative and strict monotonicity of h implies i00 ≺ i0 . The last clause contradicts to irreflexivity of the precedence relation. These contra- dictions show that h−1 is a strict monotonic map. Further, for any i ∈ Ic00 we have that h−1 (i) ∈ Ic0 and h−1 (i) ≡ h(h−1 (i)) = i. Thus, the clause T |= c00 = c0 is true t u Proposition 9 (Transitivity Law for Coincidence). For each c0 , c00 , c000 ∈ C the clause c0 = c00 , c00 = c000 c0 = c000 is true. Proof is similar to proof of Proposition 4 t u 4.5 Cause This relation is intended for specifying that each instant of one clock is caused by an instant in another clock. More precisely, let c0 , c00 ∈ C and T ∈ TC then T |= c0 4 c00 means that there exists a strict monotonic map h : Ic00 → Ic0 such that h(i) 4 i for any i ∈ Ic00 . Proposition 10 (Trivial Cause). For each c ∈ C the clause c 4 c is true. 482 I. Zaretska, G. Zholtkevych, Gr. Zholtkevych and F. Mallet Proof is trivial t u Proposition 11 (Transitivity Law for Cause). For each c0 , c00 , c000 ∈ C the clause c0 4 c00 , c00 4 c000 c0 4 c000 is true. Proof is similar to proof of Proposition 4 t u 4.6 Precedence This relation is a stronger variant of the cause relation. Namely, let c0 , c00 ∈ C and T ∈ TC then T |= c0 ≺ c00 means that there exists a strict monotonic map h : Ic00 → Ic0 such that h(i) ≺ i for any i ∈ Ic00 . Proposition 12 (Irreflexivity Law for Precedence). For each c ∈ C the equality Jc ≺ cK = ∅ is true. Proof is trivial t u Proposition 13 (Transitivity Law for Precedence). For each c0 , c00 , c000 ∈ C the clause c0 ≺ c00 , c00 ≺ c000 c0 ≺ c000 is true. Proof is similar to proof of Proposition 4 t u 4.7 Interdependencies Laws for the Basic Relations Above we considered properties of each basic relation but interdependencies between these relations were not in our focus. Thus, such interdependencies are considered below. The next lemma is needed to ground these dependencies. Lemma 1. Let (X, ≤) be a well-ordered set and φ : X → X be a strict mono- tonic map such that for all x ∈ X the assertion φ(x) ≤ x is true then φ is the identity map. Proof. One can prove the lemma by using the transfinite induction t u Proposition 14 (Interdependencies Laws for the Basic Relations). 1. For each c0 , c00 ∈ C the clause c0 ⊂ c00 , c00 ⊂ c0 c0 = c00 is true. 2. For each c0 , c00 ∈ C the clock relations c0 ⊂ c00 and c0 # c00 are inconsistent, i.e. Jc0 ⊂ c00 , c0 # c00 K = ∅. 3. For each c0 , c00 ∈ C the clause c0 ⊂ c00 c00 4 c0 is true. 4. For each c0 , c00 ∈ C the clause c0 4 c00 , c00 4 c0 c0 = c00 is true. Proof. 1) For any T ∈ TC the validity of the assertion ”T |= c0 = c00 implies T |= c0 ⊂ c00 ” is evident. Let’s check the validity of the inverse assertion. Denote the strict monotonic maps that provide for some T ∈ TC the validity of T |= c0 ⊂ c00 and T |= c00 ⊂ c0 Clocks Model for Specification and Analysis of Timing ... 483 by hc00 c0 : Ic0 → Ic00 and hc0 c00 : Ic00 → Ic0 respectively. We claim that they are mutually inverse. Indeed, for any i ∈ Ic0 we have the next coincidences: i ≡ hc00 c0 (i) and hc00 c0 (i) ≡ hc0 c00 (hc00 c0 (i)). These coincidences and the Transitivity Law for Coincidence (see Proposition 9) provide the validity of the coincidence i ≡ hc0 c00 (hc00 c0 (i)). Taking into account that both i and hc0 c00 (hc00 c0 (i)) are elements of Ic0 and the fact that restriction of 4 on Ic0 is a strict order (see Proposition 1) one can derive the equality i = hc0 c00 (hc00 c0 (i)). The equality i = hc00 c0 (hc0 c00 (i)) for all i ∈ Ic00 is derived similarly. Thus, hc00 c0 is a bijection. 2) Proof is trivial. 3) Proof is trivial. 4) Really, let hc00 ,c0 : Ic0 → Ic00 and hc0 ,c00 : Ic00 → Ic0 be strict monotonic maps provided for some T ∈ TT the validity of the clauses T |= c00 4 c0 and T |= c0 4 c00 respectively. Then the map φ = hc0 ,c00 ◦ hc00 ,c0 : Ic0 → Ic0 is strict monotonic and it satisfies the condition φ(i) 4 i. Therefore, applying the Lemma 1 allows to conclude that φ and the identity map are equal t u 5 Runs and Chronometers Following [1], in this section we introduce the notion of a run for a set of clocks. We use this notion to define a behavioural model for the set of clocks. Definition 3 (see [1]). Let C be a finite set of clock then any map r : N → 2C such that r(t) = ∅ implies r(t0 ) = ∅ for all t0 > t is called a run for C. This definition means that if r is a run then at the (global) time t all clocks of the set r(t) and only them are triggered. For each run r one can construct a quadruple T [r] = (Ir , 4, C, πr ) by the following way: – Ir = {(c, t) ∈ C × N | c ∈ r(t)}; – (c0 , t0 ) 4 (c00 , t00 ) if and only if t0 ≤ t00 ; – πr (c, t) = c for all (c, t) ∈ Ir . Proposition 15. T [r] is a time structure with clocks for given run r. Proof. It is proved by trivial checking properties (2) and (3) t u Hence, we can define the semantic relationship between a run r and a constraint C by the next way: r |= C if and only if the clause T [r] |= C is true. Also, we can introduce the relationship C1 run C2 as an abbreviation of the sentence ”for any r such that r |= C1 the next relationship r |= C2 is valid”. Proposition 15 allows to suggest that a run carries more information than a time structure because a run depends on global time. A refinement and a substanti- ation of this hypothesis is discussed below. The notion of chronometer is introduced to specify dependences between time structures and runs. 484 I. Zaretska, G. Zholtkevych, Gr. Zholtkevych and F. Mallet Definition 4. Let T = (C, I, 4, π) be a time structure with clocks and χ : I → N be a map such that the next assertions are true: for any i0 , i00 ∈ I the coincidence i0 ≡ i00 implies χ(i0 ) = χ(i00 ) (4) for any i0 , i00 ∈ I the strict precedence i0 ≺ i00 implies χ(i0 ) < χ(i00 ) (5) 0 0 for any t, t ∈ N the validity of the clauses t ∈ χ(I) and t < t (6) implies truth of the clause t0 ∈ χ(I) then χ is called a chronometer on T [9]. Example 1. Let C be a finite set of clocks, r be a run for C. Then it is evident that the map χ∗ : Ir → N determined by the equality χ∗ (c, t) = t is a chronometer. Hence, Example 1 shows that each time structure generated by a run has a native chronometer χ∗ . Proposition 16. Let T be a time structure with clocks and χ : I → N be a chronometer then the map r[T , χ] : N → 2C defined by the next formula r[T , χ](t) = π(χ−1 (t)) (7) is a run. Proof. To prove the proposition we should show that r[T , χ](t) = ∅ for some t ∈ N implies r[T , χ](t0 ) = ∅ for any t0 ≥ t. Suppose existence of t1 and t2 such that t1 < t2 , π(χ−1 (t1 )) = ∅, but π(χ−1 (t2 )) 6= ∅. Taking into account this assumption one can derive that χ−1 (t1 ) = ∅ and χ−1 (t2 ) 6= ∅. Hence, t1 ∈/ χ(I) and t2 ∈ χ(I). We have obtained the contradic- tion to condition (6) of Definition 4 t u The next property for the chronometer χ∗ from Example 1 holds. Proposition 17. Let r be a run for a clock set C then the next equality holds r[T [r], χ∗ ] = r. (8) Let T = (C, I, 4, π) be a time structure with clocks and χ : I → N be a chronome- ter on T then the map χ b : I → C × N defined in the next way χ b(i) = (π(i), χ(i)) is a map onto Ir[T ,χ] such that any coincidence i0 ≡ i00 implies the coinci- dence χb(i0 ) ≡ χ b(i00 ) in T [r] and any precedence i0 ≺ i00 implies the precedence 0 00 b(i ) ≺ χ χ b(i ) in T [r]. Proof. Really, r[T [r], χ∗ ](t) = πr (χ−1 ∗ (t)) = πr ({(c, t) ∈ Ir }) = πr ({(c, t) ∈ C × N | c ∈ r(t)}) = r(t). Further, (c, t) ∈ Ir[T ,χ] if and only if c ∈ r[T , χ](t). It is easy to see that the last clause is equivalent to existence of i ∈ I such that c = π(i) and t = χ(i), i.e. it is equivalent to (c, t) = χ b(i). If i0 ≡ i00 then χ(i0 ) = χ(i00 ) by definition of a chronometer, hence χ b(i0 ) ≡ χ b(i00 ). 0 00 0 00 0 00 Similarly, if i ≺ i then χ(i ) < χ(i ), therefore χ b(i ) ≺ χ b(i ) t u Clocks Model for Specification and Analysis of Timing ... 485 Proposition 18. There exists only one chronometer on T [r] for any run r. Proof. For any run r there exists the chronometer χ∗ on T [r]. Let χ be an other chronometer on T [r]. For (c0 , t), (c00 , t) ∈ I[r] using (4) we have χ(c0 , t) = χ(c00 , t). Hence, taking into account Definition 3 one can obtain that χ(c, t) = τ (t) where τ is strict monotonic function from α into α for some cardinal α ≤ ω. Thus, τ is the identity function and χ = χ∗ t u Hence, a chronometer exists on a time structure associated with a run. We claim that a chronometer exists on any time structure with clocks. The next binary relation / on a time structure with clocks will be used for describing an algorithm that calculates timestamps for instants. More precisely, if i0 , i00 ∈ I then i0 / i00 means that for all i ∈ I the validity of the next clause i ≺ i00 & i0 4 i implies truth of the coincidence i ≡ i0 . It is easy seen that if i1 ≡ i01 , i2 ≡ i02 , and i1 / i2 then i01 / i02 . Now we can construct the algorithm that allows to calculate timestamps for instants on an arbitrary time structure with clocks. This Algorithm 1 is a generalization of Lamport’s algorithm [9]. Algorithm 1: Computing timestamp for an instant input : T = (C, I, 4, π) is a time structure with clocks, i is an element of I output: timestamp for the instant i 1 begin 2 count ← 1; D ← ∅; W ← ∅ ; // -- initializing work variables -- 3 while i ∈ / D do // -- main loop -------------------- 4 W+ ← {j ∈SI | j ∈ / D & idx(j) = count}; 5 W+ ← WS + / D & (∃j 0 ∈ W+ )j 0 ≡ j}; {j ∈ I | j ∈ 6 W ← W W+ ; 0 0 0 7 D+ ← {j S∈ W | (∀j ∈ I)(j / j ⇒ j ∈ D)}; 8 D ← D D+ ; 9 W ← W \ D+ ; 10 count ← count + 1; 11 end 12 return count; 13 end Theorem 1 (existence of a chronometer). Let T be a time structure with clocks and χ0 : I → N be the function calculated by Algorithm 1 then χ0 is a chronometer on T . Proof. One can see that Algorithm 1 builds two sequences of sets D0 ⊂ D1 ⊂ D2 ⊂ · · · ⊂ Dn ⊂ . . . W0 , W1 , W2 , . . . , Wn , . . . 486 I. Zaretska, G. Zholtkevych, Gr. Zholtkevych and F. Mallet in accordance to the following computational scheme:    W0 = ∅ D0 =∅  0 0 0 S  W n+1 = (WnS {j ∈ I | (∃j ∈ I)(j ≡ j & idx(j ) = n + 1)}) \ Dn 0 0 0  Dn+1 = Dn {j ∈ Wn+1 | (∀j ∈ I)(j / j ⇒ j ∈ Dn )}  and maps an instant i ∈ I into χ0 (i) = inf{n ∈ N | i ∈ Dn }. Firstly, note that supposition about partial definiteness of χ0 implies existence of an infinite sequence i1 . i2 . . . . . But it contradicts the causes finiteness property (2). Secondly, it is true by the construction of Dn that the validity of i0 ≡ i00 implies the truth of the following statement: i0 ∈ Dn if and only if i00 ∈ Dn . Hence, we obtain that i0 ≡ i00 implies χ0 (i0 ) = χ0 (i00 ). Further, similar reasoning provides the validity of the following statement: i0 ≺ i00 implies χ0 (i0 ) < χ0 (i00 ). Finally, the simple inequality idx(i) ≤ χ(i), which is correct for any i ∈ I and any chronometer χ on T , provides the validity of property (6) t u Corollary 2. There exists a chronometer on an arbitrary time structure with clocks. 6 Equivalence of Semantics for RCCSL Determined by Relations and run In the section the notion of a chronometer is used to prove the theorem about equivalence of the relationships and run . The theorem is the main result of the paper. Taking into account the theorem one can confine himself to checking semantic consequence by using runs. This opens a way to constructing an opera- tional semantics of RCCSL so that it is equivalent to the denotational semantics defined above. We need two lemmas to prove the main theorem. Let’s use the notation i1 k i2 for instants i1 and i2 such that i1 64 i2 & i2 64 i1 . Lemma 2. Let T = (C, I, 4, π) by a time structure with clocks and i1 , i2 be instants such that the clause i1 k i2 is true then there exists a chronometer χ on T satisfied the following condition χ(i1 ) < χ(i2 ). Proof. Let’s consider the quadruple T 0 = (C, I, 40 , π) such that i0 ≺0 i00 is valid if one of the next conditions is true 1. i0 = i1 and i00 = i2 ; 2. i0 ≺ i00 ; 3. i0 ≺ i1 and i2 ≺ i00 ; and i0 40 i00 if and only if i0 ≡ i00 or i0 ≺0 i00 . It is easy seen that the relation 40 is a pre-order. More over, it satisfies properties (2) and (3). Hence, T 0 is Clocks Model for Specification and Analysis of Timing ... 487 a time structure with clocks. Using Corollary 2 we obtain that there exists a chronometer χ on T 0 . But then χ is a chronometer on T and χ(i1 ) < χ(i2 ) is true t u Corollary 3. Let T = (C, I, 4, π) be a time structure with clocks, i0 , i00 ∈ I be instants, then 1. i0 ≺ i00 is valid if and only if for any chronometer χ on T the inequality χ(i0 ) < χ(i00 ) is true; 2. i0 ≡ i00 is valid if and only if for any chronometer χ on T the equality χ(i0 ) = χ(i00 ) is true. Lemma 3. Let T = (C, I, 4, π) be a time structure with clocks, ∗ be an arbi- trary sign of a clock relation, c0 and c00 be clocks then T |= c0 ∗ c00 if and only if r[T , χ] |= c0 ∗ c00 for any chronometer χ on T . Proof. It is evident that T |= c0 ∗ c00 implies r[T , χ] |= c0 ∗ c00 for any chronometer χ on T . Hence, we need to prove the inverse statement. 1) Suppose that r[T , χ] |= c0 ⊂ c00 for any chronometer χ on T . Then for any i ∈ Ic0 and for each chronometer χ there exists an instant iχ ∈ Ic00 such that χ(i) = χ(iχ ). Denote by X the set formed all iχ . It is a nonempty subset of Ic00 . Suppose that there exists at least two different elements in the set X. Let’s denote them by iχ1 and iχ2 . Taking in account linearity of the order on Ic0 and iχ1 6= iχ2 one can suppose that iχ1 ≺ iχ2 . Therefore χ1 (i) = χ1 (iχ1 ) < χ1 (iχ2 ). Thus, one of the two cases is realised: i ≺ iχ2 or i k iχ2 . But in the first case we obtain the inequality χ2 (i) < χ2 (iχ2 ), which contradicts to the choice of iχ2 . Hence, i k iχ2 is true. Similarly, one can obtain that i k iχ1 is true. Therefore, we proved that |X| > 1 implies i k iχ for all i ∈ Ic0 and any chronometer χ. Let i∗ = inf iχ then i k i∗ and χ(i∗ ) ≤ χ(iχ ) = χ(i). This is a contradic- χ∈X tion because Lemma 2 provides existence of some chronometer χ0 such that χ0 (i∗ ) > χ0 (i). Hence, X contains only one element, which we denote by h(i). By construction we have χ(i) = χ(h(i)) for any chronometer χ. The last prop- erty implies strict monotonicity of h and the coincidence i ≡ h(i). Therefore, T |= c0 ⊂ c00 . 2 and 3) Suppose that r[T , χ] |= c0 ∗ c00 for any chronometer χ on T then it is evident that T |= c0 ∗ c00 where ∗ equals to # or = . 4 and 5) Suppose that r[T , χ] |= c0 ∗ c00 for any chronometer χ on T where ∗ equals to 4 or ≺ . Similarly, in the first case one can derive that T |= c0 ∗ c00 is true t u Theorem 2 (about equivalence of semantics). Let C be an arbitrary finite set of clocks, C1 and C2 be RCCSL constraints then the C1 C2 is true if and only if C1 run C2 is true. Proof. One can easily see that the Theorem is the direct consequence of the Lemma 3 t u 488 I. Zaretska, G. Zholtkevych, Gr. Zholtkevych and F. Mallet 7 Conclusion In the paper we have considered the pure relational subset of CCSL (RCCSL) and have introduced semantics for it by using a class of mathematical objects called by authors time structures with clocks. We have studied semantic properties of RCCSL (see Propositions 3 – 9). We hope that these properties can be a background of an axiomatic basis for analysing relational clock constraints. Further we have introduced the notions ”a run” and ”a chronometer”. It allowed us to study interrelations between time structures and runs, to introduce the alternative semantics closer to the operational approach than the denotational semantics discussed earlier. Finally, the main theorem about equivalence of these two semantics (see Theo- rem 2) has been proved. We are planning to continue our research in the next areas: – building an axiomatic theory of the semantic consequence for RCCSL con- straints; – extending results on complete CCSL; – studying an operational semantics of CCSL and specifying its interrelations to the denotational semantics. References 1. André, C.: Syntax and Semantics of the Clock Constraint Specification Lan- guage (CCSL). Technical report, RR-6925, INRIA (2009), http://hal.inria.fr/inria- 00384077/en/ 2. André, C., Mallet, F., de Simone, R.: The Time Model of Logical Clocks available in the OMG MARTE profile. In: Shukla, S.K., Talpin, J.-P. (eds.) ”Synthesis of Em- bedded Software: Frameworks and Methodologies Correctness by Construction”, pp. 201–227. Springer Science+Business Media, LLC New York (2010) 3. Baer, J.-L.: Multiprocessing Systems. IEEE Trans. on Computers. 12, vol. C-25, 1271–1277 (1976) 4. Bonomi, F., Milito, R., Zhu, J., Addepalli, S.: Fog computing and its role in the internet of things. In: Proceedings of the first edition of the MCC workshop on Mobile cloud computing, pp. 13–16. ACM New York, NY, USA (2012) 5. Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, Berlin Heidelberg (2003) 6. Information technology – Syntactic metalanguage – Extended BNF. ISO/IEC 14977:1996(E) 7. Harzheim, E.: Ordered Sets. Springer Science+Business Media, Inc. New York (2005) 8. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International (1985) 9. Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Comm. ACM. 7, vol. 12, 558–565 (1978) 10. Mallet, F.: Logical Time @ Work for the Modeling and Analysis of Embedded Systems, Habilitation thesis. LAMBERT Academic Publishing (2011) Clocks Model for Specification and Analysis of Timing ... 489 11. Milner, R.: Communicating and Mobile Systems: The Pi Calculus. Cambridge Uni- versity Press, Cambridge (1999) 12. Information technology – Object Management Group – Object Constraint Lan- guage (OCL). ISO/IEC 19507:2012(E) 13. Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains. Theor. Comp. Sc. 1, vol. 13, 85–108 (1981) 14. Process Algebra for Parallel and Distributed Processing. Alexander, M., Gardner, W. (eds), CRC Press (2009) 15. UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Sys- tems. OMG (2011), http://www.omg.org/spec/MARTE/1.1/pdf/ 16. OMG Unified Modeling LanguageTM (OMG UML), Infrastructure. OMG (2011), http://www.omg.org/spec/UML/2.4.1/Infrastructure 17. OMG Unified Modeling LanguageTM (OMG UML), Superstructure. OMG (2011), http://www.omg.org/spec/UML/2.4.1/Superstructure