Keywords

1 Introduction

The Unified Modeling Language (UML) Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) [1], adopted in November 2009, has introduced a Time Model [2] that extends the informal Simple Time of UML2. This time model is general enough to support different forms of time (discrete or dense, chronometric or logical). Its so-called clocks allow enforcing as well as observing the occurrences of events and the behavior of annotated UML elements. The Time Model comes with a companion language named the Clock Constraint Specification Language (CCSL) [3] defined in the annex of the MARTE specification. Initially devised as a language for expressing constraints between clocks of a MARTE model, CCSL has evolved and has been developed independently of the UML. CCSL is now equipped with a formal semantics [3] and is supported by a software environment (TimeSquare [4]) that allows for the specification, solving, and visualization of clock constraints.

MARTE promises a general modeling framework to design and analyze systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on verification techniques supported. Inspired by the works about state-based semantics interpretation for the kernel CCSL operators [5], this paper focuses on the divergence (see Sect. 3.1) detection of some CCSL specifications. This issue was addressed by [6, 7] but their propositions were applying parallel composition of individual CCSL constraints, making the propositions unsuitable for industrial size systems. In this work, we significantly reduce the complexity of the divergence detection by constructing and analyzing clock causality chains. Additionally our algorithm can point out what constraint can be added to make the specification divergence-free. In order to acquire clock causality chains, we first highlighted some interesting properties about causal relation between clocks. Furthermore, we propose an algorithm to decide if a given CCSL is divergence-free or not, by constructing the proposed a “Bounded Clock Set” (BCS) based on clock delay expression as well as the causality relation between clocks.

Section 2 introduces a state-transition based semantics for CCSL. Section 3 shows how to detect the divergence and make sure the specification is divergence-freedom based on the notion of divergence of CCSL specifications. Also, an algorithm, which is used to build the bounded clock set for determining the convergence, is depicted in this section. Section 4 illustrates, by using an example from architecture-driven analysis, the use of our algorithm on a CCSL specification. It shows how to improve a divergent specification such that it becomes a convergent one by adding clock constraints hinted by the algorithm. Finally, Sect. 5 makes a comparison with related works and Sect. 6 concludes the contribution and outlines some future works.

2 Preliminaries

This section briefly introduces the logical time model [2] of MARTE and the Clock Constraint Specification Language (CCSL). A technical report [3] and it latest update [8] describes the syntax and the semantics of a kernel set of CCSL constraints. We describe in this paper only the constraints that are used for our discussion.

The notion of multiform logical time has first been used in the theory of synchronous languages [9] and its polychronous extensions. CCSL is a formal declarative language to specify polychronous clock specification. It provides a concrete syntax to make the clocks and clocks constraints first-class citizens of UML-like models. Clocks in CCSL are used to measure the number of occurrences of events in a system. Logical clocks replace physical times by a logical sequencing. A CCSL specification do not need for clocks to be relative to a global physical time. They are by default independent of each other and what matter is the partial ordering of their ticks induces by the constraints between them.

A clock belongs to a clock set \( \mathcal{C} \). During the execution of a system, an execution step is defined and at a given step, every clock in \( \mathcal{C} \) can tick or not according to the constraints defined in the specification. A schedule captures what happens during one particular execution.

Definition 1 (Schedule):

A schedule is defined as a function Sched: \( {\mathbb{N}}_{>0} \rightarrow 2^{\mathcal{C}} \). ■

Given an execution step i ∈ ℕ>0, and a schedule σ ∈ Sched, σ(i) denotes the set of clocks that tick at step i.

For a given schedule, the configurations of the clocks tell us the advance of the clocks, relative to the others.

Definition 2 (Clock Configuration):

For a given schedule σ, clock \( c \in \mathcal{C} \) and a natural number n ∈ ℕ, the configuration χ σ : \( \mathcal{C} \) × ℕ → ℕ is defined recursively as:

$$ \chi_{\sigma } \left( {c,n} \right) = \left\{ {\begin{array}{*{20}l} {0 , } \hfill & {if\,n = 0 } \hfill \\ {\chi_{\sigma } \left( {c,n - 1} \right), } \hfill & {if\,c \notin \sigma \left( n \right)} \hfill \\ {\chi_{\sigma } \left( {c,n - 1} \right) + 1,} \hfill & {if\,c \in \sigma (n)} \hfill \\ \end{array} } \right. $$
(F.1)

■

For a clock c ∈, and a step n ∈ ℕ, χ σ(c, n) counts the number of times the clock c has ticked at step n for the given schedule σ.

CCSL is used to specify a set of valid schedules. There is usually more than one valid schedule that satisfies a given specification. If there is no satisfying schedule, then we say that the specification is ill-formed. The detail properties about the schedules against the given specification is investigated in [10]. Clocks can be finite of infinite. Since divergence problem only makes sense on infinite clocks, we do not care about constraints that make clock terminating (see [8] for details). Consequently, every clock in \( \mathcal{C} \) are infinite (will never terminate), i.e., ∀c ∈ \( \mathcal{C} \), χ σ(c, n) is boundless with n increasing.

Definition 3 (CCSL Specification):

A CCSL specification \( \mathcal{SPEC} \) is a pair <\( \mathcal{C} \), CConstr> , where \( \mathcal{C} \) is a set of clocks, CConstr is a set of formulae (see Definition 5) used to specify the relations among the clocks in the set \( \mathcal{C} \). ■

Definition 4 (Clock Set)

An element in the clock set \( \mathcal{C} \) can be given by the specification writer explicitly (explicit clock), or by one of the following clock expressions (implicit clock):

$$ Clock \text{ := } a + b\left| {a*b} \right|a\backslash b\left| {sup\left( {a, \, b} \right) \, } \right|inf\left( {a,b} \right) \, \left| {a\$ n \, | \, SampledOn\left( {a, \, b} \right)} \right|FilteredBy\left( {a,u, \, v} \right) $$
(F.2)

where a, b ∈ \( \mathcal{C} \) are clocks, u, v ∈(0 + 1)* are finite binary words, and n ∈ ℕ is a natural number. ■

Once we write one clock expression in the form of (F.2), a new clock is created and added into the clock set \( \mathcal{C} \). For example, if we give the explicit clock set {a, b, c}, and clock expression set {d = a + b, e = c $1}, then the considered clock set is \( \mathcal{C} \) = {a, b, c, d, e}. Note that there may not be any given name for the implicit clock of the clock expression (e.g. if it occurs in one clock relation) (see Definition 5). It should be noted that the new clock will be scheduled depending on the clock(s) that occur in that expression.

It is convenient to define a clock as an Abstract Data Type (ADT) [11] in Prototype Verification System (PVS) [12, 13] if we treat the clock expression as an element in a clock set instead of assigning them a new clock name.

The CCSL constraint defined over the clock set includes both the explicit clocks and implicit ones.

Definition 5 (CCSL Relation):

For a given clock set \( \mathcal{C} \), the corresponding clock relation set Φ(\( \mathcal{C} \)) over \( \mathcal{C} \) is defined recursively as:

ψ ≔ a ≺ b | a ≼ b| a ⊂ b | a # b | ψ ∧ ψ

where a, b ∈ \( \mathcal{C} \). ■

Every clock relation in the set Φ(\( \mathcal{C} \)), is a primitive formula that relates a clock pair or their conjunction.

Definition 6 (CCSL Specification Satisfaction).

For a given CCSL specification \( \mathcal{SPEC} \) = <\( \mathcal{C} \), CConstr>, A schedule σ over \( \mathcal{C} \) satisfies \( \mathcal{SPEC} \), denoted σ ⊨ \( \mathcal{SPEC} \), if and only if for every formulae r in CConstr, σ evaluates to true according to the following definition postulated by the CCSL semantics:

σ ⊨ r if and only if cases r’s form of

$$ \begin{aligned} \hfill \\ \begin{array}{*{20}l} {a \prec b:\forall n \in {\mathbb{N}},} \hfill & {\chi_{\sigma } \left( {a,n} \right) = \chi_{\sigma } \left( {b,n} \right) \Rightarrow b \notin \sigma (n + 1)} \hfill & {\left( {{\mathbf{Precedence}}} \right)} \hfill \\ {a{ \preccurlyeq }b \, :\forall n \in {\mathbb{N}},} \hfill & {\chi_{\sigma } \left( {a,n} \right) \ge \chi_{\sigma } \left( {b,n} \right)} \hfill & {\left( {{\mathbf{Causality}}} \right)} \hfill \\ {a \subset b \, :\forall n \in {\mathbb{N}}_{ > 0} ,} \hfill & {a \in \sigma \left( n \right) \Rightarrow b \in \sigma (n)} \hfill & {\left( {{\mathbf{Subclock}}} \right)} \hfill \\ {a \, \# \, b:\forall n \in {\mathbb{N}}_{ > 0} ,} \hfill & {a \notin \sigma \left( n \right) \vee b \notin \sigma (n)} \hfill & {\left( {{\mathbf{Exclusion}}} \right)} \hfill \\ {\psi_{1} \wedge \psi_{2} :\sigma { \vDash }\psi_{1} \wedge \sigma { \vDash }\psi_{2} } \hfill & {} \hfill & {\left( {{\mathbf{Conjunction}}} \right)} \hfill \\ \end{array} \hfill \\ \end{aligned} $$
(F.3)

where a, b ∈ \( \mathcal{C} \). ■

It’s straightforward to prove that both Causality and Subclock are pre-orders on \( \mathcal{C} \), i.e., they are reflexive and transitive. For simplicity, we can write a ≼ b ≼ c for a ≼ b∧ b ≼ c, and so do other transitive clock relation. The transitivity property of the Causality relation is of importance in determining the boundedness of a specification (see Sect. 3.2). It is also straightforward to prove that Exclusion is neither reflexive nor transitive. The transitive property of Precedence is very tedious to prove from this form of definition, although it is obvious in other semantics model [8].

The implicit clocks defined using clock expressions (F.2), are constrained according to the parameters of the clock expression. In other words, a clock expression is a clock generator where the output clock ticks or not according to the input clock(s) state and other arguments, if any.

Definition 7 (Clock Expression Satisfaction).

Whether an implicit clock (denoted c in the following) can tick or not in a schedule σ, is determined by the behaviors of the input clock(s) in σ,

σ ⊨ c if and only if cases c is defined by

$$ \begin{array}{*{20}l} {a \, + \, b:\forall n \in {\mathbb{N}}_{ > 0} ,c \in \sigma \left( n \right) iff a \in \sigma \left( n \right) \vee b \in \sigma (n)} \hfill & {\left( {{\mathbf{Union}}} \right)} \hfill \\ {a \, * \, b:\forall n \in {\mathbb{N}}_{ > 0} ,c \in \sigma \left( n \right) iff a \in \sigma \left( n \right) \wedge b \in \sigma (n)} \hfill & {\left( {{\mathbf{Intersection}}} \right)} \hfill \\ {a\backslash b:\forall n \in {\mathbb{N}}_{ > 0} ,c \in \sigma \left( n \right) iff a \in \sigma \left( n \right) \wedge b \notin \sigma (n)} \hfill & {\left( {{\mathbf{Minus}}} \right)} \hfill \\ {sup\left( {a, \, b} \right) \, :\forall n \in {\mathbb{N}},\chi_{\sigma } \left( {c,n} \right) = { \hbox{min} }(\chi_{\sigma } \left( {a,n} \right),\chi_{\sigma } \left( {b,n} \right))} \hfill & {\left( {{\mathbf{Supremum}}} \right)} \hfill \\ {inf\left( {a, \, b} \right):\forall n \in {\mathbb{N}},\chi_{\sigma } \left( {c,n} \right) = { \hbox{max} }(\chi_{\sigma } \left( {a,n} \right),\chi_{\sigma } \left( {b,n} \right))} \hfill & {({\mathbf{Infimum}})} \hfill \\ {a\$ d:\forall n \in {\mathbb{N}},\chi_{\sigma } \left( {c,n} \right) = { \hbox{max} }(\chi_{\sigma } \left( {a,n} \right) - d, 0)} \hfill & {({\mathbf{Delay}})} \hfill \\ \end{array} $$
(F.4)

SampledOn(a, b): ∀n ∈ ℕ>0, \( c \in \sigma \left( n \right) iff \)

$$ \begin{array}{*{20}l} {(b \in \sigma \left( n \right) \wedge (\exists j \in [1..n],a \in \sigma \left( j \right) \wedge \forall m:[j..n - 1],b \notin \sigma \left( m \right)))} \hfill & {({\mathbf{SampledOn}})} \hfill \\ \end{array} $$

FilteredBy (a, u, v): ∀n ∈ ℕ>0, \( c \in \sigma \left( n \right) iff \)

$$ \begin{array}{*{20}l} {(a \in \sigma \left( n \right) \wedge \left( {if k \le \left| u \right| {\text{then u}}\left[ k \right] = 1\,else\,v\left[ {\left( {k - \left| u \right|} \right) mod \left| v \right|} \right] = 1 } \right), where\,k = {\mathcal{X }}_{\sigma } ({\text{a}},n))} \hfill & {\left( {{\mathbf{FilteredBy}}} \right)} \hfill \\ \end{array} $$

where a, b ∈ \( \mathcal{C} \), u, v ∈ (0 + 1)*, and d ∈ ℕ>0. |u| (resp. |v|) represents the length of binary word u (resp. v), k = χσ(a, n) is the number of tick of clock a from step 1 to n. ∎

By composing the relations and the expressions provided in Definitions 4 and 5, some user-defined clock relations can be further defined, as below:

$$ \begin{array}{*{20}l} {a\sim b: = a \prec b \prec a \, \$ \, 1} \hfill & {\left( {{\mathbf{Alternation}}} \right)} \hfill \\ \end{array} $$
(F.5)
$$ \begin{array}{*{20}l} {a \prec_{\text{n}} b\text{ := }a \prec b \prec a \, \$ \, n} \hfill & {\left( {{\mathbf{Bounded}} \, {\mathbf{precedence}}} \right)} \hfill \\ \end{array} $$
(F.6)
$$ \begin{array}{*{20}l} {a \equiv b\text{ := }a{ \preccurlyeq }b \wedge b{ \preccurlyeq }a} \hfill & {\left( {{\mathbf{Coincidence}}} \right)} \hfill \\ \end{array} $$
(F.7)

Obviously, Alternation (F.5) is a special case of bounded precedence (F.6). Alternation (which is frequently used in the CCSL specifications), is a kind of bounded relation that is discussed in detail in Sect. 3.

From the definitions above, some proved propositions can be listed below. The reader who is interested the proof can get the details in the report [5].

Proposition 1 (Precedence Implies Causality).

The Precedence is a stronger form of causality:

σ ⊨ a ≺ b ⟹ σ ⊨ a ≼ b ■

Proposition 2 (Subclock Implies Causality).

When a is a Subclock of b, then b is faster than a:

σ ⊨ a ⊂ b ⟹ σ ⊨ b ≼ a ■

Proposition 3 (Union and Causality).

The union of two clocks is faster than both clocks:

σ ⊨ u ≔ a + b ⟹ σ ⊨ u ≼ a ∧ σ ⊨ u ≼ b ■

Proposition 4 (Intersection and Causality).

The intersection of two clocks is slower than both clocks:

σ ⊨ i ≔ a * b ⟹ σ ⊨ a ≼ i ∧ σ ⊨ b ≼ i ■

Proposition 5 (Infimum and Causality).

The infimum of two clocks is always faster than both clocks:

σ ⊨ f ≔ inf(a, b) ⟹ σ ⊨ f ≼ a ∧ σ ⊨ f ≼ b ■

Proposition 6 (Supremum and Causality).

The supremum of two clocks is always slower than both clocks:

σ ⊨ s ≔ sup(a, b) ⟹ σ ⊨ a ≼ s ∧ σ ⊨ b ≼ s ■

Proposition 7 (Delay and Causality).

The delayed clock is always slower than the base clock:

σ ⊨ c ≔ a $ d ⟹ σ ⊨ a ≼ c ■

Propositions 1 to 7 defines new implicit Causality relations from all the other relations (Precedence and Subclock) and expressions (Union, Intersection, Infimum, Supremum and Delay). The Definitions 1 to 7 have been formalized in PVS, and the Propositions 1 to 7 have been proved (in most cases by induction).

Based on the definitions of SampledOn and FilteredBy in (F.3), c ≔ SampledOn(a, b) implies a ≼ c and c ⊂ a, c ≔ FilteredBy(a, u, v) implies c ⊂ a. Hence, some Causality relations between the new implicit clock and their input clock can indirectly be deduced from the clock expression SampledOn and FilteredBy. Therefore, we can also get Causality relations using SampledOn and FilteredBy, besides using Propositions 1 to 7 .

3 Divergence Detection

3.1 Divergence and Bounded Relation

Let’s consider a very simple CCSL specification \( \mathcal{SPEC}_{1} \) = <{sending, ack}, {sending ≼ ack}>. It is divergent as we don’t know what will happen at a certain execution step i in a schedule σ provided that σ satisfies \( \mathcal{SPEC}_{1} \) from step 1 to step i – 1. That is to say, there are many possibilities of clock ticking (tick sending, tick ack, or both) to ensure the satisfaction of \( \mathcal{SPEC}_{1} \) at step i. Furtherly, whether the clock ack ticks or not is uncontrollable and unpredicatable since there is nothing to trigger its firing. Therefore, some expected properties may eventually not be guaranteed, if it is implied by the implementation of ack’s tick.

Definition 8 (Divergent Specification).

We say a CCSL specification \( \mathcal{SPEC} \) = <\( \mathcal{C} \), CConstr> is divergent, if an expected clock in \( \mathcal{C} \) has the possibility never ticks, formally,

∃σ, (σ ⊨ \( \mathcal{SPEC} \) ∧∃g, r ∈, ∀i:{k: ℕ>0| r ∈ σ(k)}, ∃j> i, g ∉ σ(j)). ■

Here g (means goal) is the expected action that may be an acknowledge signal/operation of other clock r (means request). That is to say, after performing some necessary operation(s) by ticking the some clocks in \( \mathcal{C} \)\{g} containing clock r, there must be an expected final result (ticking clock g) appears in the admissible future, but unfortunately only God knows g will tick or not in the divergent specification \( \mathcal{SPEC} \). Therefore, the divergence of \( \mathcal{SPEC_{1}} \) is asserted by choosing g = ack, r = sending and the given schedule σ such that ∀i ∈ ℕ>0, σ(i) = {sending}.

On the contrary, another example \( \mathcal{SPEC_{2}} \) = <{a, b}, {a ~ b}> is not divergent because the constraint a ~ b postulates that the schedule that satisfies \( \mathcal{SPEC_{2}} \) must execute by alternating a with b forever. In this case, we say the behavior and the corresponding CCSL specification are convergent if it is also free of some unexpected properties, such as deadlock and livelock and so on.

The divergent specification behavior is not predicable in the sufficient future. It is possible for some expected action(s) to be delayed infinitely in the future. This bad behavior is unexpected since some actions can never happen after a certain simulation step. Therefore, a specification that contains divergence is unsafe. How to detect divergence existence in a given CCSL specification is the main subject in this section. Additionally, we provide some suggestions to modify the CCSL specification so that it becomes divergence-free.

For a given CCSL specification <\( \mathcal{C} \), CConstr>, if the difference between the speeds of two clocks a, b ∈ \( \mathcal{C} \) is limited in an allowed boundary, we say the clock pair (a, b) has a bounded relation.

Definition 9 (Bounded Relation).

For a given clock set \( \mathcal{C} \), two clocks a, b ∈ \( \mathcal{C} \), and a schedule σ over \( \mathcal{C} \), a and b has the bounded relation with a given boundary m ∈ ℕ, denotes |a, b| ≤ m:

σ ⊨ |a, b| ≤ m iff ∀i ∈ ℕ>0, ∃j ∈ ℕ>0, | \( \mathcal{X}_{\sigma}(a, i) - \mathcal{X}_{\sigma}(b, j) \) | ≤ m

m (resp. – m) can be called upper (resp. lower) bound. ■

When such an unbounded clock pair is found, we say that there is divergence in the specification. We say the specification free of divergence is a bounded specification.

Definition 10 (Bounded Specification).

For a given CCSL specification \( \mathcal{SPEC} \) = <\( \mathcal{C} \), CConstr>, ∀a, b ∈ \( \mathcal{C} \), \( \mathcal{SPEC} \) is bounded if and only if any clock pair has the bounded relation:

∀σ, σ ⊨ \( \mathcal{SPEC} \) ⟹ ∃m ∈ ℕ, σ ⊨ |a, b| ≤ m ■

A bounded specification is divergence-free because there are no possible boundless drifts between any clock pair (i.e. between the actions).

If we check every clock pairs among all clocks in \( \mathcal{C} \) to decide whether a specification is divergence-free or not, there are \( \left( {\begin{array}{*{20}c} {|{\mathcal{C}}|} \\ 2 \\ \end{array} } \right) = \left| {\mathcal{C}} \right| \times (\left| {\mathcal{C}} \right| - 1)/2 \) pairs need to be checked. The number of checks then totals to (\( |\mathcal{C}|^{2} \)). But in practice many checks can be safely neglected when the bounded relation is implied by the already checked one.

The Bounded Relation can directly be derived from the formula for most of the constraints. Let us show how to get the Bounded Relation between two clocks implied by the existing clock relations and expressions.

Bounded Relation is an equivalence relation over \( \mathcal{C} \), i.e., it is reflexive, symmetric and transitive. Note that they do not necessarily have the same boundaries for different bounded relations.

Proposition 8 (Bounded Extension).

The Bounded Relation is transitive and the transitive resulting boundary is the sum of the original ones.

|a, b| ≤ m 1 ∧ |b, c| ≤ m 2 ⟹ |b, c| ≤ m 1  + m 2 ■

Proposition 8 can be proved by using classical properties of inequalities addition. The proof is obvious and omitted here.

Proposition 9 (Bounded Restriction).

Bounded relation can be restricted w.r.t. Causality, and the resulting boundary is not greater than the original one.

|a, b| ≤ m ∧ ∀c ∈ \( \mathcal{C} \), (a ≼ c ≼ b ∨ b ≼ c ≼ a) ⟹ |a, c| ≤ m ∧ |b, c| ≤ m ■

Proof of Proposition 9:

Let maxDrift_ab(n) = \( \chi_{\sigma } \left( {a,n} \right) - \chi_{\sigma } \left( {b,n} \right) \),

maxDrift_ac(n) = \( \chi_{\sigma } \left( {a,n} \right) - \chi_{\sigma } \left( {c,n} \right), \)

maxDrift_bc(n) = \( \chi_{\sigma } \left( {b,n} \right) - \chi_{\sigma } \left( {c,n} \right) \), for all n ∈ ℕ,

from the Definition 9 , we have

|a, b| ≤ m ⟹ |maxdrift_ab(n)| ≤ m ⟹ −m ≤ maxdrift_ab(n) ≤ m, for all n ∈ ℕ,

Assume a ≼ c ≼ b, from the definition 6 , we have∀n ∈ ℕ, \( \chi_{\sigma } \left( {a,n} \right) \ge \chi_{\sigma } \left( {c,n} \right) \ge \chi_{\sigma } \left( {b,n} \right) \) , then maxDrift_ac(n) ≥ 0 ≥ – m.

$$ from \, maxdrift\_ab\left( n \right) \le m $$
(1)
$$ maxdrift\_bc\left( n \right) \le \, 0 $$
(2)

(1) + (2) gets

maxDrift_ac(n) = maxdrift_ab(n) + maxdrift_bc(n) ≤ 0 + m = m

therefore, |maxDrift_ac(n)| ≤ m.

similarly, from ( 2 ) we have∀n ∈ ℕ, maxDrift_bc(n) ≤ 0 ≤ m,

  • maxDrift_bc(n) ≤ maxdrift_ab(n) ≤ m ⟹ maxDrift_bc(n) ≥ – m

There exists the similar proof under the cases b ≼ c ≼ a. ■

From Definition 7, we can see Delay implies the Bounded Relation:

Proposition 10 (Delay Implies Bounded).

The delayed clock a and the corresponding base clock b has the Bounded Relation with a lower bound 0 and a upper bound d:

σ ⊨ a ≔ b $ d ⟹ σ ⊨ |a, b| ≤ d ■

Proof of Proposition 10: This is direct conclusion from Definition 7.

The primitive clock relations and the other clock expressions except Delay and FilteredBy don’t imply bounded relation. But their composition may deduce.

Proposition 11 (Alternate Implies Bounded).

The clock pair involves in Alternation relation has the bounded relation with the boundary 1:

σ ⊨ a ~ b ⟹ σ ⊨ |a, b| ≤ 1 ■

Proof of Proposition 11:

\( a\sim b \Leftrightarrow \) by Alternation definition (F.5)

a ≼ b ≼ a $ 1 ⟹ by Proposition 1 ( Precedence Implies Causality )

a ≼ b ≼ a $ 1 ⟹ by Proposition 10 (Delay Implies Bounded)

|a, a $ 1| ≤ 1 ⟹ by Proposition 9 (Bounded Restriction)

|a, b| ≤ 1 ∧ |a $ 1, b| ≤ 1 ⟹ by proposition calculus

|a, b| ≤ 1 ■

Similarly, one can prove Bounded Precedence (F.6) is also a Bounded Relation. FilteredBy expression c ≔ a ▼(u.v ω), which defines a clock new clock c as a Subclock of a according to two binary words u and v, implies a Bounded Relation between clock pair (c, a) if there exists at least one 1-bit in the periodical pattern v.

Proposition 12 (FilteredBy may Imply Bounded).

The clock pair (a, c) involves in the expression c ≔ a ▼(u.v ω) has the Bounded Relation with the boundary |u| + p × (|v| – 1) if and only if ∃i ∈ [1..|v|] such that v[i] = 1. Where p is the number of periodical patterns that have passed from the initial configuration. ■

Proof of Proposition 12:

Suppose a schedule σ against by c ≔ a ▼(u.v ω ), For some schedule step m, suppose clock a has ticked |u| + |v| times from start, then

χ σ (a, m) = |u| + |v|

By FilteredBy definition (F.4), during the process, clock a ticks at step j if and only if both a ticks and u.(v) ω [j] = 1. Because ∃i ∈ [1..|v|], v[i] = 1, we get:

1 ≤ χ σ (c, m) ≤ |u| + |v|

With the passage of schedule σ, χ σ (c, n) will increase at least one while χ σ (a, n) increase every |u| + |v| after passing a periodical pattern. Therefore, when the schedule σ reaches step n by the time p periodical patterns has passed:

χ σ (a, n) = |u| + p × |v| and p ≤ χ σ (c, n) ≤ |u| + p × |v| ⟹ |χ σ (a, n) – χ σ (c, n)| ≤ |u| + p × (|v| – 1) ■

3.2 Clock Causality Chain and Bounded Clock Set

In order to determine whether a CCSL specification is divergent or not, according to Definition 9, one must show every clock pair has Bounded Relation. Due to most clock constraints without the bound information, we try to capture the Bounded Relation from the Causality relation.

Definition 11 (Clock Causality Chain).

For a given clock set \( \mathcal{C} \), some clocks in \( \mathcal{C} \) may form a Clock Causality Chain (CCC), which is a finite sequence c 1 , c 2 , …, c n such that ∀i ∈ [1..n – 1], c i ≼ c i+1 and n ≥ 2. It is called Bounded Clock Causality Chain (BCCC) if ∃m ∈ ℕ, |c 1 , c n | ≤ m, and m is called the chain’s boundary. It is an Unbounded CCC (UCCC) otherwise. ■

Proposition 13 (BCCC Boundedness).

ABCCC ρ = c 1 , c 2 , …, c n with a boundary m implies that any two clocks in ρ has the Bounded Relation: ∀i, j ∈ [1..n], |c i , c j | ≤ m. ■

Proposition 13 is easily proved by using Proposition 9 (Bounded Restriction) as well as the Causality transition.

Due to Proposition 13, Checking \( \left( {\begin{array}{*{20}c} {\text{n}} \\ 2 \\ \end{array} } \right) \) clock pairs bounded relation is replaced by checking only one clock pair and additionally sorting n clocks with respect to Causality relation. Moreover, the Causality relation is much easier to get than Bounded Relation as the former is implied by some clock constraints (see Propositions 1–7 ).

Obviously, a specification is divergent if we can get a UCCC.

Theorem 1 (UCCC Implies Divergence).

A CCSL specification \( \mathcal{SPEC} \) = <\( \mathcal{C} \), CConstr> is divergent, if there exists a UCCC ρ = c 1 , c 2 , …, c n (∀i ∈ [1..n], c i ∈ \( \mathcal{C} \)) induced by the CConstr. ■

Proof of Theorem 1:

ρ is unbounded ⟹∀i ∈ [1..n − 1], c i ≼ c i+1 ⟹ That c n doesn’t tick forever in some schedule σ has nothing about asserting the true value of σ ⊨ \( \mathcal{SPEC} \).

We can find such a schedule σ against \( \mathcal{SPEC} \) that c 1 tick at least once. σ is indeed the witness (g = c n and r = c 1 ) for uncovering the divergence of \( \mathcal{SPEC} \) according to Definition 8. ■

Let us illustrate Theorem 1 on a toy example, \( \mathcal{SPEC}_{\text{s}}=<\mathcal{C} \), CConstr>, where \( \mathcal{C} \) = {a, b, sup(a, b), c} and CConstr = {a ~ c, sup(a, b) ≼ c}. Let sup = sup(a, b), we get

|a, c| ≤ 1, by Proposition 11

a ≺ b and a ≼ b, by Alternation definition and Proposition 1.

a ≼ sup ≼ c and b ≼ sup, by Proposition 6.

The Causality Clock Graph (CCG) [5] in Fig. 1 shows the Causality relations among clocks. The Causality line from clock a to c can be safely removed because of causality transition.

Fig. 1.
figure 1

CCG for \( \mathcal{SPEC}_{\text{s}} \)

Full size image

The CCC a, sup, c is a BCCC, while the CCC ρ = b, sup is a UCCC. The existence of ρ draws the conclusion \( \mathcal{SPEC}_{\text{s}} \) is a divergent specification.

Via the analysis of \( \mathcal{SPEC}_{\text{s}} \), Theorem 1 tell us that the existence of a UCCC in a CCSL specification witnesses its divergence. Unfortunately, this is a sufficient, but not necessary, condition for deciding specification’s divergence. We say nothing about the convergence even if we get one or more BCCCs from a CCSL specification. The Bounded Clock Set can be used to determine a specification’s convergence.

Definition 12 (Bounded Clock Set).

For a given clock set \( \mathcal{C} \), a clock set \( \mathfrak{B} \) = {c ⊥, c 1, …, c m, c ⊤, c m+1…, c m + n}, subset of \( \mathcal{C} \), which contains at least 2 elements, is called a Bounded Clock Set (BCS), if all the following conditions hold:

  1. (i)

    (Lower-upper Bound) ∃d ∈ ℕ, |c ⊥, c ⊤| ≤ d,

  2. (ii)

    (Causality Bound) ∀i ∈ [1..m], c ⊥ ≼ c i ≼ c ⊤,

  3. (iii)

    (Absence Unbounded Clock) ∀i ∈ [m + 1..m + n], ∃c ∈ \( \mathfrak{B}_{\text{R}} \) (see below), d ∈ ℕ, |c, c i | ≤ d.

The clock c ⊥ (resp. c ⊤) is called the bottom (resp. top) clock. The subset \( \mathfrak{B}_{\text{R}} \) = {c ⊥, c 1, …, c m, c ⊤} of \( \mathfrak{B} \) is called Causal Bounded Clock Set (CBCS). ■

A BCS \( \mathfrak{B} \) = {c ⊥, c 1, …, c m, c ⊤, c m+1…, c m + n}, as shown in Fig. 2, includes two disjoint subsets:

Fig. 2.
figure 2

The BCS structure

Full size image

  • \( \mathfrak{B}_{\text{R}} \) = {c ⊥, c 1, …, c m, c ⊤} contains the fastest clock c ⊥ as the bottom, and the slowest clock c ⊤ as the top, while all other ones’ speed lies between c ⊥ and c ⊤. Note that m = 0 in some cases.

  • \( \mathfrak{B} \) \ \( \mathfrak{B}_{\text{R}} \) = {c m+1…, c m + n} We don’t care about the speed of these clocks in relation to the one in \( \mathfrak{B}_{\text{R}} \). But a common fact is that all of them must be bounded by speed of one of the clocks in \( \mathfrak{B}_{\text{R}} \). Note that n = 0 in some cases, i.e., this set is an empty set.

The bottom (resp. top) clock is probably not a “proper” bottom (resp. top) clock because maybe there exists a clock in \( \mathfrak{B} \)\\( \mathfrak{B}_{\text{R}} \) which is faster (resp. slower) than it.

Theorem 2 (BCS Implies Divergence-Freedom).

A CCSL specification \( \mathcal{SPEC}={<}\mathcal{C}, CConstr{>} \) is free of divergence, if there exists a BCS \( \mathfrak{B} \) ⊇ \( \mathcal{C} \) implied by the CConstr. ■

Proof of Theorem 2:

Let \( \mathfrak{B} \) = {c ⊥, c 1, …, c m, c ⊤, c m+1…, c m + n}, and \( \mathfrak{B}_{\text{R}} \) = {c ⊥, c 1, …, c m, c ⊤}

By applying Proposition 9 (Bounded restriction) to condition (i) and (ii) in Definition 12, we have

$$ \forall i \in \left[ {1, \ldots ,m} \right], \, clock \, pairs \, (c_{ \bot ,} c_{i} ) \, and \, (c_{i,} c^{ \top } ) \, are \, bounded. $$
(B_1)

By Proposition 8 (Bounded extension), via the c ⊥ or c ⊤ as the middle clock b occurs, we have

$$ \forall i,j \in \left[ {1, \ldots ,m} \right], \, clock \, pair \, \left( {c_{i,} c_{j} } \right) \, is \, bounded. $$
(B_2)

Summarizing (B_1) and (B_2),

$$ \forall c_{i,} c_{j} \in {\mathfrak{B}}_{\text{R}} , \, clock \, pair \, \left( {c_{i,} c_{j} } \right) \, is \, bounded. $$
(B_3)

From condition (iii) in Definition 12 , ∀i ∈ [m + 1..m + n], ∃c ∈ \( \mathfrak{B}_{\text{R}} \) , clock pair (c, c i ) is bounded,

By Proposition 8 again via the c occurs in the last line as the middle clock b, we have

$$ \forall c_{i} \in {\mathfrak{B}}_{\text{R}} ,_{{}} c_{j} \in {\mathfrak{B}}\backslash {\mathfrak{B}}_{\text{R}} clock \, pair \, \left( {c_{i,} c_{j} } \right) \, is \, bounded. $$
(B_4)
$$ \forall c_{i,} c_{j} \in {\mathfrak{B}}\backslash {\mathfrak{B}}_{\text{R}} , \, clock \, pair \, \left( {c_{i,} c_{j} } \right) \, is \, bounded. $$
(B_5)

Summarizing (B_3), (B_4) and (B_5), we conclude

∀c i, c j ∈ \( \mathfrak{B} \) , clock pair (c i, c j ) is bounded.

Because \( \mathfrak{B} \) ⊇ \( \mathcal{C} \) , ∀c i, c j ∈ \( \mathcal{C} \) , clock pair (c i, c j ) is bounded.

By Definition 10 ( Bounded Specification), \( \mathcal{SPEC} \) is divergence-freedom specification. ■

If we cannot derive a bounded relation from \( \mathcal{C} \) obviously, introducing some external clock(s) that can form BCCC is allowed. Therefore, we use \( \mathfrak{B} \) ⊇ \( \mathcal{C} \) rather than \( \mathfrak{B} \) = \( \mathcal{C} \) in Theorem 2.

Fig. 3.
figure 3

Causality Clock Graph for \( \mathcal{SPEC}_{\text{i}} \)

Full size image

Let us illustrate Theorem 2 on a simple example, \( \mathcal{SPEC}_{\text{i}}=<\mathcal{C}, CConstr>\), where \( \mathcal{C} \) = {a, b, inf(a, b), o 1 , o 2 } and CConstr = { a ≼ o 1 , inf(a, b) ~ o 1 , b ~ o 2 , b ≼ o 1 }.

Let inf = inf(a, b), via some given propositions above, we can get the explicit and implicit Causality relation list from CConstr (Fig. 3):

inf ≼ a≼ o 1 , b ≼ o 1 , b ≼ o 2

By Proposition 11, we know clock pairs (inf, o 1 ) and (b, o 2 ) are bounded. Then we can construct a BCS \( \mathfrak{B}_{speci} \) = {c ⊥ = inf, c 1 = a, c 2 = b, c ⊤ = o 1, c 3 = o 2 } shown in Fig. 4a with m = 2 and n = 1 in Definition 12. Because \( \mathfrak{B}_{speci} \) ⊇ (\( \mathcal{SPEC}_{\text{i}} \)), we assert \( \mathcal{SPEC}_{\text{i}} \) is free of divergence by Theorem 2.

Fig. 4.
figure 4

Two represents for BCS of \( \mathcal{SPEC}_{\text{i}} \)

Full size image

Note that maybe there several other possibilities to assign the bottom or top clock. For example, \( \mathfrak{B} \) speci_alt  = {c ⊥ = inf, c ⊤ = b, c 1 = a, c 2 = o 1 ,c 3 = o 2 } shown in Fig. 4b is another same member set but assigned with different top clock. Here m = 0 and n = 3.

\( \mathfrak{B} \) speci is a “much better” BCS than \( \mathfrak{B} \) speci_alt in the sense of determining the boundedness among clocks. We can easily assert \( \mathfrak{B} \) speci is a BCS satisfied by conditions (i), (ii) and (iii) in Definition 12. On the contrary, As to \( \mathfrak{B} \) speci_alt , both conditions (i) and (iii) are not straightforwardly asserted using the CConstr( \( \mathcal{SPEC}_{\text{i}} \) ) as well as the associated propositions list above. In fact, \( \mathfrak{B} \) speci_alt is constructed dedicatedly to show its inconvenience when I know the fact convergence. In purpose of the efficiency for convergence assertion, Subsect. 3.3 will design an algorithm for constructing BCS.

All the proofs about these propositions and theorems in Sects. 3.1 and 3.2 are completed with the help of PVS. Hence, we can try to solve some problem without any doubt about its correctness. The following theorem, written in PVS specification, is a special caseFootnote 1 of Theorem 2, can be used to assert divergence-free of CCSL specifications.

Note:

  1. (1)

    Clock is type to represent explicit clock set.

  2. (2)

    AClock is a defined ADT includes both Clock and implicit clocks defined in Definition 4.

  3. (3)

    “⊨” is interpreted via Definitions 6 and 7.

  4. (4)

    maxDrift is Bounded relation in Definition 9.

3.3 Detection Algorithm

For a given specification \( \mathcal{SPEC} \) = <\( \mathcal{C} \), CConstr>, there are three simply rules to prevent \( \mathcal{SPEC} \) from divergence:

One violation of Rules 1–3 causes the specification’s divergence. The following parts will consider only the specification that follows Rules 1–3.

If we have no enough faith to assert the convergence CCSL specification, we can try to witness its divergence via discovering a UCCC by Theorem 1 because it is much easier to find an unbounded clock pair than to determine all the clock pairs are bounded.

When there is no obvious UCCC be found from a CCSL specification, we need to design an algorithm to try to construct a BCS, for the purpose of using Theorem 2 to guarantee specification’s convergence.

For a given \( \mathcal{SPEC}=<\mathcal{C},CConstr>\), we first sort the clock based on the Causality-related clock constraints (includes Causality relation and those imply it) in CConstr with regard to Causality.

Algorithm 1 includes three parts:

  1. (I)

    Get (and update if required) the bottom and top clock.

  2. (II)

    Get the clock set in which it is not faster than the bottom and not slower than the top.

  3. (III)

    Analyze the boundedness of left clocks.

We can assert that \( \mathfrak{B} \) constructed in Algorithm 1 must be a BCS by Propositions 8 and 9. So this algorithm’s correctness is ensured by Theorem 2 since \( \mathcal{C} \) = ∅ ⟹ \( \mathfrak{B} \) ⊇ \( \mathcal{C} \).

Algorithm 1 must terminate because of the finiteness of clock set. The complexity of Algorithm 1 is (\( |\mathcal{C}| \)). If most clocks can be dealt with in part I and II, the efficiency of algorithm is very high. Therefore, via Algorithm 1, determining boundedness among all clock pairs is converted into checking boundedness on much fewer clock pairs and additionally sorting clocks w.r.t. Causality relation.

4 Case Study

To illustrate the approach, we take an example inspired by [14], that was used for flow latency analysis on Architecture Analysis and Design Language (AADL) specifications. However, with CCSL we are conducting different kinds of analyses.

Figure 5 considers a simple application described as a UML activity. This application captures two inputs in1 and in2, performs some calculations (Step1, Step2 and Step3) and then produces a result out. This application has the possibility to compute Step1 and Step2 concurrently depending on the chosen execution platform. This application runs in a streaming-like fashion by continuously capturing new inputs and producing outputs.

Fig. 5.
figure 5

Simple application

Full size image

To abstract this application as a CCSL specification, we assign one clock to each action. The clock has the exact same name as the associated action (e.g., step1). We also associate one clock with each input, this represents the capturing time of the inputs, and one clock with the production of the output (out). The successive instants of the clocks represent successive executions of the actions or input sensing time or output release time. The basic CCSL specification is \( \mathcal{SPEC}_{\text{simp}}=<\mathcal{C}, {\rm CConstr}>\), where \( \mathcal{C} \) = {in1,in2,step1,step2,step3,out}, CConstr includes the following clock constraints:

$$ in{\it 1}{ \preccurlyeq }step{\it 1} \bigwedge step{\it 1} \prec step{\it 3} $$
(F.8)
$$ in2 \preccurlyeq step2 \bigwedge step2 \prec step3 $$
(F.9)
$$ step3 {\preccurlyeq} out $$
(F.10)

(F.8) specifies that step1 may begin as soon as an input in1 is available. Executing step3 also requires step1 to have produced its output. (F.9) is similar for in2 and step2. (F.10) states that an output can be produced as soon as step3 has executed. Note that CCSL precedence is well adapted to capture infinite FIFOs denoted on the figure as object nodes. Such a specification is clearly not convergent because of its violation of Rule 2 (Bounds Existence) in Rule list for avoiding divergence. After the sorting the clocks w.r.t. Causality relation, we get two CCCs:

$$ \rho_{1}: in {\preccurlyeq} step1 { \preccurlyeq }step3 {\preccurlyeq} out $$
$$ \rho_{2}: in {\preccurlyeq} step1 { \preccurlyeq } step3 {\preccurlyeq} out $$

It is also stated again that \( \mathcal{SPEC}_{\text{simp}} \) is divergent by Theorem 1 as both ρ 1 and ρ 2 are unbounded. If one CCSL constraint like (F.11) is added into CConstr(\( \mathcal{SPEC}_{\text{simp}} \)) as a test like that in [5].

$$ sup\left( {in1, \, in2} \right)\sim out $$
(F.11)

By Proposition 6, the following are two new UCCCs are acquired since the addition of (F.11):

in1 ≼ sup(in1, in2)

in2 ≼ sup(in1, in2)

Now we try to use Algorithm 1 to check whether \( \mathcal{SPEC}_{\text{simp}} \) is free of divergence or not. Let sup in12 /sup(in1, in2), by Expanding the Alternation definition, (F.11) becomes

sup in12  ≺ out ∧ out ≺ (sup in12 $ 1)

Now (\( \mathcal{SPEC}_{\text{simp}} \)) = {in1, in2, step1, step2, step3, out, sup in12 , sup in12 $ 1} correspondingly, by part I of Algorithm 1, we get \( \mathfrak{B} \) = {c ⊥ = sup in12 , c ⊤ = sup $1}, then using part II of Algorithm 1, the clock out is added into \( \mathfrak{B} \). Furtherly, because of ρ 1 , ρ 2 and the fact sup in12 is the fastest clock that is slower than in1 and in2 by Definition 7, we can deduce ∀c ∈ {step1,step2, step3}, c ⊥≼ c ≼ c ⊤ by Propositions 1 to 7. Therefore, the clocks step1, step2 and step3 can also be added into \( \mathfrak{B} \) via part II of Algorithm 1. Up to now, \( \mathfrak{B} \) = {c ⊥ = sup in12 , step1,step2, step3,out, c ⊤ = sup in12 1}, and none of other clock can be added into \( \mathfrak{B} \) further. Therefore, \( \mathcal{SPEC}_{\text{simp}} \) is divergent because \( \mathfrak{B} \) ⊉ \( \mathcal{C} \) witnessed by in1,in2 ∈ \( \mathcal{C} \) but in1,in2 ∉ \( \mathfrak{B} \). This is caused by that bounds on Supremum do not imply bounds on in1(or in2) and out, not to mention to the bound on in1 and in2.

To become a bounded(or safe) system \( \mathcal{SPEC}_{\text{simp}\_{\text{safe}}} \), we can for instance replace (F.11) by (F.12).

$$ inf\left( {in1, \, in2} \right)\sim out $$
(F.12)

Let in f in12 /inf(in1, in2), in fact, (F.12) equals

in f in12  ≺ out ∧ out (inf in12 $ 1)

Because of introducing new clock constraint (F.12), some new clocks (implicit clocks) are introduced as well, now \( \mathcal{C}(\mathcal{SPEC}_{\text{simp}\_{\text{safe}}}) \) = \( \mathcal{C}(\mathcal{SPEC}_{\text{simp}}) \) ∪ {inf in12 , inf in12 $ 1}.

Let’s check its divergence-freedom again by Algorithm 1. By part I of Algorithm 1, we get \( \mathfrak{B} \) = { c ⊥ = inf in12 , c ⊤ = inf in12 $ 1}, then using part II of Algorithm 1, all the clocks in \( \mathcal{C} \) can be added into \( \mathfrak{B} \) because their speed are constrained between the slowest clock inf in12 and the fastest clock inf in12 $ 1 as revealed by the following CCCs deduced by the Propositions 1, 5 and 7 as well as ρ1 and ρ2 above.

inf in12 ≼ in1 ≼ step1 ≼ step3 ≼ out ≼ (inf in12 $ 1)

inf in12 ≼ in2 ≼ step2 ≼ step3 ≼ out ≼ (inf in12 $ 1)

The resulting \( \mathfrak{B} \) = {c ⊥ = inf in12 , in1, step1, in2, step2, step3, out, c ⊤ = inf in12 $ 1}, as shown in Fig. 6, is obviously a superset of \( \mathcal{C} \)(\( \mathcal{SPEC}_{\text{simp}\_{\text{safe}}} \)). Hence, the CCSL specification \( \mathcal{SPEC}_{\text{simp}\_{\text{safe}}} \) is free of divergence. Note that \( \mathfrak{B} \) is also a CBCS because all of clock c ∈ \( \mathfrak{B} \), c ⊥ ≼ c ≼ c ⊤.

Fig. 6.
figure 6

BCS of simple application

Full size image

With the help of bounded_set_boundSPEC in Sect. 3.2, we can complete the proof of theorem simp_safe for asserting the boundedness of \( \mathcal{SPEC}_{\text{simp}\_{\text{safe}}} \) in PVS by the lemma simp_bcs as follows. In fact, \( \mathcal{SPEC}_{\text{simp}\_{\text{safe}}} \) is a specification free of divergence.

5 Related Work

Some techniques were provided as an effort to analyze CCSL specifications. [15] implemented the automatic analysis by translating CCSL into signal, for the purpose of generating executable specifications through discrete controller synthesis. However, this work did not consider the Infimum and Supremum operators that introduce unbounded counters and did not address the problem of deciding whether the specification is divergence-freedom or not. Exhaustive analysis of CCSL through a transformation into labeled transition systems has already been attempted in [16]. However, in those attempts, the CCSL operators were bounded because the underlying model-checkers cannot deal with infinite labeled transition systems.

In [6], the authors showed that even though the primitive constraints were unbounded, the composition of these primitive constraints could lead to a system where only a finite number of states were accessible. [7] defines a notion of safety for CCSL and establish a condition to decide whether a specification is safe on the transformed marked graph from CCSL.

All the above works share one common point: the specification analysis were done by some transformation and performed on the transformed target. The results were dependent on the correctness and efficiency of the mechanized transformation.

Our contribution is straightforward based on the clock Causality relation used to sort and the clock expression used to determine the clock pair’s boundary. It is not necessary for the reader to have the other mathematic theory preliminaries except the basic set-theory.

6 Conclusion and Future Works

Based on the state-based semantics of a kernel subset of CCSL, We have presented a sufficient condition to discover the CCSL divergence existence, and an easily constructed Bounded Clock Set (BCS) for deciding the convergence of CCSL. An algorithm is proposed to actually build BCS of a given specification with the help of sorted the bounded clock chain with respect to causality relation and the clock delay expression used to decide clock pair’s boundary. Therefore, determining boundedness among all clock pairs is converted into checking boundedness on much fewer clock pairs and additionally sorting clocks with respect to causality relation. Finally, a simple application’s convergence is investigated. We first discover its divergence by the existence of unbounded clock causality chain. Consequently, a BCS is built to ensure the new specification is convergent by adding suitable constraint.

As a future work, we plan to extend and prove the extensive application of clock causality chain further. For instance, the potential causality conflict between clocks may be found if the specification is not deadlock-free or ill-formed, the periodicity in a schedule may be revealed in the chain in some style, etc.