Embedded System Design is becoming a eld of choice for Model-Driven Engineering techniques. On the engineering side, models bring an abstraction of the code that can then be generated (and regenerated) at will. On the semantic side, they bring a reasoning framework to guarantee or verify properties on the generated code. We focus here on the Clock Constraint Speci cation Language, initially de ned as a companion language of the uml Pro le for marte. More speci cally, we de ne a state-based representation of ccsl operators. To deal with unbounded operators, we propose to use lazy evaluation to represent intentionally in nite transition systems. We provide an algorithm to make the synchronized product of such transition systems and we study its complexity. Even though the transition systems are in nite, the result of the composition may become nite, in which case the (semi)algorithm terminates and exhaustive analysis becomes possible.
not necessarily regular in physical time (as the usual meaning suggest). Some
of the essence of multiform logical time was captured and encapsulated into a
dedicated language called the Clock Constraint Speci cation Language (ccsl)
[
ccsl has arisen from di erent models in an attempt to abstract away the
data and the algorithm and to focus on events and control. Even though ccsl
was initially de ned as the time model of the uml pro le for marte, it has now
become a full edged domain-speci c modeling language for capturing
chronological, causal and timed relationships and is now developed independently. It
combines constructs from the general net theory and from the synchronous
languages [
Until then, the clock calculus on ccsl speci cation was performed step by
step up to a prede ned number of steps. This work is an attempt to support
exhaustive analysis of ccsl speci cation. When ccsl operators are represented
as transition systems, their composition is the synchronized product of the
transition systems. However, this causes termination problems when the transition
systems have an in nite number of states. In this paper, an algorithm for the
parallel execution of automata representing ccsl operators is proposed. It has
been implemented in a prototype tool. This algorithm supports ccsl unbounded
operators. The in nite data structure is unfolded on demand using a lazy
evaluation technique. This is a signi cant evolution on previous veri cation techniques
for ccsl [
The main contribution is to propose an encoding based on lazy evaluation to represent ccsl unbounded operators. The second contribution is to propose an algorithm to build the synchronized product of such automata. The (semi)algorithm terminates when the composition of unbounded automata becomes bounded.
In this work, the main operators of the clock constraint language were considered. For each basic expression and each relations of the kernel language, a transition system is proposed. Each transition is labeled by the set of clocks that must tick for the transition to be taken. Clocks can stall, tick or be dead. When a clock is dead, it cannot tick anymore. A path in the automaton is then an in nite word on the alphabet of powersets of clock names.
The automata representing the unbounded ccsl operators consist of an innite number of states and therefore transitions (even though each state has a nite number of outgoing transitions). For those operators, the lazy evaluation technique was applied. It allows postponing the construction of the state of an unbounded automaton to the moment when it is actually needed. In very frequent cases, the speci cation becomes bounded and the intentional in nite representation is never actually expanded.
On these transition systems, we apply the classical synchronized product
of transition systems [
3.1
The formalism of timed automata [
To answer the question if this formalism can be applied for representation of the ccsl language basic constructions, the de nition of a clock in ccsl time model must be considered. In terms of ccsl time model a clock is a set of ordered instants. Each clock has a lifetime limited by birth and death instants. Formally, a Clock c is a tuple (Ic; c; c"; c#; c#) where Ic is a sequence of instants (it can be in nite), c"; c# are birth and death instants respectively such that Ic \ fc"; c#g = , c# is a coincidence relation and c is an order relation on Ic [ fc "; c #g. All instants of clocks are strictly ordered, the birth instant precedes all the other instants of the clock and every instant precedes the death. If the set of instants Ic is in nite then the death instant is not necessary. Ic represents the occurrences or ticks of the clock c.
Thus we can see that the notions of clock in the terms of timed automata formal model and the clock constraint speci cation language are radically different. Timed Automata, clocks captured physical real-valued time properties, whose value is within a dense time interval. All time clocks evolve at the same rate (without drift). In ccsl, clocks represent logical time properties. The unbounded nature precisely comes from the relative (unbounded) drifts between the clocks that evolve at their own independent rhythm.
Synchronous Data Flow (SDF) [
Safety analysis on SDF graphs is a way to determine whether the system remains bounded or not. Such techniques could be used to study boundness issues for ccsl speci cations. However, this is not the concern of this paper. We assume that the composition is bounded and propose an algorithm to build the synchronized product. 3.3
When ccsl operators are expressed as transition systems, their parallel
composition simply is the synchronized product of the transition systems [
The Clock Constraint Speci cation Language
This section brie y introduces the logical time model of the Clock Constraint
Speci cation Language (ccsl). A technical report [
A clock c is a totally ordered set of instants, Ic. In the following, i and j are instants. A time structure is a set of clocks C and a set of relations on instants I = Sc2C IC . ccsl considers two kinds of relations: causal and temporal ones. The basic causal relation is causality/dependency, a binary relation on I :4 I I. i 4 j means i causes j or j depends on i. 4 is a pre-order on I, i.e., it is re exive and transitive. The basic temporal relations are precedence ( ), coincidence ( ), and exclusion (#), three binary relations on I. For any pair of instants (i; j) 2 I I in a time structure, i j means that the only acceptable execution traces are those where i occurs strictly before j (i precedes j). is transitive and asymmetric (re exive and asymmetric). i j imposes instants i and j to be coincident, i.e., they must occur at the same execution step, both of them or none of them. is an equivalence relation, i.e., it is re exive, symmetric and transitive. i # j forbids the coincidence of the two instants, i.e., they cannot occur at the same execution step. # is irre exive and symmetric. A consistency rule is enforced between causal and temporal relations. i 4 j can be re ned either as i j or i j, but j can never precede i. We consider here discrete sets of instants only, so that the instants of a clock can be indexed by natural numbers. For a clock c 2 C, and for any k 2 N>0, c[k] denotes the kth instant of c.
Specifying a full time structure using only instant relations is not realistic since clocks are usually in nite sets of instants. Thus, an enumerative speci cation of instant relations is forbidden. The Clock Constraint Speci cation Language (ccsl) de nes a set of time patterns between clocks that apply to in nitely many instant relations. 4.1
Coincidence According to the considered relation the clocks a and b always tick simultaneously (a = b), it is de ned as (8k 2 N?)(a[k] b[k]). Subclocking a b de nes a as being a subclock of its superclock b. Every instant of the subclock occurs synchronously with one of the instants of the superclock: (8k 2 N?)(9i 2 N?)(a[k] b[i]). Exclusion a # b. The clocks connected with this relation cannot have coincidence instants: (8k 2 N?)(8i 2 N?)(a[k] # b[i]).
Precedence a b is the index-dependent relation. This operator is unbounded. Every instant of clock a has to precede the instant of clock b with the same index (8k 2 N?)(a[k] b[k]).
Strict Precedence a b. This relation is a severer version of the previous one in the sense that the instants of the clocks a, b with the same indices cannot be equal: (8k 2 N?)(a[k] 4 b[k]). 4.2
A ccsl speci cation consists of clock declarations and conjunctions of clock relations between clock expressions. A clock expression de nes a set of new clocks from existing ones. Most expressions deterministically de ne one single clock. Table 2 gives a list of the ccsl kernel expressions. E10 Preemption (UpTo)
Synchronous
Synchronous Sampling a 7! b. The sampling expression ticks in coincidence with the tick of the base clock immediately following a tick of the trigger clock and after it dies. In the considered case, the trigger clock is b and the base clock is a. The textual syntax of this expression is represented as c = a sampling b. In Figure 1 the automaton is given, where input symbol c is equal to the result clock of the expression. The notation fa; b; cg denotes that the automaton remains in state s2 if a, b and c tick all together simultaneously. if b and c tick simultaneously without a then, the automaton goes back to state s1. If a ticks alone, it stays in s2. All other cases are forbidden by the semantics of the operator. fbg s1 fag fag s2 Strict Sampling a ! b. The expression is a strict version of the previous one where c is emitted when the automaton is in state s1, and a and b tick simultaneously.
Waiting a fn b. The resulting clock ticks only once after a special number given as a parameter of the base clock, and then the resulting clock dies. c = a wait n b, where n is a given parameter (it is a natural number). Preemption (UpTo) a b. The resulting clock ticks in coincidence with a, it dies as soon as b starts to tick: c = a upto b.
Union This expression is non-terminating and index-independent. Its result is a clock with set of instants which is a union of the instants sets of the clocksparameters that participate in the expression: c = a + b.
Intersection The result of this index-independent expression is the clock which ticks each time when the clocks-parameters tick simultaneously: c = a b. Concatenation a b . The expression is terminating. The resulting clock ticks in coincidence with the rst clock-parameter a. After death of a it starts to tick in coincidence with the second clock-parameter b . It should be noted that this expression is valid only if the rst clock eventually dies, i.e. a # is speci ed. Defer (Delay) a ( ns ) b. The parameter of the expression are a (the base clock), b (the delay clock) and ns that represents a sequence of elements from N>0. The sequence of the natural numbers can have an in nite part. Let ns[i] be the ith element of the sequence. We assume that if i > 0 then ns has an in nite part, if 0 6 i < p there are p elements in the sequence. Every tick of the base clock starts up the counter for respective element of the sequence. For every tick of the delay clock the relative counter is decreased. When the counter reaches 1 the respective instant of clock b occurs. The textual form of the expression is c = a def erred b f or ns.
Sup a _ b. The expression is index-dependent. The expression a _ b de nes a clock that is slower than both a and b and whose kth tick is coincident with the later of the kth ticks of a and b. The formal de nition is presented as: (a 4 (a _ b))(b 4 (a _ b))(8c 2 C) : (a 4 c)&(b 4 c) ) ((a _ b) 4 c). This is a typical example of unbounded transition system (with an in nite number of states). fbg fbg fag fag Inf a ^ b. This is index-dependent and unbounded. It is the dual of the previous one. The result of the expression is the slowest of faster clocks. It means that the de ned clock is faster than both a and b , the kth tick of this clock occurs in coincidence with the earlier of the kth ticks of both a and b. ((a ^ b) 4 a)((a ^ b) 4 b)(8c 2 C) : (c 4 a)&(c 4 b) ) (c 4 (a ^ b)) is the formal de nition. 4.3
Lazy evaluation or call-by-needed is an evaluation strategy that delays the evaluation of an expression until its value is actually needed. This approach allows construction of potentially in nite data structures and avoids repeated evaluations. To construct the algorithm of the parallel execution of several automata, it is necessary to have the possibility to work with in nite data structures (transition systems with an in nite number of states). Lazy evaluation provides the apparatus for this task. The ccsl has four basic unbounded operators which can be represented as in nite automata: the precedence relation, the strict precedence relation, the inf expression (the fastest of slower clocks) and the sup expression (the slowest of faster clocks).
Example 1. Let us consider as an example the automaton for the strict precedence relation (Fig. 3).
If we only consider the possible outgoing transitions of each state, we can distinguish the initial state (0 on Fig. 3) from the other ones. In the initial state, only a can tick and must tick alone. In the other states, if a ticks alone, we must progress to the right (increasing an unbounded counter), if b ticks alone, we must go back to the left (decreasing the counter). If a and b tick simultaneously, we remain in the same state. We assume that each state has a default transition to itself, when nothing happens. 5
We assume that the input for the algorithm is a given nite set of automata; each of them can be either nite or in nite. The output is the automaton that is the composition of the input ones. We denote the resulting automaton through the tuple R. Let us introduce the set St which is the set of all unconsidered states of the resulting automaton. At the beginning of the algorithm execution, the initial states of input automata are considered as the current ones. The rst unconsidered state of the resulting automaton is the state formed from current ones. For each considered current state of input automata the set of available transitions from the given state is calculated. For all input symbols of each of the calculated transitions the consistent solution is computed, which is the set such that every original symbol is its subset. If the solution exists, the new state is calculated from the states of input automata, in which we can go on the appropriate input symbols that are the subset of the found solution. If the computed new state does not belong to St, it is added to the set of unconsidered states. The resulting automaton is completed by the new state and the appropriate transition, which has the input symbol that is equal to the respective solution. If the solution cannot be found, then we take a state from St, in the input automata the appropriate states are considered as current. The process is repeated while the set St is not empty. 5.1
We introduce the formal de nitions that are used to describe the algorithm. C is the ( nite) set of clocks and |C| is its cardinality; state : C ! StateDomain = fST ALL; T ICK; DEADg that denotes the state of a clock.
A = fAig: the ordered set of input automata for the composition. Ai = (Ci; Si; Ii; moveOni; si0 2 Si; curi 2 Si; availT ransi), where Ci C: the ordered set of clocks of the ith automaton; Si: the set of states of the ith automaton; si0 2 Si: the initial state of the automaton; moveOni : Si 2Ci ! Si is the transition function; curi 2 Si: the current considered state; availT ransi : Si ! 22Ci : gives a set of available con gurations for a given state.
The resulting composite automaton can be de ned as follows: R = (C; SR; moveOnR; s0R 2 SR; curR 2 SR; availT ransR), such that: C: the set of clocks of the composite automaton is equal to the set of global clocks; SR = fsR : sR = (s1; :::; sjAj); si 2 Si; 8i = 1:::jAjg: each element of the set of states of the resulting automaton consists of the states of input automata; the element of the considered composite state corresponds to the automaton with the same number; moveOnR : SR 2C ! SR is the transition function for the resulting automaton; s0R 2 SR: the initial state; curR 2 SR: the current considered state; availT ransR : SR ! 22C : this function returns the set of input symbols for the available transitions of the composite automaton.
The set of found solutions is represented by the set SOL = fsol : sol = (st1; : : : ; stjCj); sti 2 fST ALL; T ICK; DEADg; 8i = 1:::jCjg.
St = fsR : sR 2 SRg is the set of considered states of the resulting automaton.
Get : Set ! element; element 2 Set: the function that returns an element of the given set.
Register : C f1::jAjg ! 2C . This function returns an input symbol for the ith automaton based on the states of the global set clocks.
index : 2C C ! N, the position of a clock in an ordered set of clocks. 5.2
Global variables. indexTable:=0: indexTable 2 N; array StateDomain temp[]: 8i 2 f0, ..., |C|-1g, temp[i] 2 StateDomain; array StateDomain cur_sol[]: 8i 2 f0, ..., |C|-1g, cur_sol[i] 2 StateDomain; array StateDomain OptionsTable[][]: 8j 2 f0, ..., |C|-1g, 8i 2 f0, ..., 3jCj-1g,
OptionsTable[i][j] 2 StateDomain; array Boolean SolutionsTable[][]: 8j 2 f0, ..., |A|-1g, 8i 2 f0, ..., 3jCj-1g,
SolutionsTable[i][j] 2 ftrue, falseg; cur_solution 2 SOL new stR 2 SR
The main purpose of the following function is to build the composite automaton from the given set of the input ones. It uses three other functions: buildSolutions(), getSolutions() and buildOptionsTable(). function composition()f
// the initial state is the cartesian product of all the initial states 1. s0R := s00 ... sj0Aj 1; St:=fs0Rg; 3. while(St6= ;)f 4. curR:=GetElement(N);
SOL:=buildSolution(curR); while(SOL6= )f //for each solution
cur_solution:=Get(SOL); 5. 6. 7. 10. 11. 12. 13. 14. 15.
The following function calculates the set of possible solutions. It builds a table of all options (OptionsTable) for the states of the clocks. The number of rows of this table is equal to 3jCj . The base is equal to three because all three possible states are considered (ST ALL, T ICK, DEAD). The number of columns is equal to the number of the clocks in the global set. Also, the table for nding solutions is de ned (SolutionsTable). The number of rows is equal to 3jCj, the number of columns corresponds to the number of input automata. If the input set de ned in a row of OptionsTable is available for the input automaton, then the value of an element of SolutionsTable situated in the same row as the input set is set the value true. When the SolutionsTable is completed (all available input symbols of input automata have been considered), the function getSolutions() is invoked to nd the set of solutions SOL using the data of SolutionsTable. function buildSolutions(sR)f 20. buildOptionTable(0); //Initially there are no solutions for(r:=0; r<3jCj; r:=r+1)f
for(i:=0; i<|A|; i:=i+1)f SolutionsTable[r][i]:=false; g 24. for(i:=0; i<|A|; i:=i+1)f // receiving the set of input sets for all available transitions // of the current state of the appropriate ith // automaton n is a number of available transitions 25. Iin := availT ransi(sR[i]); //assignment of the value true to an element of SolutionTable
for(k:=0; k<n; k:=k+1)f setMark(Iik) g // if at least one value in the row of table is equal to false // (it means that the given input set is not available for one // of automata) then the corresponding row of OptionsTable // cannot be considered as solution if(SolutionsTable[r][i]==false) f isSolution:=false; g if(isSolution)f for(k:=0; k<|C|; k:=k+1)f
cur_sol[k]:=OptionsTable[r][k]; g
SOL:=SOL [ cur_sol; g g return SOL;
The function of building the table for all possible options (OptionsTable).
The following function assigns the value true to an element of SolutionsTable. The element corresponds to the current considered input set de ned in the table OptionsTable function setMark(Iik)f 55. for(r:=0; r<3jCj; r:=r+1)f 56. boolean isDifferent:=false; 57. for(p:=0; p<|Ii|; p:=p+1)f 58. if(OptionsTable[r][index(Iik[p])]6= Iik[p])f 59. isDifferent:=true; 60. g 61. g 62. if(!isDifferent)f 63. SolutionsTable[r][i]:=true; 64. g 65. g g 5.3
To determine the complexity of the composition algorithm, it is necessary to determine the time complexity of each of the used functions. Let us consider the function buildOptionsTable() (lines 42-54). This function is recursive. The recursion depth is determined by the number of clocks in the global set. Thus, the time complexity is equal to 3jCj .
The function getSolutions() has two nested loops. The outer loop (lines 3040) goes over all rows of the solution table. The number of iterations is equal to 3jCj . The nested loop (lines 32-39) is designed to examine the marked input sets placed in the same row of the corresponding table. Since the number of elements in the row is equal to the number of automata, the number of iterations is jAj. The complexity of the function given by the product is de ned as 3jCj jAj.
The setMark() function is represented by two loops. The number of iterations of the outer (lines 55-65) is equal to 3jCj. The number of iterations of the inner loop (lines 57-60) is determined by the number of elements in the input set of the considered automaton. Because it is equal to the number of clocks involved in the execution of the relevant automaton, the number of repetitions is equal to jCij.
We de ne the complexity of the function for building the set of solutions buildSolutions(). The initialization phase (lines 21-23) is represented by two nested loops, the time complexity of its implementation is equal to 3jCj jAj. The process of the solutions table completion is presented by lines 24-27. The number of iterations of the outer (line 24-27) is equal to the number of input automata jAj. The number of the repetitions of the rst inner loop operations depends on the number of elements which belong to the previously found set of input sets of the available transitions for the considered automaton. The size of the set is marked as n. The total time complexity of the function taking into account the previous results is equal to
D := 3jCj jAj + 3jCj jAj + 3jCj + jAj n 3jCj jCij (1)
The complexity of the developed algorithm can be computed on the basis of our results. The initialization of the initial state of the resulting automaton requires jAj operations. The cycle through all the unconsidered (lines 3-19) composite states is determined by the number of elements in N , the number of iterations is equal to jStj. In this loop the considered earlier function for building solutions (line 5) is involved. Its complexity is de ned as (1). To examine all built solutions, it is necessary to perform a number of iterations which is equal to the cardinal number of the set jSOLj. To assign to all clocks of the global set the corresponding states, it must be jCj operations (lines 8). To form a new composite state (line 9), it is performed jAj repetitions of the loop code. To reset the states of input automata, it is necessary to perform the number of iterations which is equal to the number of input automata. The formula expressing the time complexity of the algorithm is as follows: jAj + jStj(D + jSOLj(jCj + 2 jAj)) (2)
Since we are considering the worst case in which all the expressions of the clock constraint speci cation language do not have common clocks, the value n which is equal to the number of all available transitions can be approximated by the quantity 3jCij, since the number of the available transitions is not greater than the number of all possible combinations of the states of clocks for the considered input automaton. Thus, after the change of the corresponding quantity the representation formula for the time complexity becomes: jAj(1 + jStj(3jCj(2 + 1 A j j + 3jCij jCij) + jSOLj( jCj + 2)))
A j j (3)
From the obtained result (3) we can conclude that the developed composition algorithm has exponential complexity in the number of clocks involved in the composition.
Additionally, it depends on the number of states in the resulting automaton. When the composition is in nite then the algorithm does not terminate. When the composition is nite, the complexity is exponential in the number of clocks in the worst case. For a software implementation of the algorithm, it is necessary to represent each kind of the built automata in terms of classes and to de ne the suitable presentation of the correspondent states. There are two types of input automata: nite and in nite. For the latter ones, lazy evaluation is used to compute the next state on demand.
All classes are divided into 5 main, architecturally signi cant packages: entities, abstractions, states, automata and executors. The entities package contains the primary classes-entities, which are necessary for the implementation of the composition algorithm such as the class for the representation of the clock notion, the class for the resulting automaton. The abstractions package stores two main interfaces that specify responsibilities for all automata and states. The states package includes all classes intended to work with states of all kinds of automata. The implementation for all previously formally de ned automata for the basic ccsl operators is contained in the automata package. The executors package includes classes-executors that are responsible for organizing the correct interactions of all classes so as to build the synchronized product of the input automata. 6
This work has proposed a data structure based on lazy evaluation to encode the semantics of ccsl operators as transition systems. Then the composition of ccsl operators is computed as the synchronized product of those transitions systems. The underlying de nitions were implemented in Java. The automaton form representation for basic expressions and relations of the ccsl kernel were proposed. The lazy evaluation was considered and applied for building the unbounded automata of the corresponding operators.
The complexity analysis of the algorithm was conducted. It allowed estimating the time resources needed by the composition algorithm which solves a given computational problem. It was shown that the computational complexity of the developed algorithm is exponential in the number of clocks and is linear with the size of the resulting automaton. Such an automaton can be in nite in which case the (semi)algorithm does not terminate.
However, there are many classical examples where the resulting automaton is nite, and where the actual complexity is much better than the theoretical worstcase computed here. As future work, we intend to qualify useful cases that are tractable in ccsl and therefore would allow model-checking ccsl speci cations.