Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

The previous chapters have presented a symbolic representation and on top of that different extensions for the validation and verification of structural as well as behavioral aspects of models. However, apart from modeling these two aspects, system design consists of lots of specialized problems, e.g., timing or power consumption. Developing dedicated modeling tools for each of these problems would be cumbersome, impossible to keep compatible to each other, and unaffordably expensive. But the approaches introduced in the previous chapters can be utilized to also handle those specialized problems. In this chapter, timing constraints will be used as an example to show how the methods from above can be used to cope with a very specialized topic, i.e., timing, re-using the symbolic representation with its extensions.

To this end, we first need to review how timing can be described in a UML/OCL-like fashion. In fact, in UML2 it is possible to define profiles to extend the language to be able to address nearly all kinds of specific topics. One example is the Modeling and Analysis of Real-time and Embedded systems (MARTE) [Obj11] profile to support model-driven development (for real-time embedded systems). Along with the growing impact of modeling on the general domain of system design, especially the influence of specialized profiles such as MARTE is steadily increasing during the last decades. Within MARTE, the Clock Constraint Specification Language (CCSL) [Obj11] provides a formal description of timing constraints, also called clock constraints, which have to be enforced on the considered system. This chapter considers the specification of timing behavior using MARTE/CCSL.

Timing is an essential part of a specification and particularly of interest in all cases where the question “when?” is asked. Specifying timing behavior is complex, because it needs to provide a clear definition of time, clocks to access time, and relations between all of them. MARTE/CCSL allows for a precise specification of all those timing aspects in complex systems. This builds the basis for the next design steps and can be used, e.g., to, first, check whether the timing constraints are consistent, plausible, and indeed have been specified as intended, second, generate code which actually realizes the desired timing behavior, as well as, third, proving whether the time constraints have correctly been implemented at lower abstraction levels. In the recent past, very powerful and complementary methods addressing these tasks have been proposed, e.g., in [MY12, SY12, YML11, AMD10, PWD14].

These methods, however, usually rely on a translation and interpretation of the CCSL descriptions in some different computational model or language. Generating this is a laborious and, at the same time, highly critical task in which any error will spoil the validity of the respective results. Thus far, researchers approached this challenge by providing translation schemes for single application scenarios only. For example, checking CCSL as introduced in [MY12, SY12, YML11, AMD10] relies on a direct encoding of the constraints, e.g., into Promela- or UPPAAL-syntax. Code generation as proposed in [PWD14] directly creates SystemC code. That is, for each design task usually a different translation and interpretation of CCSL constraints is applied—although all of them eventually shall rely on the same semantics.

Moreover, in most of the existing approaches, the non-functional behavior of the system is not explicitly considered. This constitutes a significant drawback since, e.g., methods such as [LLH05, CCR09, Gog+14, EQF12, Wil+13] which are aiming for proving the correctness of corresponding models do not support CCSL constraints. Vice versa, CCSL checkers as introduced in [MY12, SY12, YML11, AMD10] do not consider the functional behavior. That is, functional and timing constraints are usually checked independently of each other. Consequently, design flaws caused by the combination of both constraints are often not considered before an initial implementation is available. Other design tasks such as code generation similarly suffer from the current state-of-the-art: For example, the realization of CCSL timing constraints in SystemC as described in [PWD14] relies on the fact that the entire functional description of the system is already implemented.

Overall, the “inflation” of solutions for rather specific design tasks and, at the same time, their inability to combine them with tools for functional code generation and verification significantly limits the application of CCSL timing constraints in practice.

Therefore, after Sect. 6.1 provides preliminaries about MARTE/CCSL, Sect. 6.2 aims for a generic representation of the CCSL constraints which (1) can be used for various purposes such as verification, code generation, and, moreover, (2) can easily be integrated and merged with corresponding representations of the functional behavior of the system under consideration. To this end, a transformation scheme is proposed which takes CCSL constraints and maps those into an equivalent representation in terms of a transition relation (or in other words an automaton). Afterwards, the resulting transition relation can easily be integrated into the existing solutions for design tasks as described in previous chapters (using the findings from [Pet+15]).

In Sect. 6.3, instant relations as an additional description mean of the CCSL are introduced. Instead of using instant relations for monitoring purposes only, the constraints (derived from the instant relations) are considered as properties to be satisfied by the clock constraints. Based on this interpretation, a methodology is introduced (based on [Pet+16]) which is capable of verifying clock constraints against the given instant relations. To this end, the timing behavior is again represented in terms of an automaton followed by its verification through satisfiability solvers. By this, a verification scheme becomes available which is capable of checking whether the timing behavior of a system has been specified in CCSL as intended. A case study illustrates the application of the proposed methodology.

6.1 Preliminaries About Clocks and Ticks

Like for the UML/OCL models (i.e., class diagrams for this book) a formal definition of the CCSL is needed to apply formal methods. Consequently, this subsection aims to formally define the constructs of the CCSL time model. A central part of the underlying time definition are instants, i.e., moments in the raw, unordered time, defined by clock ticks. The clock is an instrument to access a set of instants [AM08].

Remark 9

Note that some of the symbols and notations which are used in the section are shared with the UML/OCL model notations. However, from the context it will be always clear which interpretation is utilized for a symbol with a double meaning.

Definition 6.1

A clock \(c=\langle \mathcal {I}, \prec , \mathcal {D}, \lambda , u\rangle \) consists of a set of instants \(\mathcal {I}\), which owns a quasi-order relation ≺, a set of labels for the instants \(\mathcal {D}\), a labeling function λ, and a unit u for the clock ticks. A finite clock has a finite number of ticks. If no ticks are left, the clock is empty. A clock \(c_1=\langle \mathcal {I}_1, \prec _1, \mathcal {D}_1, \lambda _1, u\rangle \) is a subclock of another clock \(c_2=\langle \mathcal {I}_2, \prec _2, \mathcal {D}_2, \lambda _2, u\rangle \), if \(\mathcal {I}_1\subseteq \mathcal {I}_2\).

This definition shall be illustrated with the following example:

Example 44

Consider a sensor which can perform measurements at certain times. The time steps to perform a measurement can be described using the clock sensor1. They form a set of instants of the clock which are illustrated by dots at the time line shown in Fig. 6.1. Every instant represents a clock tick. These ticks represent time steps in which a measurement may be conducted. The order of the instants on the line is specified by ≺ sensor1 . Finally, the time steps in which a measurement does actually take place are labeled by a corresponding ID (in Fig. 6.1, denoted below the dots representing the instants).

Fig. 6.1
figure 1

An exemplary time line of a clock sensor1

Full size image

In general, clocks can be logical or chronometric [Obj11]. Logical clocks can refer to discrete events like processor cycles or sensor data, while chronometric clocks refer to physical time and can also be dense. In this section, discrete clocks are considered. From the clocks, a time structure can be derived [AM08]:

Definition 6.2

A time structure is a pair \(\langle \mathcal {C},\preccurlyeq \rangle \), where \(\mathcal {C}\) is a set of clocks and \(\preccurlyeq \) is a binary relation on \(\bigcup \limits _{c\in \mathcal {C}}\mathcal {I}_c\) named precedence (one clock tick takes place before or coincidentally with the other). From \(\preccurlyeq \), some further relations can be derived to specify instant behavior.

These instant relations affect the instants to which they are referring to, but not the rest of the instants of the clock. In contrast, if instant relations are defined for all instants of the clock, they become clock relations (or clock definitions, in terms of CCSL). These clock relations constrain the complete behavior of the clocks. An illustration of clock relations is given in the following example. A complete list of clock constraints can be found, e.g., in [Obj11].

Example 45

Consider a system with two sensors triggered by the clocks sensor1 and sensor2. Both sensors have to reply in every second step with respect to a third (minimal) clock minClock. From its second reply on, sensor1 causes an echo interfering with the signal of sensor2. Hence, this echo and the reply of sensor2 are not allowed to occur coincidentally. This is described in the CCSL specification in Listing 6.1.

At the beginning, the clocks are defined (Lines 1–5). Clock echo in Line 5 is defined as a subclock of sensor1. Both tick together, but echo starts one tick after sensor1. Afterwards, the clock relations are applied. Line 7 states the exclusion of echo and sensor2, while Lines 8 and 9 define the periodicity of sensor1 and sensor2 on minClock.

Listing 6.1 A CCSL specification

6.2 A Generic Representation of CCSL Constraints

Description means as the clock constraints described above allow for a very precise specification of the timing behavior for a system to be realized. The resulting formal descriptions can already be utilized to automatically perform design tasks such as consistency checking, code generation, or verification. For this purpose, a variety of solutions have been proposed in the recent past [MY12, SY12, YML11, AMD10, PWD14]. A typical step involved in most of these approaches consists of transforming the given specification or a part thereof into a corresponding representation such as Promela, SystemC, etc. The first goal of this section is to represent the non-functional timing constraints (provided in CCSL) in terms of a more generic representation which is applicable to existing design approaches for the tasks mentioned above but can also easily be integrated to solutions addressing only functional behavior thus far.

The idea of the proposed representation is to model the timing behavior by means of so-called ticking sets. A ticking set describes all clocks \(c\in \mathcal {C}\) which can tick in a certain time step. Clocks that are not included in a ticking set will not tick in the respective time step. Relying on such a description, the entire timing behavior can be represented as a sequence of ticking sets: Each ticking set constitutes a state; transitions allow for moving from one state to another in accordance with the constraints originally provided in CCSL. For this purpose, transitions may have guard conditions over global variables (such as counters for periodic behaviors) which state whether a transition may be taken or not. The values of these global variables may be changed during a transition by means of update functions. The given CCSL constraints shall be represented in terms of a transition relation given by an automaton A defined as follows.

Definition 6.3

Let \(\mathcal {C}\) be a set of clocks given by a CCSL specification. Furthermore, let V be a set of global variables Footnote 1 used to store additional information (e.g., counters) and V an assignment of them. In order to evaluate conditions derived from the CCSL constraints, a guard function g is applied which maps the current assignment V to either true or false. the values of V . Then, the behavior of the clocks according to a given CCSL specification can be represented by an automaton \(\mathcal {A} = (\varSigma , S_0, {{\mathcal {V}} }, V_0, \delta )\) where

  • \(\varSigma \subseteq \mathcal {P} ({{\mathcal {C}} })\) are the states referring to possible ticking sets,

  • S 0 ⊆ Σ are the initial states,

  • V is a set of global variables,

  • V 0 is an initial assignment of V , and

  • \(\delta \colon \sigma \overset {g,u}{\longmapsto } \sigma '\) is a relation representing all transitions from a source state σ ∈ Σ to a target state σ′∈ Σ with guard condition g and update function u.

Obviously, a transition can be used only if the guard function evaluates to true.

Example 46

Figure 6.2a shows a CCSL constraint defining the timing behavior of two clocks A and B being periodic. A corresponding transition relation representing this timing behavior is provided by the automaton shown in Fig. 6.2b. More precisely, from the periodicity of A on B one can conclude that A is a subclock of B, i.e. A can never tick alone. Hence, the set Σ of states to consider is composed of the ticking sets {B} and {A,B} only. In addition to that, a counter variable c A and a Boolean variable d A are utilized in order to buffer the actual period as well as to monitor whether A has already ticked. Relying on the assignments of these variables, the transitions δ between the respective ticking sets can be conducted as indicated in Fig. 6.2b.

Fig. 6.2
figure 2

Generic representation. (a) CCSL constraints. (b) Corresponding automaton

Full size image

6.2.1 Determining the Generic Representation

While the generic representation as recently introduced allows for manifold applications, a structured approach is required to automatically determine this automaton from given CCSL constraints. This section outlines a possible scheme for this purpose. A discussion of the benefits and drawbacks as well as an exemplary evaluation of the proposed approach is later provided in Sect. 6.2.2.

6.2.1.1 Initializing the Automaton

First, an initial structure for the automaton is created, i.e., an initial set of states which may have to be considered is generated. A clock \(c\in {{\mathcal {C}} }\) may either tick solely or in conjunction with one or more other clocks. Hence, in the worst case, for each possible subset of clocks, an own state may be required.Footnote 2 Additionally, it is assumed that, in each state, at least one clock is supposed to tick, i .e., there is no “empty” state. Overall, this leads to an initial set Σ of states formed over the power set of all the clocks in \(\mathcal {C}\):

$$\displaystyle \begin{aligned} \varSigma \leftarrow \mathcal{P}(\mathcal{C})\setminus\{\emptyset\}. \end{aligned} $$

In a similar fashion, it is initially assumed that an arbitrary clocking behavior is allowed and, thus, a transition from each ticking state to any other ticking state is possible. Guard conditions and update functions are initially assumed to always evaluate to true and to employ the identity, respectively:

$$\displaystyle \begin{aligned} \delta \leftarrow \{ \sigma \overset{g,u}{\longmapsto} \sigma' \mid \sigma,\sigma'\in\varSigma, g(V) = {\mathtt{true}}, u = {{\operatorname{id}}}_V \} \end{aligned} $$

Hence, the automaton is initialized as a complete graph over the power set of all clocks in \(\mathcal {C}\).

Example 47

In the remainder of this section, the necessary steps are illustrated by means of the CCSL constraints given in Listing 6.1. This specification of timing behavior is composed of the clocks \({{\mathcal {C}} }=\{\mathtt {sensor1}, \mathtt {sensor2}, \mathtt {minClock},\) echo}, leading to a set Σ composed of 15 states for the desired automaton. Each state is connected to all of the remaining states eventually leading to the initial structure as shown in Fig. 6.3a. Note that the names of the clocks have been shorted, i.e., sensor1, sensor2, minClock, and echo have been abbreviated by s1, s2, mC, and e, respectively.

Fig. 6.3
figure 3

Determining the generic representation. (a) Initial structure of the automaton. (b) Applying subclock constraints. (c) Removing transitions. (d) Determining initial states. (e) Refining guard conditions and update functions

Full size image

6.2.1.2 Applying Constraints

Once the initial structure of the automaton is generated, the constraints are applied to it. For every CCSL constraint, it is checked whether it states a subclock relation (denoted by ⊆) between two clocks. For all clocks \(c_1,c_2\in {{\mathcal {C}} }\) with c 1 ⊆ c 2, all states containing the subclock but not the superclock are removed. This means, the set of states is adjusted for each c 1 ⊆ c 2 as follows:

$$\displaystyle \begin{aligned} \varSigma\leftarrow\varSigma\setminus\{s\in\varSigma\mid c_1\in s\wedge c_2\notin s\} \end{aligned} $$

Furthermore, states containing two clocks excluding each other (denoted by #) are removed. Hence, for all clocks \(c_1,c_2\in {{\mathcal {C}} }\) with c 1 #c 2 the set of states is adjusted as follows:

$$\displaystyle \begin{aligned} \varSigma\leftarrow\varSigma\setminus\{s\in\varSigma\mid c_1\in s\wedge c_2\in s\} \end{aligned} $$

Obviously, the ingoing and outgoing transitions of all dropped states are removed as well.

Example 48

In the considered example, the constraints isPeriodicOn and delayedBy indicate subclock relations (see Lines 5, 8, and 9 in Listing 6.1), i.e., the periodic clocks sensor1 as well as sensor2 are both subclocks of minClock and echo is a subclock of sensor1. Hence, all states containing sensor1 or sensor2 but not minClock as well as all states containing echo but not sensor1 are removed. Moreover, the clocks echo and sensor2 exclude each other (see Line 7 in Fig. 6.2a), so that all states containing both are removed as well. The resulting automaton is shown in Fig. 6.3b.

At this stage, some more transitions can be removed. In fact, certain CCSL constraints may reveal that clocks cannot tick directly after each other. Thus, transitions between states containing these clocks can be removed. Although this can also be handled later when guard conditions are refined (which would never evaluate to true for such transitions), dropping them before simplifies the remaining steps significantly.

Example 49

Consider the isPeriodicOn-constraints of the example (see Lines 8 and 9 in Listing 6.1). Since the periods are greater than 0, it can be concluded that there can never be a valid transition between two states containing the respective subclock. Hence, all transitions from states containing sensor1 to states containing sensor1 are removed. The same happens with transitions from/to states containing sensor2. The resulting automaton is shown in Fig. 6.3.

Next, the initial states are determined. At the beginning, all states are assumed to be initial states. However, all clocks which are dependent from other clocks (i.e., have to wait for other clocks) obviously cannot initiate the timing behavior. Hence, whenever a CCSL constraint states that a clock \(c\in \mathcal {C}\) is dependent on another clock \(c'\in \mathcal {C}\) (e.g., clocks with an offset have to wait for a triggering clock tick), all states including c are not considered an initial state. Formally, the initial states are defined by

$$\displaystyle \begin{aligned} S_0 \leftarrow \varSigma\setminus\{\sigma\in\varSigma \mid {\exists \, }\,c\in\sigma : c \text{ depends on } c'\in{{\mathcal{C}} }\setminus\{c\}\} \end{aligned} $$

Example 50

Thus far, all five states left in the automaton and shown in Fig. 6.3 are assumed to be initial states. However, there exists a dependency between two clocks: echo has to wait until sensor1 has ticked one time. As a consequence, all states including the clock echo cannot initiate the timing behavior and, hence, they are not considered to be initial states. Figure 6.3 shows the resulting automaton.

Finally, the guard conditions g and the update functions u for the transitions are refined with respect to the CCSL constraints. For this purpose, the set \({{\mathcal {V}} }\) of global variables is initialized with

  • natural numbers ℕ which are applied as counters, e.g., to control periodicity or delays as well as

  • Boolean variables 𝔹 which are applied to monitor whether a clock has already ticked or not.

For all variables, the initial assignment is added to V 0. Then, for all transitions we refine g and u depending on the respective constraints. For this purpose, a rather direct mapping as illustrated in the following example is applied.

Example 51

The guard conditions and update functions for the transitions which remained in the automaton shown in Fig. 6.3 have to be refined. While the excluding constraint (Line 7 in Listing 6.1) has already been handled above (by excluding the corresponding states from the automaton at all), this particularly requires the consideration of the isPeriodicOn and delayedBy constraints (see Lines 5, 8, and 9 in Listing 6.1).

These constraints obviously require a counter variable \(c_{\mathrm{clock}}\in {{\mathbb {N}} }\) (in order to check whether the period or the delay has been completed) and a Boolean variable d clock (in order to store whether the restricted clocks have ticked before) for each of the restricted clocks clock. Note that, in the example, a clock can either be s1, s2, or e, while the latter just needs a counter and no Boolean variable. Then, states σ ∈ Σ including clock (i.e., with clock ∈ σ) may only be entered either (1) if the period/delay (stored in c clock) satisfies the respective CCSL constraint or (2) if clock has simply not ticked yet (stored in d clock). In a similar fashion, entering a state σ ∈ Σ sets the existing d clock-variables for all clock ∈ σ to true (since all clock ∈ σ are ticking in the following step) and leaving such states updates the corresponding c clock-variables. For the latter, this means either resetting the counter (if the corresponding clock just ticked in σ) or increasing it by one (if the corresponding reference clock ticked).

Overall, this leads to a revision of the guard conditions and update functions as shown in Fig. 6.3.

Following the scheme described above, almost all CCSL constraints can automatically be mapped into the generic representation. An exception is uncontrollable behavior, e.g., clocks ticking according to external sensor input. However, if the automaton satisfies certain characteristics these constraints are automatically satisfied as well. Hence, supporting uncontrollable behavior boils down to a particular verification task which can, e.g., be conducted by established verification methods as discussed in the next section.

6.2.2 Discussion and Application of the Generic Representation

Using the method described above, timing behavior provided in CCSL is generically represented by means of a transition relation. Now, this can be used for various purposes for which only very problem-specific design tools were available thus far. In this subsection, possible application areas of the proposed methodology are discussed and compared to related work. Further, it is explained how the problem is solved using the symbolic formulation for UML/OCL models as presented in the last chapters. Afterwards, the feasibility of the approach is exemplary demonstrated by means of the running example.

6.2.2.1 Application and Comparison to Related Work

An important issue after the specification of timing constraints is to check, e.g.,

  • whether the resulting CCSL constraints are consistent, i.e., do not contradict each other and thus allow for an execution of the clocks without deadlocks, as well as

  • whether they indeed have been specified as intended.

To conduct these checks, a few approaches have been proposed previously (cf. [MY12, SY12, YML11, AMD10]). Here, each constraint is represented by a single automaton. Moreover, they represent ticking sets in terms of transitions rather than states. For some constraints, this leads to an infinite number of states. To deal with that, the authors of [MY12, SY12, YML11, AMD10] restrict the number of transitions.

The proposed solution approaches this problem from a different direction which allows for an easier consideration of many verification tasks. It relies on a finite representation from which serious design flaws can directly be detected. For example, if CCSL constraints result in an automaton composed of states with no outgoing transitions (or outgoing transitions which will never satisfy the guard conditions), a typical deadlock scenario is identified.

In addition to that, well-known and powerful methods for (bounded) model checking (e.g., [LLH05, CCR09, SWD11c, Gog+14]) can directly be applied on the obtained transition relation in order to check more sophisticated properties. Moreover, the obtained generic representation obtained by our approach can directly be combined to a transition relation representing the functional behavior of a system (obtained, e.g., by approaches as proposed in [SWD11c, Gog+14]). In doing so, non-functional timing constraints can be considered together with functional specifications. Particular for generic verification frameworks as envisioned, e.g., in [Wil+13, HPW15, Hil+14a], this is an important benefit.

Another important use case for CCSL descriptions is code generation, i.e., the derivation of a proper implementation of the specified timing behavior. A practical approach for this purpose has recently been presented in [PWD14]. However, this solution relies on a rather heavy data-structure as well as a complex analysis scheme including, e.g., a categorization, several lists, etc. In contrast, the generic representation of timing constraints proposed in this work provides an easy and obvious basis for code generation. In fact, once an automaton has been found to be correct, it can directly be translated into an implementation by (1) mapping all states to an encoding in terms of state signals (which are connected to the clocks) and (2) mapping all transitions to if-statements ensuring the correct assignment to the state signals.

On the contrary, the proposed approach obviously suffers from the possibly exponential size of the automaton. In the generic approach as described in Sect. 6.2.1, a power set construction is conducted which represents the bottleneck of the solution. However, this worst case behavior can be avoided in many cases. For example, when CCSL constraints as discussed before in Listing 6.1 are considered, it can already be derived that only five states (rather than 24 − 1 = 15) are required. Determining more sophisticated bounds for all possible cases remains an open problem for future work, but certainly provides further room for improvement.

6.2.2.2 Exemplary Evaluation

In order to evaluate the applicability of the proposed approach, the running example considered above (i.e., the CCSL constraints from Listing 6.1) was subject to more detailed investigations. More precisely, we applied the resulting generic description to selected code generation and verification tasks. In order to evaluate the scalability of the generic representation, we additionally did not only consider this example with four clocks (denoted by sensors4), but also derivations including six and eight clocks (denoted by sensors6 and sensors8, respectively). To this end, corresponding CCSL constraints have been added for the newly introduced clocks.

Applying the approach proposed in Sect. 6.2.1 to the resulting CCSL instances yielded generic representations with characteristics as summarized in Table 6.1. The columns denote the name of the instance (Instance) as well as the number of states (States), the number of transitions (Trans.), and the number of variables (Var.). All automata have been derived in negligible run-time, i.e., within a few seconds.

Table 6.1 Characteristics of the resulting automata
Full size table

Afterwards, typical design tasks have been conducted in which the generic representation has explicitly been utilized. Since code generation can be performed by a rather simple mapping scheme (as discussed above), our evaluations on verification are summarized in more detail in the following. The resulting generic description is utilized in order to automatically prove whether

  1. 1.

    the originally given CCSL description is consistent, i.e., allows for a consistent execution at least for a given number of transition steps,

    and

  2. 2.

    the originally given CCSL description is deadlock-free, i.e., no path from an initial state to another state exists from which no further ticks can be executed anymore.

To this end, the generic description has been transformed into a UML/OCL model, more precisely, a model with just one class. This class has one integer attribute to represent the current state, i.e., the ticking set. For this purpose, the remaining states of the automaton are simply enumerated. An additional invariant restricts the valid assignments. To model the transitions, for each remaining transition an operation is added to the class. Furthermore, the guard conditions are mapped to preconditions and the update functions to postconditions. Now, it is possible to utilize the symbolic formulation together with the respective verification.

Tables 6.2 and 6.3 summarize the obtained results for the consistency- and the deadlock-checks, respectively. Again, the first column denotes the name of the instance (Instance), while afterwards the number of considered transition steps (#Steps), the overall run-time (in CPU seconds and obtained on an Intel(R) Core(TM) i5-3320M machine with 2.60 GHz and 8 GB of memory; Run-time), and the result (Res.) is provided. For the last column, a ✓ denotes that consistency/deadlock-freeness has been proven; otherwise, ✗ denotes that a corresponding flaw has been found.

Table 6.2 Verification results (consistency)
Full size table
Table 6.3 Verification results (deadlock)
Full size table

The results confirm the applicability of the proposed approach for verification purposes. In fact, the considered tasks could have been addressed in acceptable run-time and, for a given CCSL constraint, consistency could have been proven by utilizing an existing model checker rather than developing a specific CCSL-based solution. More importantly, the proposed solution even helped unveiling a severe design flaw which was hidden the entire time in the considered running example: The execution of the state sequence {mc}→{mC, s1, s2}→{mC} leads to a deadlock. This is because the periodicity forces s1 and s2 to tick in the next step (mC ticks always), but if s1 ticks, e has to tick as well (because of the delayedBy constraint). The exclusion between s2 and e eventually leads to a contradiction and, hence, no further transition can be taken at that point. While not obvious at a first glance, this flaw can be detected using the proposed generic representation (as indicated by column Res. in Table 6.3). Again, all these results have been achieved without explicitly developing a specific CCSL-checker but entirely relying on existing tools.

6.3 Validation of Clock Constraints Against Instant Relations

Clocks (as defined in Definition 6.1) are used to define sets of uniformed instants. Moreover, special instants satisfying certain conditions can additionally be defined using CCSL statements. These specific instants can be used, e.g., to trigger certain events in the system. More precisely, CCSL allows for defining instants of a clock c in categories such as:

  • Unspecific. An arbitrary instant of the clock (e.g., Instant i1 is myClock;),

  • Fixed. A fixed instant of the clock (e.g., myClock(4) precedes myOtherClock(8)),

  • Relative. A relative instant of the clock (e.g., myClock(i) precedes myOtherClock(i-7)), or

  • Conditional. A conditional instant of the clock (e.g., Instant i1 is myClock suchThat k>14;).

In general, the clocks these instants form can either refer to a constant physical (and possibly dense) time or to logical events, which do not necessarily follow constant timing rules, but can occur with varying periods in physical time. In our scenario, the target system (i.e., SystemC) is discrete and, because of that, can only simulate logical time. The processor clock itself is a logical clock counting cycles. Hence, all times derived and simulated in this context are logical.

If there is more than one clock, all clocks and their respective instants can be structured through instant relations [AM08]:

Definition 6.4

Given a set of clocks \(\mathcal {C}\), a binary instant relation \(\preccurlyeq \) (called precedence) can be defined stating that one instant occurs before or coincidentally with the other. From \(\preccurlyeq \), three further instant relations can be derived, namely

  • precedence (denoted by \(\preccurlyeq \)), i.e., one of the clock ticks takes place before or coincidentally with the other tick (e.g., i 1 precedes i 2),

  • coincidence (denoted by \(\equiv \ \triangleq \ \preccurlyeq \cap \succcurlyeq \)), i.e., two clock ticks take place coincidently (e.g., i 1 coincidentWith i 2), and

  • strict precedence (denoted by \(\prec \ \triangleq \ \preccurlyeq \backslash \equiv \)), i.e., one of the clock ticks takes place strictly before and not coincidentally with the other tick (e.g., i 1 strictly precedes i 2).

Listing 6.2 CCSL specification of instants

Example 52

CCSL can be used to describe complex temporal relations. As an example, consider the clocking as already described in Example 44.

Now, more precise statements about the instants of the clocks are given in Listing 6.2. Lines 1–2 denote that the ith tick of sensor1 is followed by or coincident with the ith tick of sensor2 and is again followed by or coincident with the (i + 1) th tick of sensor1. In the CCSL statements, the same is stated in lines 4–5 for the kth and (k + 1) th tick of sensor2 and the kth tick of sensor1. Figure 6.4 illustrates the relations. Obviously, all relations could only be satisfied, if sensor1 and sensor2 tick coincidently.

Fig. 6.4
figure 4

Instant relations with two precedes statements

Full size image

Instant relations only affect the instants to which they are referring to, not the clocking behavior itself. Because of that, no behavior can be derived from the instant relations and enforcing instants to appear is not possible. Consequently, the clock constraints represent the actual clocking behavior while instant relations provide a more detailed description of the intended timing behavior. Thus, instead of generating behavior, instants are up to now applied by some approaches to monitor the timing behavior and to report unwanted behavior (e.g., a meltdown instant) [PWD14]. Respectively, from the clock constraints indeed the actual behavior can be derived as described, e.g., in [PWD14] or as recently explained in Sects. 6.1 and 6.2.2.

6.3.1 Motivation and Proposed Idea

In this section, the current exploitation of CCSL for verification purposes is briefly discussed and illustrated. Afterwards, it is discussed how this state-of-the-art can significantly be improved. This eventually motivates the verification methodology proposed in the work. To this end, the following example is considered:

Example 53

A simple satellite application for space systems shall be designed. The satellite shall take photos of the earth and the sun. In between, it has to ensure that its orbit is still correct, i.e., it has to check (and, if necessary, correct) its height. As it has only one camera, it shall alternately take photos of the sun and the earth. The height control is a complex task leaving not enough processor performance for image processing, thus, the satellite cannot take photos and control its height at the same time.

As recently reviewed in the previous subsections, CCSL provides description means to describe the ticking of the clocks to be implemented (in terms of clock constraints). Using these notations, the clock behavior of this system can be specified:

Example 54

Listing 6.3 shows a possible specification of the clocks to be used in order to realize the timing of the satellite application. The clocks photo_earth and photo_sun specified in Line ?? and Line ?? trigger the camera to take a photo of the earth and the sun, respectively. The constraints in Line ?? and in Line ?? respectively ensure that these clocks do not tick at the same time and indeed alternate between each other. Checking height is triggered by clock check_height (Line ??) which must not tick concurrently with the other two clocks as restricted by the last two constraints in Lines ??–??.

Listing 6.3 CCSL description of a satellite

Besides that, CCSL allows to describe certain timing behavior which is intended to be executed on the realized system. To this end, detailed constraints over single instants can be specified in terms of instant relations:

Example 55

In order to further refine the specification of the satellite application, instant relations as depicted in Listing 6.4 are added. They state that between a tick of photo_sun and the consecutive tick of photo_earth the height shall be checked, i.e., clock check_height shall tick. This is expressed by two strict precedence instant relations. The identifier for the instants are the indices i and j. The two consecutive instants of photo_sun and photo_earth are the ith ticks of their clocks, while the control_height tick in between is the jth tick of its clock.

Listing 6.4 CCSL instant relations

Eventually, a CCSL description results which, using, e.g., the recently introduced generic automaton approach or approaches as presented in from [MY12, YML11], can be checked for consistency. However, whether the intended behavior as specified by the instant relations from Listing 6.4 can indeed be realized considering the clock constraints from Listing 6.3 is not covered by these verification methods. Instead, the state-of-the-art methodology continues with an implementation of the timing constraints (e.g., using code-generation approaches such as [PWD14]). As this might result in the creation of monitors (as, e.g., suggested in [PWD14]), corresponding checks can be conducted after the implementation has been finalized.

Obviously, this causes a significant drawback: Checking the intended timing behavior is considered rather late in the design process, namely not until a fully-fledged implementation is available. If it turns out that the intended behavior is not possible, re-spins of the implementation or even the CCSL specification have to be conducted. This leads to long debugging loops and poses a serious threat to time-to-market constraints.

Motivated by this, an alternative methodology is proposed. It aims for verifying at the CCSL level, i.e., prior to implementation, whether the given descriptions allow for the intended timing behavior. To this end, a slightly different interpretation of the CCSL description means is applied. Instead of considering instant relations as behavior to be monitored, they are applied as properties to be satisfied by the clock constraints. Based on this, a verification methodology is proposed whose general idea rests on three main steps:

  1. 1.

    Formulating the properties to be checked according to the instant relations

  2. 2.

    Deriving a symbolic representation of all possible ticking behavior of the clocks according to the clock constraints

  3. 3.

    Checking whether the resulting symbolic representation indeed satisfies the properties derived from the instant relations

In the remainder of this section, the implementation and application of this general idea is described and discussed, respectively.

6.3.2 Implementation

We start with a description of the three steps to be conducted in order to verify instant relations against clock constraints. All steps are illustrated by means of the satellite example from above.

6.3.2.1 Formulating the Properties

Single instant relations already provide a formal description of timing behavior to be verified. However, as they may be connected to each other (cf. Example 55), a sole consideration may not provide a sufficient verification objective or property to be verified. In fact, an instant relation is only satisfied, if all other relations connected to it are also satisfied. Hence, a property to be checked has to be composed of a group of instant relations. To this end, the following definition and notation of an instant group is used:

Definition 6.5

Let i be an instant and \(\oplus \in \{\equiv ,\prec ,\preccurlyeq \}\) an instant relation symbol. Let further (i j  ⊕ k i l ) be an instant relation and \(\mathfrak {I}\) the set of all instant relations. Then, an instant group \(\mathcal {I}\) is a set of instant relations such that

$$\displaystyle \begin{aligned} {\forall \, } \, (i_1 \oplus_1 i_2)\in\mathcal{I}: {\exists \, } \, (i_3 \oplus_2 i_4)\in\mathcal{I}: \{i_1,i_2\}\cap\{i_3, i_4\}\neq\emptyset. \end{aligned} $$

An instant group is maximal, iff

$$\displaystyle \begin{aligned} {\forall \, } \, (i_1 \oplus_1 i_2)\in\mathcal{I}: {\nexists \, } \, (i_3 \oplus_2 i_4)\in\mathfrak{I}: (\{i_1,i_2\}\cap\{i_3, i_4\}\neq\emptyset) \wedge (i_3 \oplus_2 i_4)\notin\mathcal{I} \end{aligned} $$

Example 56

Consider again the instant relations from Listing 6.4. Since both relations are connected by the instant control_height, they finally form one group. This eventually results in an instant group as shown in Fig. 6.5 and, hence, a property to be verified.

Fig. 6.5
figure 5

An instant relation group

Full size image

6.3.2.2 Deriving a Symbolic Representation

Next, a symbolic representation of all possible clock tickings is required. To this end, the recently presented approach is utilized again.

Example 57

Consider again the clock constraints from Listing 6.3. The corresponding automaton representation is provided in Fig. 6.6. As no clock can tick together with another clock, only three states have to be considered (one in which each clock is allowed to tick). The states control_height and photo_earth are initial states—the third one cannot be an initial state because of the alternatesWith-statement. The guard and update conditions consider additional Boolean variables b alt (denoting who ticks next) and f (denoting if this is the initial alternation) which direct the alternation between photo_earth and photo_sun and are initially both set to true. This ensures that the clock photo_earth ticks first and, afterwards, the states photo_earth and photo_sun are only reached if the respective other clock has ticked before.

Fig. 6.6
figure 6

Automaton representing the CCSL

Full size image

6.3.2.3 Checking the Properties

Having the automaton, all clock ticking behavior which is possible according to the clock constraints is available in a symbolic fashion. Now, it has to be verified whether this ticking behavior indeed allows for the execution of a sequence of clock ticks which satisfies the property given by the instant group. To this end, the SMT-LIB realization for the generic automaton is exploited such that an SMT-LIB instance considering the following question is derived: “Is it possible to execute a sequence defined by the instant group on the automaton derived from the clock constraints?”

6.3.2.4 Creating the Instance

In order to formulate the corresponding instance, the execution of a sequence of clock ticks is symbolically considered. Each step in this sequence is denoted as a (symbolic) simulation step in the remainder of the section. All possible clocking ticks are encoded in terms of variables to be assigned by the SMT solver. For each clock \(c\in \mathcal {C}\), the following variables are introduced and added to the sequence for every simulation step:

  • A Boolean variable t c representing whether c does tick (t c  = 1) or does not tick (t c  = 0) in the current step.

  • An integer variable ind c representing the index of the current tick of the clock c. The variable is initially undefined and set to 0 when c ticks first. Afterwards, its value is increased by 1 with any further tick.

Additionally, another integer variable step is introduced which serves as counter for the respective (symbolic) simulation steps. For the formulation, it is assumed that a maximum number \(step_{\max }\) of simulation steps to be considered is available.

Finally, constraints are added to enforce the satisfiability solver to choose the variable assignments in the consecutive simulation steps according to the behavior of the automaton. This yields an instance representing all possible ticking sequences of length \(step_{\max }\) which is allowed by the clock constraints.

Example 58

Consider again the clock constraints from Listing 6.3 and the instant group from Listing 6.4. In Fig. 6.7, a possible simulation sequence including the introduced variables is depicted. The assignments represent the simulation of the following clock ticks:

$$\displaystyle \begin{aligned} \mathtt{\{photo{\_}earth\} {\rightarrow} \{control{\_}height\}\ {\rightarrow} \{photo{\_}sun\}}. \end{aligned}$$

The variable step counts the simulation steps and, thus, increases with each step. For each step, the assignments to t c , c ∈{ps, ch, pe} (representing the clocks photo_sun, control_height, photo_earth), state the ticking clocks. For example, in the first step, photo_earth ticks, hence t pe is assigned 1, while t ps and t ch are assigned 0. Correspondingly, the index variable for clock photo_earth, i.e., ind pe is initialized with 0.

Fig. 6.7
figure 7

Additional variables for instant checking

Full size image

Note that, for illustration purposes, the example above as shown in Fig. 6.7 considers particular assignments. However, in order to symbolically represent all possible sequences of simulation steps, the created satisfiability instance is composed of un-assigned variables only. The precise assignment has to be determined by the satisfiability solver.

6.3.2.5 Adding the Properties

Simply passing the satisfiability instance created thus far to a satisfiability solver would simply yield an assignment representing an arbitrary sequence of simulation steps possible by the clock constraints. However, we are interested in a dedicated sequence which shows the executability of a considered instant group. Hence, additional constraints are added to the satisfiability instance enforcing the solver to choose assignments in this regard.

The instant relation groups refer instants with certain indices. This means, one need to extract the corresponding state number of the referred instants and to check whether the ordering of the obtained state numbers follows the constraints from the instant relations.

To extract the state number for a certain index, for all clocks and all \(step_{\max }\) simulation steps, an Integer variable c i with \(0 \leq i \leq step_{\max }\) is added for each \(c\in \mathcal {C}\) denoting the simulation step number of the ith tick of c. To model these ith ticks, special constraints are added to the SMT solver. The considered property extracts the variables c i from the encoded instance and connects them by precedence or coincidence statements. Hence, the connection between the corresponding c i is restricted using simple comparison-statements to model precedence (≤), strict precedence (< ), or coincidence (=).

The final verification task is then to check the following statement:

$$\displaystyle \begin{aligned} {\exists \, } \, k\in 0\leq k\leq step_{\max}: \left[\!\left[\mathcal{I}\right]\!\right]_k \end{aligned} $$

where \(\left[\!\left[ \mathcal {I}\right]\!\right]_k\) is the evaluation of the instant relation group concerning the given index k as the index variable from the CCSL specification,Footnote 3 e.g., (A 2 < B 3) for k = 2 and A(k) strictly precedes B(k+1). This means that the concerning index variables c i connected by the relations are chosen for every k concerning the definition in the CCSL statements.

Example 59

Consider again the instance from Example 58. Now, additional variables are created for each clock, e.g., pe 0, pe 1, pe 2, … for photo_earth, which denote in which step this clock has been ticked for the 0th, 1st, 2st, etc. time. For example, the variable pe 0 pointing to step = 0 as illustrated in Fig. 6.7 states that the 0th tick occurred in step 0. The variables without assignment (as shown in the bottom of Fig. 6.7) simply state that their respective tick has not been conducted yet.

Having this formulation, the order of clock ticks is symbolically described. Now, this can be constrained in a fashion that a particular order (namely as given by the instant group) is enforced. Considering the instant group from Listing 6.4, this requires constraining the variables ps 0, ch 0, and pe 0. In fact, as the corresponding clock tickings are restricted by strictly precedes statements, the following constraint has to be employed:

$$\displaystyle \begin{aligned} (ps_0<ch_0) \wedge (ch_0<pe_0). \end{aligned}$$

6.3.2.6 Solving the Instance

The instance is now given to a satisfiability solver which tries to determine an assignment satisfying all constraints. If such an assignment can be determined the corresponding values of each variable can be translated back to a particular sequence of simulation steps. This works as witness demonstrating that the behavior defined by the instant group indeed is possible with the additionally considered clock constraints. Footnote 4

In contrast, if the satisfiability solver proves that no assignment exists which satisfies all constraints, it has been shown that no sequence of \(step_{\max }\) simulation steps exists which satisfies both, the clock constraints and the constraints enforced by the instant group. In this case, \(step_{\max }\) can be increased, e.g., until the diameter of the automaton is reached or until the expected maximum number of time steps the behavior is supposed to become evident is reached. If this still yields no satisfiable assignment, it has been proven that the given instant group cannot be executed under the defined clock constraints. This unveils an error in the CCSL specification which can be addressed by the designer prior to the implementation.

6.3.3 Application and Evaluation

Using the method described above, clock constraints can automatically be checked against given instant relations and, hence, the timing behavior can be verified prior to its implementation. In order to confirm the applicability of the proposed methodology, the three steps described in Sect. 6.3.2 have been implemented on top of the proposed Eclipse model finding plugin.

Afterwards, the resulting tools have been applied to the CCSL descriptions from Listing 6.1/6.2 (denoted by sensors) as well as from Listing 6.3/6.4 (denoted by alternates). In order to evaluate correct as well as incorrect specifications, different variations of the first example have been considered (distinguished by the suffix corr and incorr, respectively). Furthermore, the later example (sensors) has been considered with a different amount of sensors (and, hence, clocks to be considered).

The results of the application are summarized in Table 6.4. The first columns provide the name of the respective example including its number of clocks (Clk.), number of instants (Inst.), number of instant relations (Rel.), and the eventually resulting number of instant groups (Grp.) derived from the respectively given CCSL representation (derived in Step 1 of the proposed methodology; see Sect. 6.3.2.1).

Table 6.4 Behavioral analysis for instant relation groups
Full size table

The results from the second step, i e., from the derivation of the automaton (see Sect. 6.3.2.2) are summarized in the next columns. Here, the number of the states (denoted by States) and the number of transitions (denoted by Trans.) are reported. Note that these numbers only report the size of the final automaton—intermediate results may be significantly larger due to the need to consider all possible subsets of clock tickings in the automaton. Footnote 5

Finally, the result of the third step (see Sect. 6.3.2.3) and, hence, the overall result is presented in the column Res. More precisely, it is denoted whether the instant relations indeed can be realized by the clock constraints or not (denoted by ✓ and ✗ in Column Res.). Furthermore, the total run-time (in CPU seconds) is given.

Overall, the applicability of the proposed approach can be confirmed. In fact, the considered instant relations could have been verified against the given clock constraints in acceptable run-time. More importantly, the proposed solution even helped unveiling design flaws in the examples considered above. In fact, alternates-examples behaved as expected, i.e., the correct instance has been proven correct while the error in the incorrect version has been detected.

Moreover, the sensor-example from Listing 6.1/6.2 (where no error has been introduced on purpose) has also been found erroneous. If the two instant groups are considered separately (as done in the experiments summarized in row sensors1 and sensors2), the clock constraints indeed realize the intended behavior. But enforcing both together (as done in the experiments summarized in row sensors3) would require both clocks (i.e., sensor1 and sensor2) to tick together. This is implicitly prohibited due to the exclusion between sensor2 and echo (cf. Listing 6.1). As a consequence, these instant groups cannot be realized using the clock constraints—the specified behavior is not possible. While not obvious at a first glance, this flaw can easily be detected using the proposed methodology.