Problems concerning formal semantics for Clock Constraint Speci cation Language (CCSL) are considered in the paper. CCSL is intended for describing logical time models for real-time embedded systems and the language is a part of UML pro le for MARTE. There exist two approaches to introduce a denotational semantics for CCSL. A pure relational subset of CCSL is de ned in the paper. The notion of time structure with clocks is introduced to re ne describing denotational semantics for this CCSL subset, which authors called RCCSL. Semantic properties of RCCSL have been studied. Theorem about coincidence semantics of RCCSL for the two approaches is proved.
Nowadays, the growth of using distributed real-time systems (including
embedded systems) [
Mathematical modelling of systems makes possible to develop formal speci
cations and methods of their analysis as a base for trustworthy system
constructing. 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 [
This paper is devoted to formal methods for an important subclass of
multiprocessing distributed systems, namely, real-time embedded (RTE) systems.
These methods are closely connected with the UML pro le for MARTE
(Modelling and Analysis of Real-Time and Embedded systems) [
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 [
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 [
clock constraint =
clock relation, {',', clock relation}; clock relation =
clock reference, sign of clock relation, clock reference; sign of clock relation = 'subclocking' | '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).
These ve binary relations on a clock set C are determined as logical
primitives for CCSL in [
De ning semantics for RCCSL is one of the paper objectives. Following the
paper [
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 2 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 2 I the validity of i1 i01, i2 i02, and i1 truth of i01 i02. i2 implies (1) 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.
De nition 1. Let (I; 4) be a pair of a set and a pre-order on this set
respectively. 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
niteness [
(2)
De nition 1 is based on the corresponding de nition in [
Note that De nition 1 speci es the set of instants and some time relations
on it but it does not determine any classi cation of instants in compliance with
their sources. Therefore, in the following [
De nition 2. Let (I; 4) be a time structure, C be a nite 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 2 C and i1; i2 2 1(c) the validity of i1 6= i2 implies truth of i1 i2 _ i2 i1, i.e. 1(c) is linearly ordered by the restriction of the cause. (3) If c 2 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 De nition 1 and De nition 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 2 C; 2. ordinal type of Ic for any c 2 C is less or equal to !, where ! is the rst in nite ordinal.
Proof. Firstly note that property (3) implies linear ordering Ic for an arbitrary c 2 C.
Further, suppose that A is some non-empty subset of Ic for an arbitrary c 2 C, i is some element of A.
If for all i0 2 A the statement i i0 _ i = i0 is true then inf A = i 2 A. If there exists i0 2 A such that i0 i then the set A(i) = fi0 2 A j i0 ig is not empty. It is evident that A(i) = A Tfi0 2 Ic j i0 ig. This equality and the property of cause niteness (2) imply niteness of A(i). So, taking into account property (3) we can conclude that A(i) is a nite linearly ordered set. Hence, there exists i 2 A(i) such that i = inf A(i). It is evident that inf A = inf A(i) = i 2 A(i)
A: Thus, inf A 2 A and Ic is well-ordered.
The supposition that ordinal type of Ic for some c 2 C is greater than ! is inconsistent with the property of cause niteness (2). tu Corollary 1. Any instant i 2 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) = jfi0 2 I (i) j i0 igj + 1; where the number of elements in a set A is denoted by jAj.
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
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
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 components of distributed parallel systems. Such an identi cation is provided by xing 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 speci cation of RCCSL one can say that a clock constraint is a nite set of clock relations. If the set of clock relations determining the constraint is denoted by C then the fact "the time structure T 2 TC satis es the constraint C" can be written as T j= C. More precisely, T j= C means that for each C 2 C the clause T j= C is true.
Further, for a constraint C, JCK denote the following set fT 2 TC j T j= Cg.
The rst 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. 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 fCg 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 satis ed: 1. if a constraint C and a clock relation r satisfy the condition r 2 fCg then
C r; 2. if constraints C1 and C2 and a clock constraint r satisfy the next condition
C1 r0 for all r0 2 fC2g and C2 r are true then C1 r is true. Proof is omitted tu To complete de ning the denotational semantics for RCCSL we should determine the meaning of basic clock relations. 4.2
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 rst clock is called a subclock of the second clock.
More precisely, let c0; c00 2 C and T 2 TC then T j= c0 c00 means that there exists a strict monotonic map h : Ic0 ! Ic00 such that i h(i) for any
true. c c is tu
the clause c0 c00; c00 c000 c0 c000 is true.
Proof. Let hc00 c0 : Ic0 ! Ic00 , hc000 c00 : Ic00 ! Ic000 be strict monotonic maps providing the validity of the clauses T j= c0 c00 and T j= 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 j= c0 c000 tu 4.3
any i0 2 Ic0 , i00 2 Ic00 the coincidence i0 This relation is used for specifying the mutual exclusion for two events.
More formally, let c0; c00 2 C and T 2 TC then T j= c0 # c00 means that for i00 is false.
ity Jc # cK = ; is true. Proof is trivial
clause c0 # c00 c00 # c0 is true.
true. c = c is
clause c0 = c00 c00 = c0 is true.
Proof. Let h : Ic0 ! Ic00 be a strict monotonic bijection providing the validity of the clause T j= c0 = c00 for some T and h 1 be its inverse map. Suppose that i0; i00 2 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 rst alternative contradicts to bijectivity of h, and the second alternative and strict monotonicity of h implies i00 i0. The last clause contradicts to irre exivity of the precedence relation. These contradictions show that h 1 is a strict monotonic map.
Further, for any i 2 Ic00 we have that h 1(i) 2 Ic0 and h 1(i) h(h 1(i)) = i. Thus, the clause T j= c00 = c0 is true tu
the clause c0 = c00; c00 = c000 c0 = c000 is true. tu tu tu tu Proof is similar to proof of Proposition 4 4.5
i 2 Ic00 .
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 2 C and T 2 TC then T j= c0 4 c00 means that there exists a strict monotonic map h : Ic00 ! Ic0 such that h(i) 4 i for any
c 4 c is true. Proof is trivial Proposition 11 (Transitivity Law for Cause). For each c0; c00; c000 2 C the clause c0 4 c00; c00 4 c000 c0 4 c000 is true. tu tu tu tu tu This relation is a stronger variant of the cause relation.
Namely, let c0; c00 2 C and T 2 TC then T j= c0 c00 means that there exists a strict monotonic map h : Ic00 ! Ic0 such that h(i) i for any i 2 Ic00 .
equality Jc cK = ; is true. Proof is trivial
c0; c00; c000 2 C the clause c0 c00; c00 Law c000 for c0
c000 is true.
Proof is similar to proof of Proposition 4 For each 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 monotonic map such that for all x 2 X the assertion (x) x is true then is the identity map.
Proof. One can prove the lemma by using the trans nite induction Proposition 14 (Interdependencies Laws for the Basic Relations). 1. For each c0; c00 2 C the clause c0 2. For each c0; c00 2 C the clock relations c0 i.e. Jc0
c00; c0 # c00K = ;. 3. For each c0; c00 2 C the clause c0 c00; c00 c0
c0 = c00 is true.
c00 and c0 # c00 are inconsistent, c00 c00 4 c0 is true. 4. For each c0; c00 2 C the clause c0 4 c00; c00 4 c0 c0 = c00 is true.
Proof. 1) For any T 2 TC the validity of the assertion "T j= c0 = c00 implies T j= c0 c00" is evident.
Let's check the validity of the inverse assertion. Denote the strict monotonic maps that provide for some T 2 TC the validity of T j= c0 c00 and T j= c00 c0 by hc00 c0 : Ic0 ! Ic00 and hc0 c00 : Ic00 ! Ic0 respectively. We claim that they are mutually inverse.
Indeed, for any i 2 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 2 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 2 TT the validity of the clauses T j= c00 4 c0 and T j= c0 4 c00 respectively. Then the map = hc0;c00 hc00;c0 : Ic0 ! Ic0 is strict monotonic and it satis es the condition (i) 4 i. Therefore, applying the Lemma 1 allows to conclude that and the identity map are equal tu 5
Following [
For each run r one can construct a quadruple T [r] = (Ir; 4; C; r) by the following way: { Ir = f(c; t) 2 C N j c 2 r(t)g; { (c0; t0) 4 (c00; t00) if and only if t0 { r(c; t) = c for all (c; t) 2 Ir.
t00; 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) tu Hence, we can de ne the semantic relationship between a run r and a constraint C by the next way: r j= C if and only if the clause T [r] j= C is true. Also, we can introduce the relationship C1 run C2 as an abbreviation of the sentence "for any r such that r j= C1 the next relationship r j= 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 re nement and a substantiation of this hypothesis is discussed below.
The notion of chronometer is introduced to specify dependences between time structures and runs. De nition 4. Let T = (C; I; 4; ) be a time structure with clocks and be a map such that the next assertions are true: : I ! N for any i0; i00 2 I the coincidence i0 for any i0; i00 2 I the strict precedence i0 for any t; t0 2 N the validity of the clauses t 2 implies truth of the clause t0 2 (I) i00 implies (i0) =
(i00) i00 implies (i0) <
(i00) (I) and t0 < t then
is called a chronometer on T [
Example 1. Let C be a nite 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 de ned by the next formula r[T ; ](t) = ( 1(t)) is a run.
Proof. To prove the proposition we should show that r[T ; ](t) = ; for some t 2 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 2= (I) and t2 2 (I). We have obtained the contradiction to condition (6) of De nition 4 tu 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]; Let T = (C; I; 4; ) be a time structure with clocks and : I ! N be a chronometer on T then the map b : I ! C N de ned in the next way b(i) = ( (i); (i)) is a map onto Ir[T ; ] such that any coincidence i0 i00 implies the coincidence b(i0) b(i00) in T [r] and any precedence i0 i00 implies the precedence b(i0) b(i00) in T [r].
Proof. Really, r[T [r]; ](t) = r(
1(t)) = r(f(c; t) 2 Irg) = r(f(c; t) 2 C
N j c 2 r(t)g) = r(t): Further, (c; t) 2 Ir[T ; ] if and only if c 2 r[T ; ](t). It is easy to see that the last clause is equivalent to existence of i 2 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 de nition of a chronometer, hence b(i0) b(i00). Similarly, if i0 i00 then (i0) < (i00), therefore b(i0) b(i00) tu (4) (5) (6) (7) (8) 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) 2 I[r] using (4) we have (c0; t) = (c00; t). Hence, taking into account De nition 3 one can obtain that (c; t) = (t) where is strict monotonic function from into for some cardinal !. Thus, is the identity function and = tu 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 2 I then i0 / i00 means that for all i 2 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 [
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
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; : : : in accordance to the following computational scheme: 8> W0 = ; >< D0 = ; > Wn+1 = (Wn Sfj 2 I j (9j0 2 I)(j0 j & idx(j0) = n + 1)g) n Dn >: Dn+1 = Dn Sfj 2 Wn+1 j (8j0 2 I)(j0 / j ) j0 2 Dn)g and maps an instant i 2 I into 0(i) = inffn 2 N j i 2 Dng.
Firstly, note that supposition about partial de niteness of 0 implies existence of an in nite sequence i1 . i2 . : : : . But it contradicts the causes niteness 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 2 Dn if and only if i00 2 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 2 I and any chronometer on T , provides the validity of property (6) tu Corollary 2. There exists a chronometer on an arbitrary time structure with clocks. 6
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 con ne himself to checking semantic consequence by using runs. This opens a way to constructing an operational semantics of RCCSL so that it is equivalent to the denotational semantics de ned 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 satis ed 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 satis es properties (2) and (3). Hence, T 0 is 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 tu Corollary 3. Let T = (C; I; 4; ) be a time structure with clocks, i0; i00 2 I be instants, then Lemma 3. Let T = (C; I; 4; ) be a time structure with clocks, trary sign of a clock relation, c0 and c00 be clocks then T j= c0 if r[T ; ] j= c0 c00 for any chronometer on T . Proof. It is evident that T j= c0 c00 implies r[T ; ] j= c0 c00 for any chronometer on T . Hence, we need to prove the inverse statement. 1) Suppose that r[T ; ] j= c0 c00 for any chronometer on T . Then for any i 2 Ic0 and for each chronometer there exists an instant i 2 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 di erent 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 rst 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 jXj > 1 implies i k i for all i 2 Ic0 and any chronometer . Let i = inf i then i k i and (i ) (i ) = (i). This is a contradic2X 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 property implies strict monotonicity of h and the coincidence i h(i). Therefore, T j= c0 c00. 2 and 3) Suppose that r[T ; ] j= c0 c00 for any chronometer on T then it is evident that T j= c0 c00 where
equals to # or = . 4 and 5) Suppose that r[T ; ] j= c0 c00 for any chronometer on T where equals to 4 or . Similarly, in the rst case one can derive that T j= c0 is true
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 c00 tu
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 Theorem 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 constraints; { extending results on complete CCSL; { studying an operational semantics of CCSL and specifying its interrelations to the denotational semantics.