Min Zhang

Feng Dai

Frédéric Mallet
email: frederic.mallet@unice.fr

Periodic scheduling for MARTE/CCSL: theory and practice

The UML profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) is used to design and analyze real-time and embedded systems. The Clock Constraint Specification Language (ccsl) is a companion language for MARTE. It introduces logical clocks as first class citizens as a way to formally specify the expected behavior of models, thus allowing formal verification. ccsl describes the expected infinite behaviors of reactive embedded systems. In this paper we introduce and focus on the notion of periodic schedule to allow for a nice finite abstraction of these infinite behaviors. After studying the theoretical properties of those schedules we give a practical way to deal with them based on the executable operational semantics of ccsl in rewriting logic with Maude. We also propose an algorithm to find automatically periodic schedulers with the proposed sufficient condition, and to perform formal analysis of ccsl constraints by means of customized simulation and bounded LTL model checking.

Introduction

Lamport's logical clocks [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] originated from the need to synchronize distributed systems without assuming a reliable single common timing mechanism to compare events. Indeed, maintaining a global clock in a widely distributed system may be very costly. Rather than maintaining a total order on events, a partial view was proposed as sufficient to maintain causal relationships.

In a very different community, synchronous languages [START_REF] Berry | The Esterel synchronous programming language: Design, semantics, implementation[END_REF][START_REF] Benveniste | The synchronous languages 12 years later[END_REF][START_REF] Potop-Butucaru | The synchronous hypothesis and polychronous languages[END_REF] use the word clock to emphasize a multiform notion of time where the notion of physical time is initially relaxed with the notion of ordering. The main important difference is that synchronous languages accept instantaneous causal relations, which are an important abstraction in synchronous circuits but are less relevant in widely distributed environments.

The Clock Constraint Specification Language (ccsl) [START_REF] André | Syntax and semantics of the Clock Constraint Specification Language (CCSL)[END_REF][START_REF] Mallet | CCSL: specifying clock constraints with UML/MARTE[END_REF] proposes a concrete syntax to handle logical clocks as first-class citizens. While synchronous languages mainly focus on signals and values and use logical clocks as a controlling mechanism, ccsl discards the values and only focuses on clock-related issues. In this paper, we focus on the periodic scheduling of ccsl from both theoretical and practical perspectives, considering that reactive embedded systems have recurrent behaviors for which the design of correct periodic schedulers is very important in the development of such systems [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-real-time environment[END_REF][START_REF] Cucu | Periodic real-time scheduling: from deadline-based model to latency-based model[END_REF]. While deciding on the existence of a schedule for a given set of ccsl constraints is still an open problem, we discuss here a sufficient condition for having a class of bounded schedules which can be extended to infinite but periodic ones. In our earlier work [START_REF] Zhang | An executable semantics of clock constraint specification language and its applications[END_REF], we considered a pragmatic point of view and a very restrictive condition for the existence of periodic schedules. We propose here a much less restrictive condition, that (1) allows to find more periodic schedules, ( 2) is less restrictive on the condition to find a periodic schedule, and (3) considers a bigger subset of ccsl constraints. About (3), we consider specifically the periodic filter of ccsl, which offers a generic notion of periodicity on logical clocks that generalizes the classical definition of periodic activation. In this paper, we prove the correctness of our condition and present an operational method for building periodic schedules from a bounded schedule that satisfies the condition.

Furthermore, we also give a formal executable operational semantics of the extended ccsl language using Maude [START_REF] Clavel | All about Maude[END_REF], an algebraic language based on rewriting logic. The formal operational semantics of ccsl was initially defined in a research report [START_REF] André | Syntax and semantics of the Clock Constraint Specification Language (CCSL)[END_REF] in a bid to provide a reference semantics for building simulation tools, like TimeSquare [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF]. Maude provides various formal analysis approaches, such as simulation, state space exploration (exhaustive or bounded, symbolic or explicit-state), by which we can analyze ccsl specifications to, for instance, check the existence of desired schedules with specific properties (e.g., reduce memory usage), produce a schedule or simulation by applying customized scheduling policies, and verify the satisfiability of expected properties.

The benefits of the new semantics defined in rewriting logic are multifold. The first benefit is that rewriting logic gives a direct implementation of the operational semantics while TimeSquare provides a Java-based implementation which is prone to introduce unexpected complexity. The second and most important benefit is that we can directly use the tools that are provided for rewriting logic to analyze a ccsl specification by means of simulation, state-space exploration, and even linear temporal logic model checking. Previous work on studying ccsl properties [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF] relies on several intermediate transformations to automata and other specific formats so that model-checking becomes possible when a ccsl specification is finite. A ccsl specification is called finite if it can be transformed into a finite-state automaton [START_REF] Mallet | Safe CCSL specifications and marked graphs[END_REF]. However, some ccsl operators, which are called unsafe operators, cannot be transformed into finite-state automata. It either meant reducing to a safe subset of ccsl [START_REF] Gascon | Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL[END_REF] or detecting that the specification was describing a finite reachable state-space even though relying on unsafe operators. In this contribution, we rely on the Maude environment [START_REF] Clavel | All about Maude[END_REF] to provide a direct analysis support to ccsl specifications by formally defining its operational semantics in Maude, and we can explore unsafe specifications using bounded model checking and do not restrict to the safe subset.

For periodic scheduling, we provide a prototype implementation in Maude based on the new formal semantics of ccsl to detect the proposed conditions and build the satisfying schedule. As another contribution, we propose five arbitration policies to reduce the set of possible solutions when a ccsl specification is under-specified. Such arbitration policies can be seen as optimization criteria akin to those classically used in real-time scheduling to optimize memory or bandwidth. Those arbitration policies can also be naturally implemented in Maude based on the new formal semantics.

This paper is an extended version of our previous work [START_REF] Zhang | An executable semantics of clock constraint specification language and its applications[END_REF]. Apart from adding much more detail on the formal semantics of ccsl, this extended version adds the following contributions:

1. We consider an operator for the ccsl language that was ignored in previous work, the so-called periodic filter, which serves for the specification of logical repetitive patterns between logical clocks.

2. We propose a less constraining sufficient condition for the existence of periodic schedules and give a formal proof of its correctness.

3. We present a formal executable operational semantics of the extended ccsl language in Maude and illustrate its applications to various formal analysis tasks, such as checking the existence of bounded and periodic schedules, deriving a customized simulation and performing LTL modelchecking.

4. More user-defined arbitration policies are supported for customized simulations of schedules.

The rest of this paper is organized as follows. Section 2 introduces ccsl and the notion of schedule with bounded and periodic restrictions. It also gives conditions for being able to build a periodic schedule, and we prove that those conditions are sufficient. Section 3 gives a brief introduction to Maude. Section 4 discusses the encoding of the semantics of ccsl in Maude and details the way its environment can be used to compute bounded and periodic schedules. Section 5 considers several examples to illustrate the interest of this encoding and the usefulness of our tool. Finally, Section 6 compares this work to previous work, including our own, and Section 7 gives some concluding remarks. While a logical clock can represent any kind of repetitive event, the ticks stand for their successive occurrences. All the events are assumed to be independent, so there is no relationship between the ticks of two clocks unless explicitly defined. ccsl gives a syntax to define such relationships. Concretely, clocks can be used to observe the occurrence of events. In such cases, ccsl describes the expected observations. They can also be used as activation conditions to control the behavior of a system.

ccsl constraints express some relationships between clocks, and their underlying ticks. One possible behavior is captured as a synchronous schedule defined as an infinite sequence of steps. At each step, the schedule defines which clocks tick and which ones do not tick. A ccsl specification characterizes a set of valid schedules. Each constraint potentially reduces the number of valid schedules by forbidding some clocks to tick.

Definition 2 (Schedule). Given a set C of clocks, a schedule of C is a total function δ : N + → 2 C such that at each step n in N + , δ(n) = ∅.
N + denotes the set of all the non-zero natural numbers. By the condition δ(n) = ∅ in Definition 2 we exclude from schedules those trivial steps where there is no clock ticking.

Purely synchronous constraints define when some clocks should tick together and when they cannot, i.e. synchronization conditions. Other more general constraints look at the past, the history (as far as they need) to decide what may happen at a given step.

Definition 3 (History).

A history of a schedule δ over a set C of clocks is a function χ δ : C × N + → N such that for each clock c ∈ C and n ∈ N + :

χ δ (c, n) =    0 if n = 1 χ δ (c, n -1) if n > 1 ∧ c ∈ δ(n -1) χ δ (c, n -1) + 1 if n > 1 ∧ c ∈ δ(n -1)
Intuitively, χ δ (c, n) denotes the number of times that a clock c has ticked before reaching step n in the schedule δ. For simplicity, we write χ for χ δ when the context is clear. This ability to look into the past as far as we need raises reachability problems unusual in traditional synchronous languages, which commonly look only at the preceding step.

In ccsl, there are four primitive constraint operators which are binary relations between clocks, and five kinds of clock definitions [START_REF] Mallet | CCSL: specifying clock constraints with UML/MARTE[END_REF]. The four constraint operators are called precedence, causality, subclock and exclusion; and the five clock definitions are called union, intersection, infimum, supremum, and delay. For simplicity, we call all of them ccsl constraints in this paper. Besides the nine existing primitive operators, we consider a new one called periodic filter. The purely synchronous operators (subclock, exclusion, union, intersection) rely only on the notion of schedule. The other ones rely on history.

Figure 1 shows the definition of the satisfiability of a constraint φ with regards to a schedule δ, which is denoted by δ |= φ. For example, given two clocks c 1 and c 2 , δ |= c 1 ≺ c 2 holds if and only if for each n in N + , c 2 must not tick at step n if the number of ticks of c 1 is equal to the one of c 2 up to step n (not including step n). Intuitively, 'c 1 precedes c 2 ' means that c 1 must always tick earlier than c 2 . Precedence and causality are asynchronous constraints and they forbid clocks to tick depending on what has happened on other clocks in the earlier steps. Subclock and exclusion are synchronous constraints and they force clocks to tick depending on whether another clock ticks or not in the same step. Union defines a clock c 1 which ticks whenever either c 2 or c 3 ticks; intersection defines a clock c 1 which ticks whenever both c 2 and c 3 tick; supremum defines the slowest clock c 1 which is faster than both c 2 and c 3 ; infimum defines the fastest clock c 1 which is slower than both c 2 and c 3 ; and delay defines the clock c 1 which is delayed by c 2 with d steps. Periodic filter is used to define a clock, e.g., c 1 in the figure, which ticks once periodically every p th tick of another clock c 2 . Note that we need m × p -1 because the tick of c 2 at step n is not counted in the history χ(c 2 , n). By construction, c 1 is a subclock of c 2 and is slower than c 2 .

Subclock, exclusion, union and intersection are also called stateless constraints since the tick of a clock at a step only depends on the ticks of other clocks at the same step, while other constraints are stateful, when the ticks of a clock depend on the ticks of other clocks at previous steps.

Given a set Φ of clock constraints and a schedule δ, δ satisfies Φ (denoted by δ |= Φ) if δ |= φ for each φ in Φ. We use δ; k |= φ to denote that δ satisfies φ at step k (k ∈ N + ). That is, δ; k |= φ holds if and only if the counterpart formula of φ in Figure 1 is true after the universally quantified variable n in the formula is eliminated by being instantiated with k. We use δ; k |= Φ to denote that δ satisfies all the constraints in Φ at step k, i.e., ∀φ ∈ Φ.δ; k |= φ.

Bounded and periodic schedules

Given a set Φ of ccsl constraints, deciding if there exists at least one schedule that satisfies Φ is still an open problem. Intuitively, the satisfying schedule may

1. δ |= c 1 ≺ c 2 ⇐⇒ ∀n ∈ N + .χ(c 2 , n) = χ(c 1 , n) ⇒ c 2 ∈ δ(n) (Precedence) 2. δ |= c 1 c 2 ⇐⇒ ∀n ∈ N + .χ(c 1 , n) ≥ χ(c 2 , n) (Causality) 3. δ |= c 1 ⊆ c 2 ⇐⇒ ∀n ∈ N + .c 1 ∈ δ(n) ⇒ c 2 ∈ δ(n) (Subclock) 4. δ |= c 1 # c 2 ⇐⇒ ∀n ∈ N + .c 1 ∈ δ(n) ∨ c 2 ∈ δ(n) (Exclusion) 5. δ |= c 1 c 2 + c 3 ⇐⇒ ∀n ∈ N + .(c 1 ∈ δ(n) ⇐⇒ c 2 ∈ δ(n) ∨ c 3 ∈ δ(n)) (Union) 6. δ |= c 1 c 2 × c 3 ⇐⇒ ∀n ∈ N + .(c 1 ∈ δ(n) ⇐⇒ c 2 ∈ δ(n) ∧ c 3 ∈ δ(n)) (Intersection) 7. δ |= c 1 c 2 ∧ c 3 ⇐⇒ ∀n ∈ N + .χ(c 1 , n) = max(χ(c 2 , n), χ(c 3 , n)) (Infimum) 8. δ |= c 1 c 2 ∨ c 3 ⇐⇒ ∀n ∈ N + .χ(c 1 , n) = min(χ(c 2 , n), χ(c 3 , n)) (Supremum) 9. δ |= c 1 c 2 d ⇐⇒ ∀n ∈ N + .χ(c 1 , n) = max(χ(c 2 , n) -d, 0) (Delay) 10. δ |= c 1 c 2 ∝ p ⇐⇒ ∀n ∈ N + .c 1 ∈ δ(n) ⇐⇒ c 2 ∈ δ(n) ∧ ∃m ∈ N + .χ(c 2 , n) = m × p -1 (Periodicity) $ 1
Figure 1: Definition of the 10 primitive ccsl operators. be an infinite sequence of finite valuations, so it may require to explore an infinite number of states. For example, Figure 2 shows a state-based representation of the schedules that satisfy the constraint c 1 ≺ c 2 [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF]. An arrow from one state to another represents one step and the label of the arrow is the set of all the clocks that tick at this step. An infinite path from the initial state s 0 represents a schedule. For precedence, it needs an infinite number of states to represent all the possible schedules [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF]. In the work [START_REF] Xu | Divergence detection for CCSL specification via clock causality chain[END_REF], such constraint is called divergent. Finding a periodic schedule is a way to have a finite abstraction to characterize this infinite state space.We consider two special kinds of schedules called bounded schedule and periodic schedule from a pragmatic point of view. We show that the existence of a bounded schedule for a set of ccsl constraints among those introduced in the previous subsection is decidable. Additionally, we propose a simple sufficient condition for the existence of a periodic schedule. Definition 4 (Bounded schedule). Given a set Φ of clock constraints on clocks in C and a function δ :

s 0 start s 1 s 2 s 3 . . . {c 1 } {c 2 } {c 1 , c 2 } {c 1 } {c 1 , c 2 } {c 2 } {c 1 } {c 1 , c 2 } {c 2 } {c 1 } {c 1 , c 2 } {c 2 }
N + ≤n → 2 C , δ is called an n-bounded schedule of Φ if for each 0 < i ≤ n, δ; i |= Φ. N +
≤n denotes the set of all the non-zero natural numbers that are less than or equal to n. The satisfiability of an n-bounded schedule with respect to a set Φ of constraints is denoted by δ |= n Φ. It is obvious that given a bound n it is a decidable problem to check if there exists an n-bounded schedule for [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF] for the analysis of ccsl constraints can be considered as a bounded schedule solver because it builds a schedule up to a given number of steps and stops whenever it cannot progress anymore. Bounded schedules are sometimes too restrictive in practice because we usually do not assign a bound to clocks in real-time embedded systems and assume that reactive systems can run forever and only terminate when shut down. Thus, clocks should tick infinitely often from the theoretical point of view. We identify another class of schedules which are unbounded and force all the clocks to occur periodically. We call them periodic schedules.

Definition 5 (Periodic schedule). A schedule δ is periodic if there exist k, p in N + such that for each k ∈ N + and k ≥ k, δ(k + p) = δ(k ).

Figure 3 depicts a periodic schedule whose period is p. Each node denotes a time point, and each plain arrow denotes the elapse of a time unit. The dashed line indicates that, any clock ticking at either end of line also ticks at the other end. From step k, the schedule starts to repeat every p th step infinitely.

It is also an open problem to decide whether there exists a periodic schedule for a given arbitrary set of clock constraints. In the rest of this section, we propose a sufficient condition for the existence of a periodic schedule, and an approach to construct periodic schedules based on bounded ones. Theorem 1. Given a schedule δ : N + → 2 C , a clock constraint φ, and two natural numbers k, k with k > k, then δ |= k φ ⇒ δ; k |= φ if all the following five conditions hold:

1. δ(k ) = δ(k); 2. If φ is in form of c 1 ≺ c 2 or c 1 c 2 , then χ(c 1 , k ) -χ(c 1 , k) ≥ χ(c 2 , k ) - χ(c 2 , k); 3. If φ is in form of c 1 c 2 $ d, then χ(c 2 , k) ≥ d and χ(c 1 , k ) -χ(c 1 , k) = χ(c 2 , k ) -χ(c 2 , k); 4. If φ is in form of c 3 c 1 ∧ c 2 or c 3 c 1 ∨ c 2 , then χ(c 1 , k ) -χ(c 1 , k) = χ(c 2 , k ) -χ(c 2 , k) = χ(c 3 , k ) -χ(c 3 , k); 5. If φ is in form of c 1 c 2 ∝ p, then c 1 ∈ δ(k ) =⇒ (χ(c 2 , k ) + 1) mod p = 0.
Intuitively, condition 1 says that the clocks that tick at step k are the same as those at step k ; condition 2 says that the number of ticks of clock c 1 must be greater than or equal to the one of clock c 2 in a period if they are constrained by causality or precedence; and 3 and 4 say that the number of ticks of clocks that are constrained by a delay, infimum or supremum must be the same in a period. Note that we do not care about what has happened to clocks only constrained by stateless constraints. In addition, if c 1 and c 2 are constrained by a delay, the number of ticks of c 2 up to step k must be greater than or equal to d, as required by condition 3.

Proof. By case analysis:

The stateless (synchronous) constraints only use condition 1, we start with them. [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF], and hence

1. φ ≡ c 1 ⊆ c 2 : δ; k |= c 1 ⊆ c 2 implies that c 1 ∈ δ(k) ⇒ c 2 ∈ δ(k). Obviously, we have c 1 ∈ δ(k ) ⇒ c 2 ∈ δ(k ). Thus, δ; k |= c 1 ⊆ c 2 . 2. φ ≡ c 1 c 2 + c 3 : δ; k |= c 1 = c 2 + c 3 means that c 1 ∈ δ(k) ⇐⇒ c 2 ∈ δ(k) ∨ c 3 ∈ δ(k). It is obvious that c 1 ∈ δ(k ) ⇐⇒ c 2 ∈ δ(k ) ∨ c 3 ∈ δ(k ), and hence δ; k |= c 1 c 2 + c 3 . 3. φ ≡ c 1 c 2 * c 3 : δ; k |= c 1 = c 2 * c 3 means that c 1 ∈ δ(k) ⇐⇒ c 2 ∈ δ(k) ∧ c 3 ∈ δ(k). It is obvious that c 1 ∈ δ(k ) ⇐⇒ c 2 ∈ δ(k ) ∧ c 3 ∈ δ(k ), and hence δ; k |= c 1 c 2 * c 3 . 4. φ ≡ c 1 # c 2 : δ; k |= c 1 # c 2 means that c 1 ∈ δ(k) ∨ c 2 ∈ δ(k). Obviously, we have c 1 ∈ δ(k ) ∨ c 2 ∈ δ(k ), and hence δ; k |= c 1 # c 2 . 5. φ ≡ c 1 ≺ c 2 : δ; k |= c 1 ≺ c 2 implies that χ δ (c 1 , k) = χ δ (c 2 , k) ⇒ c 2 ∈ δ(k). It is obvious that χ δ (c 1 , k) = χ δ (c 2 , k) ⇐⇒ χ δ (c 1 , k ) = χ δ (c 2 , k ) If χ δ (c 1 , k) = χ δ (c 2 , k), there must be χ δ (c 1 , k) > χ δ (c 2 , k) because precedence implies causality
χ δ (c 1 , k ) > χ δ (c 2 , k ) by condition 2. Consequently, we have δ; k |= c 1 ≺ c 2 . If χ δ (c 1 , k) = χ δ (c 2 , k), then c 2 ∈ δ(k), which implies c 2 ∈ δ(k ) because δ(k) = δ(k ) by condition 1. Thus, δ; k |= c 1 ≺ c 2 6. φ ≡ c 1 c 2 $ d: δ; k |= c 1 c 2 $ d implies that χ(c 1 , k) = max(χ(c 2 , k) - d, 0). Because χ(c 2 , k) ≥ d, there is χ(c 1 , k) = χ(c 2 , k) -d. We have χ(c 1 , k) + n = χ(c 2 , k) + n -d for each n in N. Let n = χ(c 1 , k ) -χ(c 1 , k). Thus, χ(c 1 , k ) = χ(c 2 , k ) -d by condition 3. Because n ≥ 0, we have χ(c 2 , k ) -d ≥ 0. Thus, χ(c 1 , k ) = max(χ(c 2 , k ) -d, 0). Namely, δ; k |= c 1 c 2 $ d. c1 c1 c1 c2 c2 c2 1 2 3 4 5 6 1 2 3 4 5 6 1 2 3 4 5 6 Schedule (a) Schedule (b) Schedule (c)
Figure 4: Three schedules that satisfy the precedence constraint c1 ≺ c2.

7. φ ≡ c 1 c 2 : δ; k |= c 1 c 2 . Namely, χ(c 1 , k) ≥ χ(c 2 , k). Since χ(c 1 , k ) - χ(c 1 , k) ≥ χ(c 2 , k ) -χ(c 2 , k) then χ(c 1 , k) + (χ(c 1 , k ) -χ(c 1 , k)) ≥ χ(c 2 , k) + (χ(c 2 , k ) -χ(c 2 , k)), i.e., χ(c 1 , k ) ≥ χ(c 2 , k ). Thus, δ; k |= c 1 c 2 . 8. φ ≡ c 3 c 1 ∧ c 2 : δ; k |= c 3 c 1 ∧ c 2 means that χ(c 3 , k) = max(χ(c 1 , k), χ(c 2 , k)). Thus, we have χ(c 3 , k) + m = max(χ(c 1 , k) + m, χ(c 2 , k) + m) for each m in N. Let m = χ(c 1 , k ) -χ(c 1 , k). By condition 4, we have χ(c 3 , k ) = max(χ(c 1 , k ), χ(c 2 , k )), and hence δ; k |= c 3 c 1 ∧ c 2 . 9. φ ≡ c 3 c 1 ∨ c 2 : δ; k |= c 3 c 1 ∨ c 2 means that χ(c 3 , k) = min(χ(c 1 , k), χ(c 2 , k)). for each m in N. Let m = χ(c 1 , k ) -χ(c 1 , k). By condition 4, we have χ(c 3 , k ) = min(χ(c 1 , k ), χ(c 2 , k )), and hence δ; k |= c 3 c 1 ∨ c 2 .
10. φ ≡ c 1 c 2 ∝ p: the proof is straightforward by condition 5 and the definition of periodic filter.

The proof is done. We explain by an example that the conditions in Theorem 1 are less constraining than those defined in our previous work [START_REF] Zhang | An executable semantics of clock constraint specification language and its applications[END_REF]. Figure 4 shows three schedules for the precedence constraint c 1 ≺ c 2 . All three are periodic schedules according to Definition 5. For instance, we can find k = 1 and p = 2 for schedule (a), and k = 1 and p = 4 for schedule (b) such that k and p satisfy Definition 5. Schedule (a) and (b) also satisfy the condition in Theorem 1 with k = 1, k = 3 and k = 1, k = 5 respectively. It is also obvious that schedule (c) also satisfies Definition 5 with k = 1, p = 1 and the conditions in Theorem 1 with

k = 1, k = 2. By schedule (c), we have χ(c 1 , k ) -χ(c 1 , k) > χ(c 2 , k ) -χ(c 2 , k) with k = 1, k = 2.
Schedule (c) does not satisfy the conditions defined in the work [START_REF] Zhang | An executable semantics of clock constraint specification language and its applications[END_REF], where all the clocks are required to tick the same number of ticks from k to k . In that sense, the conditions in Theorem 1 are less constraining and provide an important relaxation to find practical solutions.

Corollary 1. Given a schedule δ : N + → 2 C , a set Φ of clock constraints, and two natural numbers k, k (k > k), δ |= k Φ ⇒ δ; k |= Φ if each constraint φ in Φ satisfies all the five conditions in Theorem 1.
Given an n-bounded schedule δ of a set Φ of clock constraints, if there exist two natural numbers k, k ≤ n, which satisfy the five conditions in Theorem 1, we can define a periodic schedule δ by extending δ such that δ satisfies Φ. Figure 5 shows the construction of δ based on δ. From k , the schedule δ repeats infinitely the steps from k to k -1. We next prove that δ |= Φ. By definition of δ , it is obvious that for all k ≤ k there is δ

δ (x) = δ(x) if x ≤ k δ(k + (x -k) mod (k -k)) if x > k 1 start 2 . . . k . . . k1 . . . k . . . x . . . n . . . k -k k1 = k + (x -k) mod (k -k) δ δ
; k |= Φ. For all k such that k > k , let k 1 = k + (k -k) mod (k -k). Obviously, k 1 < k , and hence δ ; k 1 |= Φ. By definition of δ , we have δ (k ) = δ(k 1 )
Because k and k satisfy the five conditions, so do k 1 and k . By Corollary 1, we have δ ; k |= Φ for all k in N + such that k > k . Thus, we have δ |= Φ.

Note that the five conditions in Theorem 1 are independent, which means that given a set Φ of ccsl constraints, if two clocks c 1 and c 2 are constrained by different stateful constraints the number of ticks from step k to k of clock c 1 is not necessarily the same as the one of clock c 2 . Namely, by the extended schedule δ , the clocks that are constrained by different stateful constraints in Φ can tick different times in a period. This makes a periodic schedule that is defined in the above-mentioned approach relatively general, compared with those schedules which force all the clocks to tick the same number of times in a period. However, if the stateful constraints delay, infimum and supremum where c 1 and c 2 are referenced are related to each other due to some other clocks, c 1 and c 2 must tick the same number of times in a period. This is straightforward to prove by Theorem 1.

We can also define infinite but non-periodic schedules with the proposed approach. Let us consider two disjoint ccsl constraints φ 1 and φ 2 such that clock(φ 1 ) ∩ clock(φ 2 ) = ∅, where clock : Φ → 2 C is a function that returns the set of all the clocks in a given constraint. We assume that φ 1 is a stateless constraint while φ 2 is a stateful one. Because φ 1 is stateless, we can find a non-periodic schedule for it and denote it by δ 1 . For the stateful constraint φ 2 , we assume there is a periodic schedule δ 2 found under the proposed sufficient condition. Let δ be a schedule such that for each i in

N + , δ(i) = δ 1 (i) ∪ δ 2 (i).
Then, δ must be a schedule of {φ 1 , φ 2 }. However, δ may not be periodic because δ 1 is non-periodic.

The proposed approach is also suitable to more general cases where there are n sets of ccsl constraints and each set is disjoint from others.

Theorem 2. Given n sets Φ 1 , . . . , Φ n of ccsl constraints on n sets C 1 , . . . , C n of clocks where C i ∩ C j = ∅ with 1 ≤ i < j ≤ n, let δ 1 , . . . , δ n be n schedules of Φ 1 , . . . , Φ n respectively and δ : N + → 2 C1∪...∪Cn be a schedule such that ∀i ∈ N + .δ(i) = j∈n δ j (i). Then, δ is a schedule of Φ 1 ∪ . . . ∪ Φ n .

We explain the basic idea of the proof of Theorem 2. Let φ be a constraint in some Φ i (1 ≤ i ≤ n). We prove δ |= φ by case analysis on the form of φ. As an example, we consider precedence and assume that φ = c 1 ≺ c 2 with clocks

c 1 and c 2 in C i . For each j in N + , χ δi (c 1 , j) = χ δi (c 2 , j) =⇒ c 2 ∈ δ i (j). By definition of δ, there is c 2 ∈ δ i (j) ⇐⇒ c 2 ∈ δ(j) and χ δ (c, j) = χ δi (c, j) for each c ∈ {c 1 , c 2 } and j ∈ N + . That is because c 1 , c 2 ∈ C k with k = 1, . . . , n and k = i. Thus, for each j in N + we have χ δ (c 1 , j) = χ δ (c 2 , j) =⇒ c 2 ∈ δ(j)
, and hence δ |= φ. Other cases can be proved likewise, and we omit the details in the paper.

By Theorem 2, we can divide a set Φ of constraints into several subsets such that the sets of clocks of these subsets of constraints are disjoint. Then, we search for a schedule for each subset of constraints with which we can define a schedule for Φ. 3.

C = i∈|C| C i ; 4. ∅ ∈ C.
Intuitively, C is a set of disjoint subsets of clocks, and clocks in each subset are connected. A special case is that C = {C} if all the clocks in C are connected. Given a set Φ of ccsl constraints on a set C of clocks, we assume that C = {C 1 , . . . , C n } with some n in N, and Φ i ⊆ Φ is the set of all the constraints in Φ which are defined on C i . If there exists a schedule δ i for each Φ i such that δ i |= Φ i , let δ be a schedule such that ∀j ∈ N + .δ(j) = i∈|C| δ i (j). By Theorem 2, δ |= Φ must hold.

Maude in a Nutshell

In this section, we introduce some background on Maude that is necessary to understand this paper. Maude is a rewriting-logic-based algebraic specification language and also an efficient rewrite engine [START_REF] Clavel | All about Maude[END_REF]. The underlying rewriting logic of Maude is a logic of concurrent change well suited to formalize states and concurrent computations. Maude has been widely used as a logical and semantic framework for the formalization and verification of computer systems and programming languages [START_REF] Meseguer | The rewriting logic semantics project: A progress report[END_REF][START_REF] Meseguer | The rewriting logic semantics project[END_REF][START_REF] Meseguer | Twenty years of rewriting logic[END_REF][START_REF] Csaba | Real-Time Maude and its applications[END_REF]. Maude specifications are executable, and various formal analysis methods are provided, such as simulation, reachability analysis by state-space exploration, and LTL model checking.

Formalization in Maude

A module is the unit of Maude programs. A module specifies a logical theory. In Maude there are two kinds of modules, functional modules and system modules. A functional module specifies a membership equational theory, and a system model specifies a rewrite theory. A membership equational theory is a pair of the form (Σ, E ∪A), whose underlying logic is called membership equational logic [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]. Σ is called a signature, specifying type structures as sorts and subsorts and function symbols; E is a collection of (possibly conditional) equations and memberships defined on Σ; and A is a collection of equational attributes such as associativity, commutativity and identity, declared for those operators in Σ. Equations are used to axiomatize the properties of the operators in Σ. Maude performs equational reduction with the equations E oriented from left to right modulo the axioms A.

A system module specifies a rewrite theory (Σ, E ∪ A, R), which consists of an underlying membership equational theory (Σ, E ∪ A) and a set R of rewrite rules, each of which has the form:

l : t -→ t if ( i p i = q i ) ∧ ( j u j := v j ) ∧ ( k w k : s k ) ∧ ( m t m -→ t m ),
where l is a label, and t, t are the terms that are constructed by the operators in Σ with some universally quantified variables. A rewrite rule may have conditions. There are four kinds of conditions which can be ordinary equations, matching equations, membership conditions, or rewrite conditions [START_REF] Clavel | All about Maude[END_REF]. Mathematically, a matching equation u j := v j is interpreted as an ordinary equation. Operationally, it is treated by matching the term e.g., u j on the left-hand side against the one e.g., v j on the right-hand side. A matching equation holds if and only if the matching succeeds. In u j there may be new variables, i.e., the variables that occur in u j but neither in t nor in any of the conditions before u j in the rewrite rule. After matching succeeds, these new variables are instantiated by the corresponding subterms in the canonical form of v j . We omit explanations of membership conditions and rewrite conditions because they are not used in our work. Interested readers can refer to the work [START_REF] Clavel | All about Maude[END_REF] for more details. Computationally, given a term t 0 which has a subterm t 0 that can be matched by t in the above rule with a substitution σ, t 0 can be rewritten into a new term with t 0 being replaced by the corresponding substitution instance of t , provided that the conditions of the rule hold in the context of the substitution.

When specifying a system in Maude as a rewrite theory, the underlying membership equational theory of the rewrite theory specifies the "static aspects" of the system, i.e., the algebraic structure of the set of system states, and the rules in R specify the "dynamic aspects" of the system, i.e., all the possible transitions that the system can perform. In Maude, a system state is represented as a Σ-term. Transitions among the states are formalized by rewrite rules.

We briefly summarize the syntax of Maude (see [START_REF] Clavel | All about Maude[END_REF] for more details). A functional module has the form of fmod ModName is Decs&Stmts endfm, where ModName is a user-defined name of the module and Mod &Stmts includes importations of other modules, declarations of sorts and subsort relations, declarations of operators, variables and equations. Sorts and subsort relations are declared by the keywords sorts and subsort, respectively. Operators are declared with the op keyword in the form: op f : s 1 . . . s n -> s, where s i (i = 1, . . . , n) and s are sorts. Maude allows for user-defined mixfix operators and uses underbars in operators to indicate each of the argument positions. An equation in Maude is declared in the form of eq t = t , where t and t are two terms of the same sort. An equation can be conditional, which is declared by the keyword ceq and ended with the keyword if, followed by a conjunction of conditions. A rewrite rule in Maude is declared in the form of rl [label]: t => t . A conditional rewrite rule is declared by the keywords crl and if with a conjunction of rewrite conditions.

Formal analysis in Maude

Maude specifications are executable under certain conditions. Maude provides multiple formal analysis methods, including simulation, reachability analysis, and LTL model checking to formally analyze systems.

Simulation is achieved using Maude's rewrite command (abbreviated rew), which repeatedly applies the rewrite rules to transform a given term step by step. The transformation process simulates one behavior of the specified system. There may be some rules that can be applied an infinite number of times. In such cases, an upper bound to the rewrite steps is needed to force Maude to stop.

Maude provides the search command to explore the reachable state space of specified systems. The syntax of search command follows the general scheme:

search [n,m] in ModName : t 1 =>* t 2 such that condition .
where n, m are optional arguments providing a bound on the number of expected solutions and the maximum depth of the search; t 1 is the starting term; t 2 is a pattern which is essentially a term that contains some variables and has the same sort as t 1 ; and condition represents an optional condition which has the same form as the one of conditions in conditional rules. A term t is a solution if t matches against t 2 with a match satisfying the optional condition and there exists a rewriting sequence from t 1 to t. The arrow =>* is used to restrict the length of rewriting steps to none, one or more steps. If the arrow =>! is used instead of =>*, then a solution must be a term that cannot be further rewritten.

X, c1 ≺ c2 F -→ X , c1 ≺ c2 X(c1) = X(c2) =⇒ c2 ∈ F [Precedence] X, c1 c2 F -→ X , c1 c2 X(c1) = X(c2) [Causality-I] X, c1 ⊆ c2 F -→ X , c1 ⊆ c2 [Subclock] X, c1 # c2 F -→ X , c1 # c2 [Exclusion] X, c1 c2 + c3 F -→ X , c1 c2 + c3 [Union] X, c1 c2 × c3 F -→ X , c1 c2 × c3 [Intersection] X, c1 c2 ∧ c3 F -→ X , c1 c2 ∧ c3 [Infimum-I] X(c2) > X(c3) X, c1 c2 ∧ c3 F -→ X , c1 c2 ∧ c3 X(c2) < X(c3) [Infimum-II] X, c1 c2 ∧ c3 F -→ X , c1 c2 ∧ c3 X(c2) = X(c3) [Infimum-III] X, c1 c2 ∨ c3 F -→ X , c1 c2 ∨ c3 [Supremum-I] X(c2) < X(c3) X, c1 c2 ∨ c3 F -→ X , c1 c2 ∨ c3 X(c2) > X(c3) [Supremum-II] X, c1 c2 ∨ c3 F -→ X , c1 c2 ∨ c3 X(c2) = X(c3) [Supremum-III] X, c1 c2 $ d F -→ X , c1 c2 $ d [Delay-I] X(c2) ≥ d X, c1 c2 $ d F -→ X , c1 c2 $ d X(c2) < d [Delay-II] X, c1 c2 ∝ p F -→ X , c1 c2 ∝ p [Periodicity-I] ∃m ∈ N + .X(c2) = p × m -1 X, c1 c2 ∝ p F -→ X , c1 c2 ∝ p [Periodicity-II] ∃m ∈ N + .X(c2) = p × m -1 c1 ∈ F ∨ c2 ∈ F c1 ∈ F ∨ c2 ∈ F ∨ c3 ∈ F c2 ∈ F ∨ {c1, c2} ⊆ F c1 ∈ F ∨ c2 ∈ F c1 ∈ F ∨ {c2, c3} ⊆ F c1 ∈ F ⇐⇒ c2 ∈ F c1 ∈ F ⇐⇒ c3 ∈ F c1 ∈ F ⇐⇒ c2 ∈ F c1 ∈ F ⇐⇒ c2 ∈ F ∧ c3 ∈ F c1 ∈ F ⇐⇒ c2 ∈ F ∨ c3 ∈ F c1 ∈ F ⇐⇒ c2 ∈ F c1 ∈ F c1 ∈ F c1 ∈ F ⇐⇒ c2 ∈ F c1 ∈ F ⇐⇒ c3 ∈ F X, c1 c2 F -→ X , c1 c2 X(c1) > X(c2) [Causality-II]
Maude has an efficient LTL model checker, supporting model checking of the properties expressed in linear temporal logic. Given a Maude specification of a system and a set of atomic propositions defined on system states, the Maude LTL model checker is invoked by the built-in function modelCheck, which takes two arguments, an initial state and an LTL formula, and returns true if no counterexample is found, and otherwise a counterexample as a witness to the violation. An LTL formula is built out of atomic propositions that need to be predefined and logical and temporal operators in LTL. A condition of doing LTL model checking in Maude is that the set of states that are reachable from the given initial state is finite.

Operational Semantics of CCSL and its formalization in Maude 4.1 Operational semantics of CCSL

We define a clock system, denoted by X, Φ , consisting of a configuration X and a set Φ of ccsl constraints. Let C Φ be the set of all the clocks in Φ. A configuration X : C Φ → N is a function and for each c in C Φ , X(c) denotes the current number of ticks of clock c. Let F be a non-empty subset of C Φ . If the ticking of every clock in F satisfies all the clock constraints in Φ, there is a transition from X, Φ to X , Φ with respect to F , denoted by X, Φ F -→ X , Φ , where:

∀c ∈ C Φ .X (c) = X(c) + 1 if c ∈ F X(c) if otherwise. ( 1
)
Figure 6 shows the operational semantics of the 10 types of clock constraints in ccsl. Above a line is the condition of the transition under the line. We take the operational semantics of precedence for example. The rule labeled Precedence says that there is a transition from X, c 1 ≺ c 2 to X , c 1 ≺ c 2 with respect to F if the condition X(c 1 ) = X(c 2 ) =⇒ c 1 ∈ F holds. The condition clearly corresponds to the definition of precedence in Figure 1. For the definition of infimum, three cases are considered based on the relation between X(c 2 ) and X(c 3 ). For instance, when X(c 2 ) > X(c 3 ) holds, c 1 is in F if and only if c 2 is in F , as formalized by the rule labeled by Infimum-I. Otherwise, c 1 c 2 ∧ c 3 is violated in the new configuration X . Two other cases are formalized by Infimum-II and Infimum-III, respectively. The operational semantics of other constraints are defined likewise.

Formalization of a clock system

The formalization of a clock system X, Φ consists of formalizations of X and Φ. ccsl constraints can be naturally formalized in Maude. We use quoted identifiers to represent clocks in ccsl, e.g., 'c represents a clock c. We declare a sort Clock whose elements are essentially the quoted identifiers that are represented by the sort Qid in Maude. In the following Maude module CONSTRAINTS two sorts Constraint and Constraints are declared to represent ccsl constraints and sets of constraints, respectively. The constant empty denotes an empty set of constraints, and the infix operator __ denotes the union of two sets of constraints. The operators declared from Line 6 to 15 are used to represent the ten ccsl constraints correspondingly. To formalize a configuration X in a clock system, we think of a logical clock in a configuration as a triple (c, , n), consisting of the clock identifier c, a list of records with each value being tick or idle (abbreviated by t or i respectively), which represents that the clock ticks or not at the step where the value is located in the list, and a natural number n that denotes the numbers of ticks in . 1 We call it a clock triple. Initially, is an empty list, and n is 0. In the following module CONFIGURATION, sort ConfElt is declared to represent clock triples. The infix operator [_,_,_] is used to construct a clock triple with a clock, a list of records and a natural number as its arguments. Clock and TickList are the sorts to represent clocks and lists of ticks. Each list consists of a finite number of t and i, which are constants to represent tick and idle respectively. Given a clock system, we use a collection of clock triples to represent a configuration of the clocks in the system, and declare a sort named Conf to represent the configurations. Each state of a clock system for a set of ccsl constraints consists of a set of clocks, a set of ccsl constraints on the clocks and a configuration of all the clocks. Besides the three information, we introduce a natural number to each state to represent the elapsed time (the number of elapsed steps) of the system. Such information is not used for specifying the operational semantics of ccsl, but for the purpose of verification by fixing a bound for searching and state exploration. We declare a sort CCSLState and an operator <_;_;_;_> as shown below to formalize states of clock systems.

1 fmod CONFIGURATION is

Formalization of the operational semantics of CCSL

The operational semantics of CCSL constraints can be naturally formalized using Maude rewrite rules. The main rule is defined as follows:

1 ---The transition rule that formalizes the operational semantics of CCSL 2 crl < (F , F ') ; PHI ; X ; K > = > < (F , F ') ; PHI ; update (X , F ) ; K + 1 > 3 if F =/= empty /\ satisfy (F , X , PHI ) .

In the above rule, F, F' are variables of sort ClockSet; and PHI, X, and K are variables of sorts Constraints, Conf, and Nat, respectively. X and F correspond to X and F in Figure 6. Given a set C of clocks, F can be instantiated by any subset C of C by matching (F, F') to C with the variable F' of sort ClockSet being instantiated by C -C . As mentioned in Section 4, F must be a non-empty set and satisfy corresponding conditions for ccsl constraints so that the clocks in F can tick in the current configuration X. The first conjunct in the condition part of the above rule says that F is not empty, and the second one means that F satisfies the constraints PHI in the configuration X. The definition of the function satisfy is explained later. If the two conditions hold, we obtain a new configuration by updating configuration X with the set F of clocks according to Equation 1, as represented by update(X,F).

To formalize the satisfiability of a bounded schedule with respect to a set Φ of ccsl constraints, we declare in Maude a predicate satisfy which takes three arguments: a set F of clocks, a configuration X, and a ccsl constraint φ. The predicate returns true if C satisfies Φ with respect to X, and otherwise false. We consider each possible constraint form in Φ when defining satisfy. As examples, we list below four equations that are defined in Maude to specify the satisfiability of a set F (represented by F) of clocks with precedence, delay, infimum and periodicity with respect to X, respectively:

1 ---Declaration of predicate satisfy :

2 op satisfy : ClockSet Conf Constraint -> Bool . 3 ---Precedence 4 eq satisfy (F , ([ C1 , TL1 , N1 ] , [ C2 , TL2 , N2 ] , X ) , C1 < C2 ) = 5 if N1 == N2 then not ( C2 in F ) else true fi . 6 ---Delay 7 eq satisfy (F , ([ C2 , TL2 , N2 ] , X ) , C1 != C2 $ N ) = 8 if N2 >= N then ( C1 in F ) == ( C2 in F ) else not ( C1 in F ) fi .
We first consider the Maude definition of precedence for example. The second argument of satisfy at Line 4 represents an arbitrary configuration X, where there must be at least two clock triples of C1 and C2 whose lists of ticks are TL1 and TL2 respectively. The variables N1 and N2 of sort Nat in the triples represent the numbers of ticks in TL1 and TL2. The right-hand side term of the equation represents the condition of the rule defined for precedence in Figure 6. Because the correspondence between the condition and their definitions in the equation is clear, we omit detailed explanations in the paper. The second equation is defined to formalize the two cases (Delay-I and Delay-II in Figure 6) of the operational semantics of delay.

Likewise, we consider the Maude definitions of infimum and periodicity. The equations defined for them are as follows:

1 ---Infimum 2 eq satisfy (F , ([ C1 , TL1 , N1 ] ,[ C2 , TL2 , N2 ] ,[ C3 , TL3 , N3 ] , X ) , C1 != C2 /\ C3 ) = 3 ( if N2 > N3 then ( C1 in F ) == ( C2 in F ) else 4 ( if N2 < N3 then ( C1 in F ) == ( C3 in F ) else 5 ( C1 in F ) == ( C2 F or C3 in F ) 6 fi ) 7 fi ) . 8 ---Periodicity 9 eq satisfy (F , ([ C1 , TL1 , N1 ] , [ C2 , TL2 , N2 ] , X ) , C1 != C2 P ) = 10 if ( N2 + 1) rem P == 0 then ( C1 in F == C2 in F ) else not ( C1 in F ) fi .

Formal Analysis on CCSL in Maude

Given a set of ccsl constraints, several properties need to be checked or verified, e.g., is there a schedule that satisfies all the constraints? (are the constraints consistent?); if so, pick one specific schedule according to an external criteria (avoid deadlocks, reduce memory usage, force a fast pace). In this section, we show four applications that directly derive from our encoding of the operational semantics of ccsl in Maude.

Bounded scheduling

Given a bound n and a set of clock constraints Φ, we can use Maude's search command to search for all the n-bounded schedules that satisfy Φ. If Maude cannot find at least one of such schedules, it means that there does not exist such an n-bounded schedule, and further we can conclude that there does not exist a schedule that satisfies Φ, i.e., Φ is not valid. For instance,

{c 1 ≺ c 2 , c 2 ≺ c 1 } is invalid.
We show an example of finding bounded schedules for a given set of clock constraints using Maude's search command.

Example 1. Find bounded schedules that satisfy the set of constraints

Φ 1 = {c 1 ≺ c 2 , c 3 c 1 $ 1, c 2 ≺ c 3 }.
In Maude, we use 'c1 < 'c2, 'c3 != 'c2 $ 1 and 'c2 < 'c3 to represent the three constraints, respectively. First, we use Maude's search command to find schedules with maximal search depth 30. The actual command and the result returned by Maude are as follows: In the above search command, we only provide the maximum depth of the search and do not specify the number of expected solutions. It means that Maude will return all the solutions it finds within the depth 30. The starting term represents the initial configuration where the list of each clock is nil, and the step is 0. The pattern represents an arbitrary configuration where the step is 30, which means a configuration after 30 steps of evolution. The collection of the tick lists of all the clocks in the configuration can be interpreted as a schedule of bound 30.

1 search [ ,30] < ( ' c1 , 'c2 , ' c3 ) ; ( ' c1 < ' c2 ) ( ' c2 < ' c3 ) ' c3 != ' c1 $ 1 ; 2 [ ' c1 , nil ,0] ,[ ' c2 , nil ,0] ,[ ' c3 ,
The search command returns only one solution, which means that there exists only one schedule whose bound is 30 within the search depth 30. The bounded schedule satisfies the three constraints in Φ 1 . From the list of ticks of the three clocks, one can see that c 1 and c 3 only tick at all odd steps except that c 3 does not tick at the first step because of the constraint c 3 c 1 $ 1, and c 2 only ticks at all even steps. Namely, c 1 and c 2 tick alternatively by the returned bounded schedule. The result coincides with the definition of alternation constraint between clocks in an earlier work of the third author [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF].

Periodic scheduling

We can also find periodic schedules in Maude using the operational semantics of ccsl. The basic idea is to formalize the sufficient conditions in Theorem 1 and at each step k we check if all these conditions are satisfied by a k -bounded schedule, that is, if there exists a step k such that 1 ≤ k < k and the k -bounded schedule satisfies the five conditions with k and k. If that is the case, a periodic schedule is found, whose period is kk.

We declare a function getPeriod, which returns the period for a given configuration X if the underlying bounded schedule in X satisfies the sufficient conditions, and 0, otherwise. As shown below, getPeriod takes four arguments, a configuration, a set of constraints, and two natural numbers corresponding to k and k , respectively. It checks each step from k to 0 in a backward manner until it finds one satisfying the sufficient conditions. Once (and if) such a step is found, the corresponding period is returned. In the equation, term sd(K',K) represents the value of subtracting K from K', with K' greater than K. isPeriodic is an auxiliary function, which returns true when a bounded schedule satisfies the sufficient conditions with respect to a set of constraints and two given steps. It is defined inductively with respect to each kind of constraint. The second equation defined below considers the case of precedence. The conjuncts at Line 9 represent Condition 1 and the first conjunct at Line 10 represents Condition 2 in Theorem 1. Other conditions are formalized likewise, and we omit the details in the paper. Let us consider finding periodic schedules of the precedence constraint c 1 ≺ c 2 as an example. We set the number of expected periodic schedules to search to be 4. The command used for the search is as follows:

Table 1 shows four periodic schedules found by Maude for c 1 ≺ c 2 when the bound is set to 4. The red steps in each schedule in the table are the starting steps of the first and second iterations of the period. We can also provide a concrete period and use Maude to search if there exist such periodic schedules with the given specific period. However, due to the infinite number of steps, and like when searching bounded schedules, it cannot be guaranteed that there do not exist such periodic schedules even if Maude returns no result.

Formal verification by (bounded) model checking

Beside checking the existence of expected schedules, one may also want to explore the properties of the schedules that satisfy a set of constraints. For instance, one would expect that all the clocks must tick infinitely often, or a clock must tick some steps later after some other clock ticks. Another important application of the executable semantics of ccsl is to verify such properties by bounded model checking using the search command or Maude's LTL model checker.

Detection of deadlock schedules by bounded model checking

Finding deadlocks, or rather finding schedules without deadlocks, is one very important feature for a ccsl specification. The word deadlock usually means that after some steps, the system cannot evolve at all, i.e., no clock can tick. Due to the polychronous nature of ccsl, some parts of the system may be highly independent from other parts (see Definition 6 about connected clocks). Consequently, we use a stronger condition for deadlocks. Indeed, in ccsl, we expect all the clocks to tick infinitely often, so deadlock means that after some steps there is at least one clock that will never be allowed to tick.

Besides, since a ccsl specification may have conflicts, some schedules may end up in deadlocks while others may not. On this matter, we use the same definition as in [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF]. We rely on our encoding in Maude to select those schedules that do not have deadlocks. Example 2. The example is from a previous work [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF]. It was previously used to perform flow latency analysis with the Architecture Analysis & Design Language (AADL) [START_REF] Feiler | Flow latency analysis with the architecture analysis and design language (AADL)[END_REF]. As shown in Figure 7, the component takes two inputs in 1 and in 2 , performs computations on the two inputs concurrently in step 1 and step 2 , then combines the results to produce a final value in step 3 based on data produced at step 1 and step 2 , and then outputs this final result through out.

The application continuously captures new inputs and produces one output for each pair of inputs in a streaming fashion.

Each processing unit is controlled by a clock, and a set Φ 2 of clock constraints specify the intentional semantics of the AADL specification (see Figure 8). Let us note that tmp 1 and tmp 2 are two intermediate clocks required to specify constraints between in 1 , in 2 and out.

Using the approach introduced in Section 5.2, we can find multiple periodic schedules in which each clock can tick infinitely often. A common feature of these periodic schedules is that in 1 must always tick simultaneously with in 2 . If we break this pattern (not explicitly specified), the application may go into In Maude, one can find such a deadlock by searching for a target state which cannot be further rewritten by any rewrite rules. For the above example, we search for the deadlock schedules within 3 steps in Maude with the following command:

1 search [ ,3] < 'in1 , 'in2 , 'out , ' step1 , ' step2 , ' step3 , ' tmp , ' tmp2 ; The search command finds six deadlock schedules, as shown in Table 2. A common feature of these deadlock schedules is that at some step in 1 and in 2 do not tick simultaneously, which finally results in a state where no clock can tick anymore.

One solution to the deadlock is to force in 1 and in 2 to tick simultaneously, which can be achieved by introducing two new constraints, i.e. in 1 ⊆ in 2 and in 2 ⊆ in 1 . Maude returns no solution, which means that no deadlock schedule is found 2 . However, forcing in 1 and in 2 to tick simultaneously may be too restrictive from a pragmatic point of view since it may be difficult to synchronize two independent events. It suffices to enforce the slowest clock between in 1 and in 2 to tick before out. Thus, we replace in 1 + in 2 by in 1 ∧ in 2 in Figure 8. We denote the new set after replacing the constraint by Φ 2 . Maude also returns no solution with a given maximum depth of the search for Φ 2 .

LTL Model checking of periodic schedules

In this section, we explore the solutions that do not require to rely on bounded model-checking only. This is the reason that motivated the definition of periodic schedules since it allows a finite abstraction of the infinite state space.

By definition, in periodic schedules all clocks tick periodically. For properties where the exact number of ticks is not relevant (most often, only the difference between the number of ticks of two clocks is important), we can force each periodic schedule to go from step k back to step k, where k and k are the beginning and ending steps of the first period of the schedule (k < k ). An extra condition is added to check if a successor configuration X' has an underlying periodic schedule. If not, configuration X is changed into a new one, i.e. X'. Otherwise, it is changed into an old one by rolling back P steps, where P is the period of the searched periodic schedule. By excluding non-periodic schedules, we obtain a finite state space only from the searched periodic schedules, as depicted in Figure 9. Figure 9 (left) shows an example of a state space that contains both periodic and non-periodic schedules up to a bound, e.g. 3. The path with a loop represents a periodic schedule. In the figure there are three periodic schedules, which constitute a finite state space, as shown in Figure 9 (right). The finite state space can then be model checked. It is worth mentioning that we still need to set a bound in order to search for periodic schedules. In that sense, model checking of periodic schedules is still not complete because it is possible that some periodic schedules are not found within a given search bound and hence cannot be model checked.

Next, we show some basic properties that clock constraints are expected to satisfy and their representations as LTL formulae. Let tick be a parameterized predicate on states, which takes a clock c as argument and returns true if c ticks in a state. The definition of tick in Maude is as follows: Repeated ticking: all clocks must tick infinitely often, which can be formalized as: c∈C tick(c).

1 subsort CCSLState < State .
Simultaneous ticking: two clocks c 1 and c 2 must always tick simultaneously, which can be formalized as: (tick(c 1 ) ⇐⇒ tick(c 2 )).

Leading-to ticking: if a clock c 1 ticks, it must cause another clock c 2 to tick eventually, which can be formalized as: (tick(c 1 ) → tick(c 2 )).

Alternative ticking: two clocks c 1 and c 2 must always tick in alternation, which can be formalized as:

(tick(c 1 ) → (¬tick(c 1 ) U tick(c 2 )) ∧ tick(c 2 ) → (¬tick(c 2 ) U tick(c 1 )).
We take the model checking of some LTL properties of the constraints in Φ 1 as an example. The intention of composing the three constraints in Φ 1 is to force clocks c 1 and c 2 to tick alternatively. By bounded scheduling and periodic scheduling analyses, we have indeed found a schedule that seemingly satisfies this property. By model checking, we can formally verify it. The command used for model checking the property is as follows:

1 red modelCheck ( <( ' c1 , ' c2 , ' c3 ) ; ( ' c1 < ' c2 ) ( ' c2 < ' c3 ) ( ' c3 != ' c1 $ 1) ; 2 [ ' c1 , nil ,0] , [ ' c2 , nil ,0] , [ ' c3 , nil ,0]; 0 >, 3 [](( tick ( ' c1 ) -> O (~tick ( ' c1 ) U tick ( ' c2 ) ) ) /\ 4 ( tick ( ' c2 ) -> O (~tick ( ' c2 ) U tick ( ' c1 ) ) ) )
) . 5 result Bool : true Maude returns true, meaning that Φ satisfies the alternative ticking property.

Simulation with customized arbitration policies

Given a set Φ of clock constraints, there may be more than one schedule. In such cases, we can find an external criteria to pick one that has a given property. In a previous work [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF], this was called an arbitration/simulation policy. One of the side effects of our work is that we can now formalize these arbitration policies and ask Maude to apply them for us. a clock must not tick if it does not have to tick. Such policies are usually user-definable. Another application of the executable operational semantics of ccsl is to simulate the behaviors of clocks under given constraints along with some arbitration policies. We consider five basic arbitration policies, which we call randomness, maximum minimum, laziness, activeness and mixity, respectively.

Randomness: to specify that at each step a successor is randomly chosen among all possible successors. Maximum: to specify that at each step the number of clocks that tick is maximal among all possible successors. Such a solution is not necessarily unique. This is useful to force the pace and execute as much as possible.

Minimum: to specify that at each step the number of clocks that tick is minimal among all possible successors. Such a solution is not necessarily unique.

Laziness: to specify a set of lazy clocks that only tick if they have to tick at each step.

Activeness: to specify a set of active clocks that tick as soon as they can at each step. When all the clocks are active ones, the policy is equivalent to maximum.

Mixity: to specify a set of lazy clocks and a set of active clocks. When all the clocks are lazy ones, the policy is equivalent to minimum. Each of the above arbitration policies except randomness determines a unique successive behavior of each clock. By simulating the behaviors of clocks from initial state with an arbitration policy, it produces a trace which is essentially a schedule characterized by the policy. represent sets of configurations. In the definition of getAllSuccessors from Line 10 to 14, metaSearch is a built-in meta-level function corresponding to the search command. We omit detailed explanations about this function because it is out of the scope of this paper. Interested readers are referred to the work [START_REF] Clavel | All about Maude[END_REF] for details. As an example, we give the definition of getConfbyPol with laziness policy, i.e., the equation at Line 16. CF is a variable of ConfSet, representing a set of configurations. The function getNonTickConf returns the sets of configurations in CF where clock C does not tick at the last step. If there is no such a configuration, CF is returned. We omit the definition of getNonTickConf because it is straightforward.

With the rule defined above, we can use Maude's rew command to simulate the behavior of a clock system with respect to a set of ccsl constraints and an arbitration policy. As an example, we simulate a clock system with respect to the constraints in Φ 2 with different arbitration policies. Because simulation will not terminate unless the schedule being simulated is a deadlock one. We set a bound 50 to the maximal depth of simulation. The commands used for the simulations are of the following form: We replace P in the above command with max, min, lazy('step1,'step2), active('step1,'step2) and mix('step1,'step2) to simulate with the five arbitration policies, respectively. Maude returns different schedules. To make simulation results easier to read, we developed a prototype tool on the top of Eclipse using Maude as the underlying simulation engine. Figure 10 shows the graphical representation of the five simulation results generated by the tool. All the five schedules satisfy the sufficient conditions of periodicity, and hence are periodic. There two main reasons for the periodicity of these schedules. One reason is the alternation constraint between the clocks out and tmp 1 . However, only by alternation a schedule may not be periodic because there is no constraint on the interval between two alternative ticks. When an arbitration policy is provided, the clocks that should tick in next step may be deterministic. The schedule becomes periodic when all the intervals between alternative ticks are the same. However, the periods of schedules may be different under different policies. For instance, the periods under maximum and activeness with step 1 and step 2 are 1, while the periods under the other three policies are 5 (under minimum), 3 (under laziness) and 2 (under mixity), respectively. 6 Related Work and Discussion ccsl mainly deals with logical clocks, i.e., unbounded increasing sequences (streams) of integers. The semantics of clock constraints may depend on Boolean parameters, in which case, we remain in a finite world and can rely on traditional verification and analysis results and tools. The constraints may also depend on unbounded natural numbers, for instance, the number of times a given clock has ticked. In this latter case, the constraint is called unsafe [START_REF] Mallet | Safe CCSL specifications and marked graphs[END_REF]. A specification is safe if it does not use any unsafe constraint. The satisfiability of ccsl specifications has already been studied. Most of the time, decidability is achieved by reducing to a safe subset of ccsl constraints. The reference semantics of ccsl was given in a research report [START_REF] André | Syntax and semantics of the Clock Constraint Specification Language (CCSL)[END_REF] mainly to be able to define a simulation tool called TimeSquare [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF]. TimeSquare encodes the operational semantics of ccsl in Java and captures Boolean constraints symbolically using Binary Decision Diagrams (BDD). TimeSquare works step by step and at each step, finding a solution reduces to a satisfiability problem. After deciding if and how many valid solutions can be found at a step, the TimeSquare clock engine picks one solution according to its simulation policy, updates the state space and moves forward. TimeSquare does not consider the unbounded specification as a whole and only produces one finite possible trace that satisfies all the constraints up to a given number of steps. In this work, we use bounded model-checking, and we can then explore all the solutions reached in a given number of steps, instead of only one.

1 rew [50] [ < 'in1 , 'in2 , 'out , ' step1 , ' step2 , ' step3 , 'tmp , ' tmp2 ; 2 ( ' out < ' tmp2 ) ( ' step1 < ' step3 ) ( ' step2 < ' step3 ) ( ' tmp < ' out ) ( ' in1 <= ' step1 ) 3 ( ' in2 <= ' step2 ) ( ' step3 <= ' out ) ( ' tmp2 != ' tmp $ 1) ( ' tmp1 != ' in1 /\ ' in2 ) ;
Several solutions have been proposed to make an exhaustive exploration of the entire state space (not up to a pre-defined number of steps). A comprehensive list of references has been summarized in a recent survey [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF]. However, one aspect is to be able to decide whether the state space can be represented with a finite abstraction even though the specification is unsafe [START_REF] Mallet | Safe CCSL specifications and marked graphs[END_REF]. Another way is to force a finite space by restricting to subsets of safe constraints [START_REF] Yu | Polychronous controller synthesis from MARTE/CCSL timing specifications[END_REF][START_REF] Gascon | Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL[END_REF][START_REF] Yin | Verification of MARTE/CCSL time requirements in Promela/SPIN[END_REF]. In the work [START_REF] Suryadevara | Verifying MARTE/CCSL mode behaviors using UP-PAAL[END_REF], a subset of CCSL constraints are transformed into timed automata to model check both logical and chronometric properties of CCSL constraints using the UPPAAL tool. In this work, we do not make any assumptions on whether the specification is safe or not by considering only periodic scheduling of ccsl from both theoretical and practical perspectives.

Like other existing approaches proposed for the formal analysis of ccsl, the formal analysis approach to periodic scheduling of ccsl is also based on its formal semantics. However, the main difference is that, thanks to the Maude environment, all the analyses performed result directly from the operational semantics without intermediate transformations, so without the need to prove that the semantics is preserved. Yu et al. [START_REF] Yu | Polychronous controller synthesis from MARTE/CCSL timing specifications[END_REF] proposed to encode ccsl in Signal before transforming it to the internal format of Sigali. We hope that the encoding in Maude will allow to conduct automated verification for all the transformational approaches that use ccsl as a step. Maude also gives a framework to define the arbitration policies formally for the purpose of simulation. Some undocumented simulation policies are available in TimeSquare [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF]. In Section 4, we give a simple formal interpretation for three of these simulation policies. We also propose three more and show how they can be implemented using Maude metasearch function.

Finally, abstract interpretation [START_REF] Cousot | Abstract interpretation[END_REF] or infinite model-checking [START_REF] Leroux | Flat counter automata almost everywhere! In 3rd International Symposium on Automated Technology for Verification and Analysis[END_REF] would allow reasoning on the global ccsl specification without restrictions. However, the encoding is likely to introduce semantic variations and we do not know at the moment how to encode ccsl constraints in a compositional way.

Conclusion and Future Work

We have proposed a new notion of bounded and periodic schedules to satisfy a ccsl specification. The satisfiability problem for ccsl specifications, which is still an open problem in the general case, is proved to be decidable with regards to bounded and periodic schedules even when using unsafe constraints. This is the first main result from a theoretical perspective. From a practical point of view, the second result of this paper is to present a Maude encoding of the formal semantics of an extended subset of ccsl to compute bounded and periodic schedules. We also describe how to implement customized arbitration policies within both simulation and bounded model-checking context.

Compared with our earlier work [START_REF] Zhang | An executable semantics of clock constraint specification language and its applications[END_REF], we proposed in this paper less constraining conditions for being able to build more periodic schedules automatically with the tool. We have also improved our work by considering an extended subset of the language to support the notion of logical periodicity between logical clocks. We then had to define a new semantic model for considering this extension.

ccsl is still an emerging formal specification language which is under further study. We are considering introducing new types of constraints such as alternative operators. Maude, as a formal meta-tool, provides a formal environment to study the language itself by quickly developing formal analysis toolkit for ccsl in terms of the executable semantics of ccsl constraints. For its executability of the mathematical semantics, Maude can be used as a precise interpreter and state explorer for the formal analysis of ccsl constraints.

Figure 2 :

 2 Figure 2: State-based representation of the schedules satisfying c 1 ≺ c 2 .

Figure 5 :

 5 Figure 5: Construction of periodic schedule δ from an n-bounded schedule δ.

Definition 6 (

 6 Connected clocks). Given a set C of clocks and a set Φ of clock constraints, two clocks c and c in C are connected, denoted by c c , if and only if one of the following two conditions is satisfied: 1. There exists a constraint φ in Φ such that c ∈ clock(φ) and c ∈ clock(φ), or 2. There exist n clocks (n > 0), i.e., c 1 , . . . , c n in C, such that c c 1 , c 1 c 2 , . . ., c n c . Let C be a partition of C, i.e., C ⊆ 2 C is a set of subsets of clocks in C such that: 1. For each C in C and two arbitrary clocks c, c in C , c c ; 2. For two arbitrary subsets C 1 , C 2 in C, C 1 ∩ C 2 = ∅, and for each c 1 in C 1 and c 2 in C 2 there is c 1 c 2 ;

Figure 6 :

 6 Figure 6: Operational semantics of ccsl.

2 includingmodules 3 sort ConfElt Conf . 4 subsort

 234 NAT + CLOCK + TICK -LIST . ---+ is a union operator on ConfElt < Conf .5 op [_ ,_ , _ ] : Clock TickList Nat -> ConfElt [ ctor ] . 6 op empty : -> Conf [ ctor ] . 7 op _ , _ : Conf Conf -> Conf [ ctor assoc comm id : empty ] 8 endfm

Figure 7 :

 7 Figure 7: A component in a practical application.

1 ≺Figure 8 :

 18 Figure 8: An abstraction as a clock constraint specification.

2 ( 3 ( 4 [ 5 [

 2345 ' out < ' tmp2 ) ( ' step1 < ' step3 ) ( ' step2 < ' step3 ) ( ' tmp < ' out ) ( ' in1 <= ' step1 ) ' in2 <= ' step2 ) ( ' step3 <= ' out ) ( ' tmp2 != ' tmp $ 1) ( ' tmp != ' in1 + ' in2 ) ; ' in1 , nil ,0] , [ ' in2 , nil ,0] , [ ' out , nil ,0] ,[ ' step1 , nil ,0] , [ ' step2 , nil ,0] , ' step3 , nil ,0] , [ ' tmp , nil ,0] , [ ' tmp2 , nil ,0] ; 0 > = >! S : CCSLState .

1 4 X 7 < 11 P

 4711 crl [ next ] : < (F , F ') ; PHI ; X ; K ' > = > < (F , F ') ; PHI ; X ' ; K ' + 1 >2 if F =/= empty /\ 3 satisfy (F ,X , PHI ) /\ ' := update (X , F ) /\ 5 getPeriod (X ' ,K ' + 1 , PHI ) == 0 .6 crl [ periodic ] : < (F , F ') ; PHI ; X ; K ' > = > (F , F ') ; PHI ; rollback (X ' , P ) ; sd (:= getPeriod (X ' ,K ' + 1 , PHI ) .

2

 2 op tick : Clock -> Prop . 3 eq < F ; PHI ; [ C , ( TL t ) ,N ] X ; K > |= tick ( C ) = true . 4 eq S : CCSLState |= P : Prop = false [ owise ] . The operator tick defines a proposition tick(c) for each clock c. The first equation defines that tick(c) is true in a given state where clock c ticks. The second equation (line 4) means that tick(c) is false in other cases. Below we list four common properties of ccsl constraints and their corresponding LTL formulas.

3 =⇒Figure 9 :

 39 Figure 9: Bounded state space of periodic schedulers.

4 [ 5 [

 45 ' in1 , nil ,0] , [ ' in2 , nil ,0] , [ ' out , nil ,0] , [ ' step1 , nil ,0] , [ ' step2 , nil ,0] , ' step3 , nil ,0] , [ ' tmp , nil ,0] , [ ' tmp2 , nil ,0] ; 0 >, P ] .

Figure 10 :

 10 Figure 10: The simulation results with the five arbitration policies.

  We use the wording clock or logical clock indistinctly in the following. While traditional synchronous languages give a syntax to combine signals, infinite sequences of values, and use clocks to express when the signals are present (have a value), ccsl discards the values on purpose to focus on relationships among clocks.

	2 The Clock Constraint Specification Language
	with Periodic Filter
	2.1 Syntax and semantics of CCSL
	ccsl relies on the notion of logical clocks, which are commonly used to express
	partial orders in distributed systems [1] or synchronization conditions in syn-
	chronous languages [3].

Definition 1 (Logical clock).

A logical clock c is an infinite sequence (a stream) of ticks, (c n ) n∈N + .

Table 1 :

 1 Four periodic schedules found by Maude for c 1 ≺ c 2 when the bound is set to 4.

	Schedule	Clock/	1	2	3	4	5	6	. . .	Period
		Step								p
	1	c 1 c 2	t i	t t	t t	t t	t t	t t	. . . . . .	1
	2	c 1 c 2	t i	i t	t i	i t	t i	i t	. . . . . .	2
	3	c 1 c 2	t i	t i	t t	t t	t t	t t	. . . . . .	1
	4	c 1 c 2	t i	t i	t i	i t	t i	i t	. . . . . .	2
	set of constraints.

Table 2 :

 2 Six deadlock schedules found by Maude for ccsl constraints Φ 2 . The reason for the deadlock is that the specification does not force in 1 and in 2 to tick simultaneously (see Φ 2 ). If in 1 ticks alone (resp. in 2 ), then out should tick next, but in order to tick out needs both ticks of in 1 and in 2 , as defined by the constraints between in 1 , in 2 and out. However, in 2 (resp. in 1 ) can only tick if out ticks before, which therefore leads to a deadlock.

	No.	in 1	in 2	step 1	step 2	step 3	out	tmp 1	tmp 2
	1	t	i	t	i	i	i	t	i
	2	i	t	i	t	i	i	t	i
	3	t i	i i	i t	i i	i i	i i	t i	i i
	4	i i	t i	i i	i t	i i	i i	t i	i i
	5	t i t	t i i	t i t	t i i	i t i	i t i	t i t	i i t
	6	t i i	t i t	t i i	t i t	i t i	i t i	t i t	i i t
	a deadlock state.

sort CCSLState .

op <_ ; _ ; _ ;_ > : ClockSet Constraints Conf Nat -> CCSLState [ ctor ] .In the initial state of a clock system, the configuration is the set of initial clock triples and the step is 0.1 We keep n in the triple for the efficiency purpose of formal analysis because in this way we do not need to count the number of ticks in every time it is needed.

---Declaration and definition of getPeriod and isPeriodic

op getPeriod : Conf Constraints Nat Nat -> Nat .

search [4] < ( ' c1 , ' c2 ) ; ( ' c1 < ' c2 ) ; [ ' c1 , nil ,0] , [ ' c2 , nil ,0] ; 0 > = >*

< F ; PHI ; X ' ; K ' > such that P := getPeriod (X ' , PHI , sd (K ' ,1) ,K ') .

It is worth mentioning that it does not guarantee that there is no deadlock schedule because only a bounded state space is explored.

http://www.clarity-se.org/

Acknowledgment

We thank all the anonymous reviewers including those who reviewed the workshop version published in FTSCS 2015 for their valuable comments on this work. This research was supported by The National Natural Science Foundation of China (NSFC) project: No. 61502171 and by the French Clarity Project 3 .

3 op isPeriodic : Conf Constraints Nat Nat -> Bool . [START_REF] Potop-Butucaru | The synchronous hypothesis and polychronous languages[END_REF] eq getPeriod (X , PHI , K , K ') = 5 if K > 0 then ( if isPeriodic (X , PHI ,K ,K ') then sd (K ' , K ) else 6 getPeriod (X , PHI , sd (K ,1) ,K ') fi ) Using the rewrite rule defined in Section 4.3, one can find periodic schedules with search command by specifying an extra condition. The condition is that isPeriod must return a non-zero period in the expected configuration. For instance, the following code shows the command to find a periodic schedule for the constraints in Φ 1 and the solution returned by Maude:

The solution states that a periodic schedule is found, whose period is 2 and the starting step of the first period is 2. The returned periodic schedule is essentially the same as the one found by bounded scheduling in Section 5. [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] We can search simultaneously more than one periodic schedules for a given

The arbitration policies can be considered as internal strategies that control how the rewrite rules are applied. Formalizing strategies in Maude can be done using Maude's built-in meta-programming features, in which Maude programs are used as data in formalized strategies. Thanks to this feature, arbitration policies in CCSL can be naturally formalized in Maude.

Below we give partly the Maude definitions of the basic data types, functions and the rewrite rules used to achieve customized simulation. We declare a sort Policy for arbitration policies, and six operators (as shown above at Lines 2 and 3) to represent the six kinds of arbitration policies respectively. A state of a clock system with policy consists of two parts, i.e., a state of the system and a policy, which is formalized as a term [ S, P ] with a state S of sort CCSLState and a policy P of sort Policy. We name the sort of such terms CCSLState4Sim. Behaviors of a clock system with policy can be formalized by the conditional rewrite rule defined at Lines 7 to 8. The main difference with Section 4.3 is that the successor X' of X in the new rule must be the one that follows the given arbitration policy. The basic idea for obtaining such X' is to search by one-step forward from X using the rule defined in Section 4.3 and find all possible successors, which is achieved by function getAllSuccessors. Then, X' is determined according to the given policy, which is achieved by function getConfbyPol.

The two functions getAllSuccessors and getConfbyPol are declared at Lines 5 and 6. In the declaration of getAllSuccessors, ConfSet is a sort to


Miguel Angel Garcia-Ruiz

Arthur Edwards

Raul Aquino-Santos

Miguel Vargas Martin

Samir A El Seoud

Using Auditory Display to Teach Network Intrusion Detection

Keywords: Computer Networks, Intrusion Detection, Auditory Display

Teaching network intrusion detection, or NID (the identification of violations of a security policy in a computer network) is a challenging task, because students need to analyze many data from network logs and in real time to identify patterns of network attacks, making these activities visually tiring. This paper describes an ongoing research concerned with designing and applying sounds that represent meaningful information in interfaces (sonification) to support teaching of NID. An usability test was conducted with engineering students. Natural sound effects (auditory icons) and musical sounds (earcons) were used to represent network attacks. A post-activity questionnaire showed that most students preferred auditory icons for analyzing NID, and all of them were very interested in the design and application of sonifications.

Introduction

The increasing threat of cybernetic attacks has become one of the major concerns of network equipment designers and administrators. An intrusion is defined as an unauthorized access to a computer system violating some security policy. One of the main problems caused by intruders is that they consume or take over resources (e.g., bandwidth, processing power, services) and compromise vulnerable systems. In some cases, even non-vulnerable systems are affected by the massive propagation of malicious software attacks such as computer worms or denial-of-service (DoS) attacks. Moreover, we can not always assume that an intrusion detection system (IDS) can discern between malicious and non-malicious traffic; and even after diagnosing the presence of an intrusion, it requires time to decide on what the reaction should be, when disconnecting or shutting down services are not viable solutions. For an overview of intrusion detection systems see [START_REF] Van Oorschot | A Monitoring System for Detecting Repeated Packets with Applications to Computer Worms[END_REF].

The topic of network intrusion detection, or NID, is generally taught in computer security courses, either in classrooms or in computer rooms [START_REF] Frank | Tutorial on laboratory exercises for a computer security course[END_REF]. However, teaching NID is pedagogically challenging. One of the problems that students face is that they can be easily be confounded by network accesses that appear malicious (false positives) or actual threats or attacks that go undetected (false negatives). Thus, NID is critically important, but it is a timeconsuming process required to distinguish between malicious and non-malicious attacks registered in network logs and in real time. The analysis of network logs and network ports by students in real time can be visually tiring and can possibly overload their visual sensory channel (and their working memory) if it is performed repeatedly, since students have to revise many text lines of network logs and have to be constantly watching in a computer monitor graphical or text reports about network ports accesses in real time. To overcome this, in an educational setting, we propose using sound parameters to represent information on attacks and footprints present in a network log, in addition to the log visualization.

IT security specialists are typically trained (and/or certified) by trusted institutions (such as colleges, universities, or other institutions like the SysAdmin, Audit, Network, Security Institute [3]). The education of these trainees usually covers a number of areas including exploit tools, network traffic analysis (e.g., using tcpdump), incident handling, and of course IDSs (e.g., Snort). Nevertheless, this training is rather conservative, and often does not include new education paradigms such as the one proposed in this paper. We believe that auditory displays will enhance significantly the training of IT security specialists. In this paper we describe this approach, and report on a usability study conducted with individuals who declared to be non-experts on intrusion detection but to have some knowledge in the area.

Past Research on NID Sonification

The Computer Science branch of Auditory Display studies non-verbal sounds that represent meaningful information in a computer interface [START_REF] Kramer | Auditory display: Sonification, audification, and auditory interfaces[END_REF]. Sound is a powerful medium in Human-Computer Interaction (HCI), used mainly for helping humans discriminate data patterns and for representing alarms, as long as the sounds are correctly designed and adapted to the computer interface. However, non-verbal sounds can be annoying if they are played too loud, or distract persons who are nearby. This difficulty may be solved, by doing careful sound design and application [START_REF] Shneiderman | Designing the User Interface: Strategies for Effective Human-Computer Interaction[END_REF]. Sonification is the action of mapping data onto parameters of nonspeech sounds (i.e. volume or loudness, timbre, pitch, duration, frequency, amplitude, and rhythm) in a computer interface [START_REF] Kramer | Auditory display: Sonification, audification, and auditory interfaces[END_REF], and its use includes mapping of scientific data to support search of data trends or patterns.

Auditory Display, and thus sonification, employs a number and types of non-verbal sounds. The most used of these types are auditory icons and earcons. Auditory icons are defined as sound effects found in nature that map information or actions at the computer interface [START_REF] Gaver | Auditory icons, using sound in computer interfaces[END_REF]. This type of sounds and their mappings are generally easy to recognize, but they can be difficult to design. Earcons are composed of abstract, short musical sounds made of string, wind, or percussion instruments, and represent information or activities in interfaces [START_REF] Blattner | Earcons and icons: their structure and common design principles[END_REF]. Earcons are relatively easy to design and create, but their users have to learn the mappings prior their use in an interface.

Sonification has been used in a number of science fields, and has also been successfully applied to computer networks, and particularly to conduct NID analysis. Non-speech sounds have been successfully designed and used, at least in experimental stages, for representing web server status to detect malfunctions and malicious attacks, especially for excessive network traffic, email spam, and denial-of-service (DoS), either in real time and applied in network logs [START_REF] Barra | Personal WebMelody: Customized sonification of web servers[END_REF][START_REF] Gilfix | Peep (The network auralizer): Monitoring your network with sound[END_REF][START_REF] Gopinath | Auralization of intrusion detection system using Jlisten[END_REF].

Our Approach

Sound can be an engaging medium to motivate students, especially to maintain their attention on particular information details and relationships, ease their identification of information patterns and trends, and also to serve as a "mnemonic device" for recalling "chunks" of information, among other advantages [START_REF] Kramer | Auditory display: Sonification, audification, and auditory interfaces[END_REF]. Sonification has been researched and employed successfully in educational settings, for example, for learning molecular biology [START_REF] Garcia-Ruiz | An overview of auditory display to assist comprehension of molecular information[END_REF]. In the case of Network Intrusion Detection, sonification may alleviate students' visual channel from being overloaded, since they generally rely on visual information for discerning network attacks and their characteristics, making this a tedious and long task. The use of multimodal interfaces (including sonification) for NID has been proposed elsewhere by [START_REF] Garcia-Ruiz | Towards a Multimodal Human-Computer Interaction to Analyze Intrusion Detection in Computer Networks[END_REF].

Our research approach focuses on the study of Auditory Display as an effective tool for helping students in NID analysis in an educational setting. One particularly interesting question is whether sonification can lower the cognitive load of students when associating and understanding the relationships between the types of network attacks, the network ports and the occurring times. Our research is based on the Cognitive Load Theory [START_REF] Chandler | Cognitive load theory and the format of instruction[END_REF], which states that effective learning takes place when the working memory load of learners is kept to a minimum to facilitate knowledge transfer to their long term memory, in which cognitive load can be decreased by adding non-redundant auditory and visual learning materials to the working environment.

In our preliminary research, we devised, developed, and tested two sonification prototypes. We sonified a network log downloaded from the Internet [START_REF]DARPA intrusion detection evaluation: Data sets[END_REF], a declassified Defense Advanced Research Projects Agency (DARPA) log from the U.S. that is publically available for research reasons. It contains markers of five types of possible attacks that were mapped onto earcons in the first prototype, and auditory icons in the second one. Those mappings are described in detail and can be downloaded from http://docente.ucol.mx/~mgarcia/Sonificatedlog.htm.. A .WAV file with the log sonification and auditory icons was generated using our program developed in Tcl/Tk language. For the first prototype, these are the mappings of auditory icons to the five types of attacks registered in the log: A frog sound is mapped onto "guess" A cat sound is mapped onto "rcp" A horse sound is mapped onto "rsh" A cock sound is mapped onto "rlogin" A bird sound is mapped onto "port-scan"

We generated a second sonification prototype using earcons (piano notes). These are the mappings of earcons to the five types of attacks registered in the log: A 128Hz key note is mapped onto "guess" A 197Hz key note is mapped onto "port-scan" A 263Hz key note is mapped onto "rcp" A 525Hz key note is mapped onto "rsh" A 1056Hz key note is mapped onto "rlogin"

In an exploratory fashion, the sounds were randomly chosen and downloaded from the Internet, and were designed according to their sound parameters of pitch and timbre, following the Auditory Display design guidelines from [START_REF] Kramer | Auditory display: Sonification, audification, and auditory interfaces[END_REF]. In an attempt to facilitate recognition, all the sounds were played at different stereo positions.

Usability Study

Based on our research approach and using our two sonification prototypes, we conducted an informal usability test with a group of Telematics engineering students. The purpose of our preliminary usability study was to obtain initial student feedback on the delivery media and types of sound sources to represent network attacks, and thus modify them or choose other types of sounds or sound parameters in later developments. Usability measures, among other aspects, the efficiency, efficacy, errors, and pleasantness of use of a computer interface [START_REF] Dumas | A practical guide to usability testing[END_REF]. Usability studies are important because past research has been found that educational software with high usability has a positive support for learning [START_REF] Macfarlane | Assessing usability and fun in educational software[END_REF].

Test Design

We designed a usability test, which was carried out with a group of students. After the test, we administered a post questionnaire with questions to obtain subjective opinions on the sounds quality and sound sources for representing attacks in NID, as well as the pleasantness of the sounds played.

Materials

For playing the sonifications, a set of Labtec Pulse 475 computer speakers (comprised of a pair of speakers and a subwoofer, rated at 28 Watts RMS) was used for playing the sonifications. We used this set of speakers because of its low cost, easy transport, simple set up, good audio fidelity, and loudness. The speakers were placed on tripods in front of the classroom to ensuring all students could easily listen to the sounds, and were placed at a height of approximately 1.80 meters, and had about five meters of separation. We used a laptop that was connected to a data projector to show the test objective and the log sound mappings, as well as to play the prototype sonifications. The speaker set up is shown in Figure 1. The sonification prototypes earlier described in this paper were used in the test.

Participants of the Test

Twenty-nine Telematics Engineering students were asked to volunteer in the usability test. The students averaged 20 years (3 women and 26 men), representing both the size and the composition of a typical class at the College of Telematics of the University of Colima.

Although most of the students knew the basics of computer networks, none of them knew of network intrusion detection. Sixteen participants had received differing degrees of musical training or knew how to play a musical instrument, and none reported to suffer hearing problems. Although none of them have designed auditory icons or earcons before, most of them are competent in computer programming.

Procedure

To assure ecological validity to the usability test, it was conducted in one of the classrooms of the College of Telematics. The purpose of the test and its sound mappings were explained to the students using a Powerpoint projection. The students listened to the sound mappings (earcons and auditory icons) and read their corresponding network values on the projection four times. After that, students listened to the two sonification prototypes only; the Powerpoint projection was turned off. The auditory icons' sonification was played first. After playing the sonification, a number of questions were asked, including: How many auditory icons could you identify? What is the auditory icon mapping to "port-scan" and "rlogin"? Next, the earcons sonification was played, and the same questions again asked. After playing the sonifications, a usability questionnaire was administered to the students, which included questions with Likert scales, as shown in Table 2.

Results

Table 1 summarizes a list of earcons and auditory icons that students suggested in the questionnaire for making new non-speech sounds to represent network attacks. We found that most of the suggested auditory icons are of violent nature. Eight students preferred to use guitar sounds for developing earcons. Similarly, a different set of eight students suggested drums for earcons. The other students listed diverse musical instruments. Table 2 depicts some of the questions with Likert scales about the sound usability.

Likert scales

Average scale value

The sounds volume level (loudness) was perceived as adequate 1

The sounds were clearly heard

6(8)
The auditory icons were useful for recalling the attacks 1 The earcons were useful for recalling the attacks 5 Both earcons and auditory icons can be useful for learning NID 2 Table 2. Opinion scales of the questionnaire (1=strongly agree, 5=strongly disagree)

Conclusions

This paper described an exploratory research concerned with designing and applying sounds that represent meaningful information in interfaces (sonification) to support teaching of NID.

An usability test was conducted with Telematics students, where natural sound effects (auditory icons) and musical sounds (earcons) were used to represent network attacks. A postactivity questionnaire showed that most students preferred auditory icons for analyzing NID, and all of them were very interested in the design and application of sonifications.

The previous musical training of some students did not affect their outcome in the postquestionnaire; their answers were consistent with the rest of the group. Men and women reached almost the same conclusions on their usability opinions. In addition, none of the students complained about the speakers' sound quality. This means that even modest sound equipment can be effective for delivering sonifications in classrooms. Most of the students showed enthusiastic in the test, and wished to continue on participating in testing NID sonifications. As this usability test was informal, further usability studies are needed to study the sonifications in controlled experiments and in different educational settings, for example, in a computer room.

However, there was no student consensus on which sounds would best represent software or hacker attacks in a network using auditory icons and earcons. Interestingly, one student suggested using Morse code to represent NID. Auditory icons appeared to perform better in identifying attacks, although more formal usability tests are needed to confirm this. Earcons did have a flaw in their design; the piano notes, although were distinctive from one another in terms of pitch, all of them were made of piano notes. They should be made of different musical instruments to ease mappings learning.

The students' comments indicate that the auditory icons and earcons played at different stereo positions helped them to better identify the mappings of the network attacks. Also, the speaker separation was very effective for conveying a stereo sound effect.

In further sonification prototypes, we will let students choose their own sounds (auditory icons and earcons) from a repertoire. This certainly will help them to remember the mappings between the types of attacks and the sounds. In addition, we will test new forms of mapping the network attacks with non-speech sounds, as well as other types of sound delivery media, such as headphones or more powerful speakers.

Figure 1 .

 1 Figure 1. Students participating in the usability test.

Sounds for creating earcons Sounds for creating auditory icons

	Guitar	Breaking glass
	Electric guitar	Breaking china (plates)
	Drums	Water stream
	Trumpets	Thunder
	Violin	Nature sounds
	Bass	Rain
	Cello	Beach waves
	Piano	Cars crashing
	Flute	Screams
		Dog barking

Table 1 .

 1 A summary of the sounds suggested by students for representing network attacks.

September 26 -28, 2007 Villach, Austria 5[START_REF] Gopinath | Auralization of intrusion detection system using Jlisten[END_REF]

Authors:

Miguel Angel Garcia-Ruiz, Ph.D.