Charles André

Julien Deantoni

Frédéric Mallet

Robert De Simone

The Time Model of Logical Clocks available in the OMG MARTE prole

Multiform logical time, introduced and made popular through its central role in Synchronous Language theory, is already present in many formalisms pertaining to embedded system design, although usually in a hidden fashion. Logical time considers time bases that can be generated from any sort of sequences of events, not necessarily equally spaced in physical time. Our main goal here is to capture some of the essence of multiform logical time, and encapsulate it into a dedicated syntax (ccsl, Clock Constraint Specication Language, part of the uml prole for marte). ccsl provides ways to express loose or strict constraints between distinct logical clocks. Solving such clock constraints amounts to relating clocks to a common reference one, which then can be thought of as closer to physical. We motivate the role of marte Time Model and ccsl by using them to explain and formally characterize important semantic features of east-adl/autosar, aadl, and Ptolemy's sdf models.

before they are actually built. Architecture exploration is becoming a key ingredient of embedded system design, where applications and execution platforms are essentially designed jointly and concurrently at model level; 2. Applications are often reactive by nature, that is, meant to react repeatedly with an external environment. The main design concern goes with handling data or control ow propagation, which includes frequently streaming and pipelined processings. In contrast, the actual data values and computation contents are of lesser importance (for design, not for correctness). Application models such as process networks, reactive components and state/activity diagrams are used to represent the structure and the behavior of such applications (more than usual software engineering notions such as classes, objects, and methods); 3. Designs are usually subject to stringent real-time requirements, imposed from above, while they are constrained by the limitations of their components and the availability of execution platform resources, from below.

Allocation models can here serve to check at early stages whether there exist feasible mappings and schedulings of application functions to architecture resources and services that may match the requirements under the given constraints.

The model-driven approach to embedded system engineering is often tagged as Y-Chart methodology, or also Platform-Based design. In this approach, application and architecture (execution platform) models are developed and rened concurrently, and then associated by allocation relationships, again at a virtual modeling level.

The representation of requirements and constraints in this context becomes itself an important issue, as they guide the search for optimal solutions inside the range of possible allocations. They may be of various natures, functional or extra-functional. In this article, we focus on requirements and constraints which we call logical functional timing, and which we feel to be an important (although too often neglected or misconceived) aspect of embedded system modeling.

Timing information in modeling is often used as extra-functional, real-time annotations analyzed mostly by simulation. But the relevance of these timing gures in later implementations has to be further assessed then. On the other hand, time information also carries functional intent, as it selects some behaviors and discards others. Very often this can be done not only by using single form physical time, but also logical multiform time models. For instance, it may be sucient to state that a process runs twice as fast as another, or at least as fast as the second, without providing concrete physical time gures. The selected solutions will work for any such physical assignment that matches the logical time constraints. Also, durations may be counted with events that are not regular in physical time: the number of clock cycles of a processor in a low-power design context may vary according to frequency scaling or clock gating; processing functions may be indexed by the engine crankshaft revolution angle in case of automotive applications. Other examples abound in the embedded design world. Modeling with logical time partial ordering was advocated in [START_REF] Lee | A framework for comparing models of computation[END_REF]. The notion of multiform (or polychronous) logical time has been exploited extensively in the theory of Synchronous languages [START_REF] Benveniste | The synchronous languages twelve years later[END_REF], in hdls (Hardware Description Languages), but also importantly in the many approaches of model-based scheduling theories around process networks [START_REF] Eker | Taming heterogeneity -the ptolemy approach[END_REF][START_REF] Sriram | Embedded Multiprocessors Scheduling and Synchronization[END_REF] and formal data/control-ow graphs synthesized from nested loop programs [START_REF] Feautrier | Compiling for massively parallel architectures: a perspective[END_REF]. Software pipelining and modulo scheduling techniques are based on such logical time counted in parallel processor execution cycles. The important common feature of all these approaches is that (logical) time is an integral part of the functional design, to be used and maintained along compilation/synthesis, and not only simulation. In many cases the designer is fronted with time decisions in order to specify correct behaviors. This is of course largely true also of classical physical real-time requirements, but their operational demand is usually downplayed as they are only considered for analysis, not synthesis. Many of the techniques are still shared between both worlds (for instance consider zero-time abstraction of atomic behaviors, and progress all behaviors in correct causal order in a run-to-completion mode before time may pass in a discrete step). Some techniques are still dierent, and certainly the goals are, but the underlying models are similar. Large and heterogeneous systems require a single common environment to integrate all these models while still preserving the semantics and the analysis techniques of each of them.

We consider here the use of existing modeling tools to integrate all these models. The uml appears as a good candidate since it has unied in a common syntactic notation most of the underlying formal models generally used for embedded systems: state machines, data-ow graphs (uml activities), static models to describe the execution platforms (block diagrams). It is even more relevant because the uml prole for marte, recently adopted by the omg, proposes extensions to uml specically targeting real-time and embedded systems. Our goal is to provide an explicit formal semantics to the uml elements so that it can be referred to as a golden model by external tools and make the model amenable to formal analysis, code generation or synthesis.

An explicit and formal semantics within the model is fundamental to prevent dierent analysis tools from giving a dierent semantics to the same model. Each analysis technique relies on a specic formal model that has its own model of computation and communication (mocc). We propose a language, called Clock Constraint Specication Language (ccsl), specically devised to equip a given model (conformant to the uml or to any domain-specic language) with a timed causality model and thus dene a specic mocc. When considering uml models, ccsl relies on the marte time subprole to identify model elements on which ccsl constraints apply.

In this chapter, we select dierent models from dierent domains to illustrate possible uses of ccsl. First, we show how it can be used to express classical constraints of the real-time and embedded domain by expressing east-adl [START_REF]East-ADL2 specication[END_REF] extra-functional properties in ccsl. east-adl proposes a set of time requirements classical in automotive applications (duration, deadline, jitter) and on which time requirements for autosar3 are being built. The second illustration falls in the avionics domain and focuses on aadl (Architecture & Analysis Description Language) [START_REF] Feiler | The architecture analysis & design language (AADL): An introduction[END_REF]. aadl is an Architecture Description Language (adl) adopted by the sae (Society of Automotive Engineering) that oers specic support for schedulability analysis. It also considers classical computation (periodic, sporadic, aperiodic) and communication (immediate/delayed, event-based or timed-triggered) patterns. However, it departs from east-adl because it explicitly considers the execution platform to which the application is allocated. Our illustration uses marte (and notably its allocation subprole) to build a model amenable to architecture exploration and schedulability analysis. These rst two examples consider models that combine logical and physical time. The last example considers a purely logical case. A ccsl library that species the operational semantics of the Synchronous Data Flow (sdf [START_REF] Lee | Static scheduling of synchronous data ow programs for digital signal processing[END_REF]) is built. This library is applied to several diagrammatic views, equipping purely syntactic models with an explicit behavioral semantics.

Section 2 gives a general overview of marte, a detailed view of the time subprole and of its facilities to annotate uml models with (logical) time. Then, Section 3 describes the ccsl syntax and semantics together with the mechanisms for building libraries. It also introduces timesquare, the dedicated environment we have built to analyze and verify uml/marte/ccsl models. The following sections address several possible usages of ccsl and describe ccsl libraries for the dierent sub-domains: automotive and east-adl in Section 4, avionics and aadl in Section 5, static analysis and sdf in Section 6. [START_REF] Benveniste | The synchronous languages twelve years later[END_REF] The UML Prole for MARTE

Overview

The Unied Modeling Language (uml) [START_REF] Omg | Unied Modeling Language, Superstructure, v2.2[END_REF] is a general-purpose modeling language specied by the Object Management Group (omg). It proposes graphical notations to represent all aspects of a system from the early requirements to the deployment of software components, including design and analysis phases, structural and behavioral aspects. As a general-purpose language, it does not focus on a specic domain and maintains a weak, informal semantics to widen its application eld. However, when targeting a specic application domain and especially when building trustworthy software components or for critical systems where life may be at stake, it is absolutely required to extend the uml and attach a formal semantics to its model elements. The simplest and most ecient extension mechanism provided by the uml is through the denition of proles. A uml prole adapts the uml to a specic domain by adding new concepts, modifying existing ones and dening a new visual representation for others. Each modication is done through the denition of annotations (called stereotypes) that introduce domain-specic terminology and provide additional semantics. However, the semantics of stereotypes must be compatible with the original semantics (if any) of the modied or extended concepts.

The uml prole for Modeling and Analysis of Real-Time and Embedded systems (marte [START_REF] Omg | 1.0. Object Management Group[END_REF]) extends the uml with concepts related to the domain of real-time and embedded systems. It supersedes the uml prole for Schedulability, Performance and Time (spt [START_REF] Omg | UML Prole for Schedulability, Performance, and Time specication, v1.1. Object Management Group[END_REF]) that was extending the uml 1.x and that had limited capabilities. marte has three parts: Foundations, Design and Analysis. The foundation part is itself divided into ve chapters: CoreElements, NFP, Time, Generic Resource Modeling and Allocation. CoreElements denes congurations and modes, which are key parameters for analysis. In real-time systems, preserving the non-functional (or extra-functional) properties (power consumption, area, nancial cost, time budget. . . ) is often as important as preserving the functional ones. The uml proposes no mechanism at all to deal with nonfunctional properties and relies on mere string for that purpose. NFP (Non Functional Properties) oers mechanisms to describe the quantitative as well as the qualitative aspects of properties and to attach a unit and a dimension to quantities. It denes a set of predened quantities, units and dimensions and supports customization. NFP comes with a companion language called VSL (Value Specication Language) that denes the concrete syntax to be used in expressions of non-functional properties. VSL also recommends syntax for user-dened properties. Time is often considered as an extra-functional property that comes as a mere annotation after the design. These annotations are fed into analysis tools that check the conformity without any actual impact on the functional model: e.g., whether a deadline is met, whether the end-to-end latency is within the expected range. Sometimes though, time can also be of a functional nature and has a direct impact on what is done and not only when it is done. All these aspects are addressed in the time chapter of marte. The next section elaborates on the time prole.

The design part has four chapters: High Level application modeling, Generic component modeling, Software Resource Modeling, and Hardware Resource Modeling. The rst chapter describes real-time units and active objects. Active objects depart from passive ones by their ability to send spontaneous messages or signals, and react to event occurrences. Normal objects, the passive ones, can only answer to the messages they receive. The three other parts provide a support to describe resources used and in particular execution platforms on which applications may run. A generic description of resources is provided, including stereotypes to describe communication media, storages and computing resources. Then this generic model is rened to describe software and hardware resources along with their non-functional properties.

The analysis part also has a chapter that denes generic elements to perform model-driven analysis on real-time and embedded systems. This generic chapter is specialized to address schedulability analysis and performance analysis. The chapter on schedulability analysis is not specic to a given technique and addresses various formalisms like the classic and generalized Rate Monotonic Analysis (RMA), holistic techniques, or extended timed automata. This chapter provides all the keywords usually required for such analyses. In Section 5, we follow a rather dierent approach and instead of focusing on syntactic elements usually required to perform schedulability analysis (periodicity, task, scheduler, deadline, latency), we show how we can use marte time model and its companion language ccsl to build libraries of constraints that reect the exact same concepts. Finally, the chapter on performance analysis, even if somewhat independent of a specic analysis technique, emphasizes on concepts supported by the queueing theory and its extensions. marte extends the uml for real-time and embedded systems but should be rened by more specic proles to address specic domains (avionics, automotive, silicon) or specic analysis techniques (simulation, schedulability, static analysis). The three examples addressed here consider dierent domains and/or dierent analysis techniques to motivate the demand for a fairly general time model that has justied the creation of marte time subprole.

The Time prole

Time in spt is a metric time with implicit reference to physical time. As a successor of spt, marte supports this model of time. uml 2, issued after spt, has introduced a model of time called SimpleTime [START_REF] Omg | Unied Modeling Language, Superstructure, v2.2[END_REF]Chap. 13]. This model also makes implicit reference to physical time, but is too simple for use in real-time applications, and was initially devised to be extended in dedicated proles. marte goes beyond spt and uml 2. It adopts a more general time model suitable for system design. In marte, Time can be physical, and considered as continuous or discretized, but it can also be logical, and related to user-dened clocks. Time may even be multiform, allowing dierent times to progress in a non-uniform fashion, and possibly independently to any (direct) reference to physical time.

In marte, time is represented by a collection of Clocks. Each clock species a totally ordered set of instants. There may be dependence relationships between instants of dierent clocks. Thus this model, called the marte time structure, is akin to the Tagged Systems [START_REF] Lee | A framework for comparing models of computation[END_REF]. To cover continuous and discrete times, the set of instants associated with a clock can either be dense or discrete. In this paper, most clocks are discrete (i.e., they represent discrete time). In this case the set of instants is indexed by natural numbers. For a clock c, c[k] denotes its k th instant.

The marte Time prole denes two stereotypes ClockType and Clock to represent the concept of clock. ClockType gathers common features shared by a family of clocks. The ClockType xes the nature of time (dense or discrete), says whether the represented time is linked to physical time or not (respectively identied as chronometric clocks and logical clocks), chooses the type of the time units. A Clock, whose type must be a ClockType, carries more specic information such as its actual unit, and values of quantitative (resolution, oset, etc.) or qualitative (time standard) properties, if relevant.

TimedElement is another stereotype introduced in marte. A timed element is explicitly bound to at least one clock, and thus closely related to the time model. For instance, a TimedEvent, which is a specialization of TimedElement extending uml Event, has a special semantics compared to usual events: it can occur only at instants of the associated clock. In a similar way, a TimedVal-ueSpecication, which extends uml ValueSpecication, is the specication of a set of time values with explicit references to a clock, and taking the clock unit as time unit. Thus, in a marte model of a system, the stereotype TimedElement or one of its specializations is applied to model elements which have an inuence on the specication of the temporal behavior of this system.

The marte Time subprole also provides a model library named TimeLibrary. This model library denes the enumeration TimeUnitKind which is the standard type of time units for chronometric clocks. This enumeration contains units like s (second), its submultiples, and other related units (minute, hour. . . ). The library also predenes a clock type (IdealClock) and a clock (idealClk) whose type is IdealClock. idealClk is a dense chronometric clock with the second as time unit. This clock is assumed to be an ideal clock, perfectly reecting the evolutions of physical time. idealClk should be imported in user's models with references to physical time concepts (i.e., frequency, physical duration, etc.). This is illustrated in Sections 4 and 5.

CCSL Time Model

3.1 The Clock Constraint Specication Language ccsl is a language to impose dependence relationships between instants of dierent clocks. This dependency is specied by Clock constraints. A Clock-Constraint is a TimeElement that extends uml Constraint. The constrained elements are clocks. A clock constraint imposes relationships between instants of its constrained clocks. So, to understand clock constraints, we have rst to dene relations on instants.

Instant Relations

The precedence relation ≼ is a reexive and transitive binary relation on set of instants. From ≼ we derive four new relations: Coincidence

(≡ ≜ ≼ ∩ ≽), Strict precedence (≺ ≜ ≼ \ ≡), Independence (∥ ≜ ≼ ∪ ≽),

Clock relations

Specifying a full time structure using only instant relations is not realistic. Moreover a set of instants is usually innite, thus forbidding an enumerative specication of instant relations. Hence the idea to extend relations to clocks. ccsl denes ve basic clock relations. In the following denitions, a and b stand for Clocks. For simplicity, mathematical expressions are given only in the case of discrete clocks.

Subclocking: a ⊂ b means that each instant of a is coincident with an instant of b, and that the coincidence mapping is order-preserving. a is said to be a subclock of b, and b a superclock of a.

Equality: a = b is a special case of subclocking where the coincidence

mapping is a bijection. ∀k ∈ N ⋆ , a[k] ≡ b[k]. a and b are synchronous. Precedence: a ≼ b means ∀k ∈ N ⋆ , a[k] ≼ b[k]. a is said to be faster than b.
Strict precedence: a ≺ b is similar to the previous one but considers the

strict precedence instead. ∀k ∈ N ⋆ , a[k] ≺ b[k].
Exclusion: a # b means that a and b have no coincident instants.

The Alternation a ∼ b, used in the application sections, is a derived clock

relation that imposes ∀k ∈ N ⋆ , a[k] ≺ b[k] ≺ a[k + 1]. a alternates with b.

Clock expressions

They allow denitions of new clocks from existing ones. For instance, Filtering is an often used clock expression. Let a be a clock, and w a binary word (i.e., a nite or innite word on bits: w ∈ {0, 1} * ∪ {0, 1} ω ). w is used as a ltering pattern. a ▼ w denes a new clock, say b,

such that ∀k ∈ N ⋆ , b[k] ≡ a[w ↑ k],
where w ↑ k is the index of the k th 1 in w. Binary words are convenient representations of Boolean ows and schedules. A schedule is an activation sequence, generally periodic in which case periodic binary words are used, denoted as w = u(v) ω , where u (prex) and v (period) are nite binary words. w is the innite binary word u There also exist mixed constraints in which case the two meta-attributes are set to true. A third meta-attribute (isChronometricBased) is used only for chronometric clocks and quantitative time constraints such as stability, skew.

• v • • • • • v • • • • . Periodic

Temporal evolutions

A ccsl specication imposes a complex ordering on instants. We do not explicitly represent this time structure. We compute possible runs instead. A run is a sequence of steps. Each step is a set of clocks that are simultaneously red without violating any clock constraint. When a discrete clock ticks (or res), the index of its current instant is incremented by 1. The computation of a step is detailed in a technical report [START_REF] André | Syntax and Semantics of the Clock Constraint Specication Language (CCSL)[END_REF] that provides a syntax and an operational semantics for a kernel of ccsl. Here, we just sketch this process.

Using the semantics of ccsl, from a clock constraint specication S we derive a logical representation of the constraints S . This representation is a Boolean expression on a set of Boolean variables V, in bijection b with the set of clocks C. Any valuation v : V → {0, 1} such that S (v) = 1 indirectly represents a set of clocks F that respects all the clock constraints: CCSL libraries ccsl specications are executable specications. However, the expressiveness of the kernel ccsl is limited, for instance by the lack of support for parameterized constructs. The full ccsl overcomes these limitations through libraries.

F = {c ∈ C | v(b(c)) = 1}. F is
A library is a collection of parameterized constraints, using constraints from one or many other libraries. The primitive constraints, which constitute the kernel ccsl, are grouped together in the kernel library. The operational semantics is explicitly dened only for the constraints of the kernel library. Each user-dened constraint is structurally expanded into kernel constraints, thus dening its operational semantics. def

≡ (clock v1, clock v2, clock v3) ≜ (v1 = v2) | (v1 = v3)
ccsl libraries are used in the remainder of the paper either to group domain specic constraints (Section 4) or to encapsulate a specic mocc (Section 6). timesquare is released as a set of Eclipse plug-ins. A detailed description of timesquare features, examples, and video demonstrations are available from its website (http://www-sop.inria.fr/aoste/dev/time_square).

Summary

In marte, clock constraints impose physical time or logical time (causal) relationships between timed elements. ccsl is a formal specication language, so that clock constraints expressed in ccsl are executable in the timesquare environment. They are also amenable to analysis. Note that while fully integrated with concepts from the marte prole, ccsl can be used outside the uml, for instance within the framework of a dsl. The purpose remains the same: to provide a time causality model tting a model-driven approach.

MARTE and East-ADL2

We consider here an example from the automotive domain. We build a ccsl library for expressing the semantics of east-adl time requirements. Their semantics is left informal in the east-adl specication and we had to disambiguate some of their denitions to build our ccsl model. By building this library we make east-adl requirement specications executable and allow the use of timesquare to execute and animate uml models annotated with eastadl stereotypes.

East-ADL2

east-adl (Electronic Architecture and Software Tools, Architecture Description Language) has been initially developed in the context of the East-EEA European project [START_REF] East | Denition of language for automotive embedded electronic architecture approach[END_REF]. To integrate proposals from the emerging standard autosar and from other requirement formalisms like sysml [START_REF] Weilkiens | Systems Engineering with SysML/UML: Modeling, Analysis, Design[END_REF][START_REF] Omg | Systems Modeling Language (SysML) Specication, v1.1. Object Management Group[END_REF], a new release called east-adl2 [START_REF] Cuenot | Managing complexity of automotive electronics using the East-ADL[END_REF][START_REF]East-ADL2 specication[END_REF] has been proposed by the atesst project. In this section, we abusively refer to both versions under the name east-adl.

Structural modeling in east-adl covers both analysis and design levels.

In this chapter the focus is on the analysis level and especially on timing requirements.

Timing Requirements east-adl requirements extend sysml requirements and express conditions that must be met by the system. They usually enrich the functional architecture with extra-functional characteristics such as variability and temporal behavior. We focus on the three kinds of timing requirements available in east-adl:

1. DelayRequirement that constrains the delay from a set of entities until another set of entities. It species the temporal distance between the execution of the earliest from entity and the latest until entity;

2. RepetitionRate that denes the inter-arrival time of data on a port or the triggering period of an elementary ADLFunction; 3. Input/outputSynchronization that expresses a timing requirement on the input/output synchronization among the set of ports of an ADLFunction.

It should be used to express the maximum temporal skew allowed between input or output events or data of an ADLFunction.

Timing requirements specialize the meta-class TimingRestriction, which denes bounds on system timing attributes. The timing restriction can be specied as a nominal value, with or without a jitter, and can have lower and upper bounds. The jitter is the maximal positive or negative variation from the nominal value. A bound is a real value associated with an implicit time unit (ms, s. . . ).

Example

As an illustration, we consider an Anti-lock Braking System (ABS). This example and the associated timing requirements are taken from the atesst report on east-adl timing model [START_REF] Johansson | ATESST timing model[END_REF]. The ABS architecture consists of four sensors, four actuators and an indicator of the vehicle speed. The sensors (i f l , i f r , i rl , i rr ) measure the rotation speed of the vehicle wheels. The actuators (o f l , o f r , o rl , o rr ) indicate the brake pressure to be applied on the wheels.

The FunctionalArchitecture is composed of FunctionalDevices for sensors and actuators and an ADLFunctionType for the functional part of the ABS. An ADLOutFlowPort provides the vehicle speed (speed).

The execution of the ABS is triggered by the occurrences of event R (Fig. 1). Parameter Ls represents the latency of sensor sampling. The values of the four sensors involved in the ABS must arrive on the input ADLFlowPorts within delay Jii (InputSynchronization). A similar OuputSynchronization delay Joo is represented on the output interface side. Lio represents the delay from the rst event occurrence on the input set of the ABS until the last event occurrence on the output set. The sampling interval of the sensor is given by parameter H. requirements can be modeled simply by using ccsl relations. To ease the use of such relations, user-dened relations are proposed and grouped together in a library.

Applying the UML prole for Marte

The ABS function is modeled in uml (Fig. 2) and some model elements

| element isPeriodicOn c 1 period rate

| element hasStability jitter/rate

This relation denition involves three ccsl constraints. For the duration to be specied in seconds (time unit s), we use the clock idealClk dened in the marte time library (Section 3). The ccsl expression discretizedBy discretizes idealClk and denes a chronometric discrete clock c 1 so that the distance between two successive instants of c 1 is 0.001 s (Eq. 1). The unit (here s) is the default unit dened for idealClk and therefore c 1 is a 1 kHz chronometric clock. Eq. 2 uses the ccsl expression isPeriodicOn to undersample c 1 and build another clock element, rate times slower than c 1 . The clock expression isPeriodicOn has not been described before but Eq. 2 is equivalent to Eq. 4.

element = c 1 ▼ (1.0 rate-1 ) ω (4) Finally, Eq. 3 expresses the jitter of the repetition rate. The ccsl constraint hasStability states that the clock element is not strictly periodic: a maximal relative variations of jitter/rate is possible on its period.

Back to the example of the ABS. One timing requirement of the atesst example species that the ABS function must be executed every 5 ms with a maximum jitter of 1 ms. If abs.start is the clock that triggers the execution of the function ABS, then repetitionRate(f.start, 5, 1) enforces this requirement. A jitter of 1 ms for a nominal period of 5 ms corresponds to a stability of 20 %.

Delay requirements

A DelayRequirement constrains the delay between a set of inputs and a set of outputs. At each iteration, all inputs and outputs must occur. So, dening a delay requirement between two model elements means constraining the temporal distance between the i th occurrences of their events. In the atesst example, a delay requirement is used, for instance to constrain the end-toend latency for the function ABS. The denition is that at each iteration, the distance between the reception of the rst input and the emission of the last output must be less than 3 ms. Consequently, we dene a ccsl clock relation named distance that has three parameters: begin, end and duration. The specication is that the distance between the i th occurrence of begin and the i th occurrence of end must be less than duration ms. If we need a better precision than the ms we may dene a 10 kHz chronometric clock rather than a 1kHz one (Eq. 5).

def distance(clock begin, clock begin, int duration) ≜ clock c 10 = idealClk discretizedBy 0.0001 [START_REF] Douglass | Real-time UML[END_REF] | end ≺ (begin delayedFor duration on c 10 )

(6)
The ccsl clock expression delayedFor is a ternary operator. a delayedFor 3 on b builds a clock c that is a subclock of b. Operator delayedF or expresses a pure delay where the delay duration is in number of ticks of b. Note that this operator is polychronous, contrary to usual synchronous delay operators (pre in Lustre, $ in Signal). In section 6, we use the synchronous form of this operator where the third parameter is implicit (i.e., a delayedFor 3 on a).

To specify the end-to-end latency, we need clocks to model the arrival of the earliest input and of the latest output. Kernel ccsl expressions inf and sup are used for that purpose.

clock i inf = inf(i f l , i f r , i rl , i rr ); clock i sup = sup(i f l , i f r , i rl , i rr ); stating that the end-to-end latency of the function ABS is less than 3 ms is simply written distance(i inf , o sup , 30) in ccsl.

clock o inf = inf(o f l , o f
Similarly, input (resp. output) synchronizations are specializations of a delay requirement. An input synchronization delay requirement for the function ABS bounds the temporal distance between the earliest input and the latest input (specied by Jii on Fig. 1). distance(i inf , i sup , 5) enforces an input synchronization of 0.5 ms. Likewise, an output synchronization bounds the temporal distance between the earliest output and the latest output (specied by Joo on Fig. 1). distance(o inf , o sup , 5) enforces an output synchronization of 0.5 ms.

Analysis of East-ADL specication

In timesquare, we have implemented a specic set of menus to build eastadl specications. The menus give access to the dierent east-adl keywords and to the ccsl library for east-adl. Hence, an east-adl specication can be built interactively. Actually, the menu builds an internal model of the specication as well as a uml marte model. The internal model can be transformed into either a pure east-adl model or a pure ccsl specication. The east-adl model can be used by east-adl-compliant tools. The ccsl specication can be analyzed by the timesquare clock calculus engine to detect inconsistent specications or to execute the uml model. The execution trace can be dumped as a VCD le or can drive the animation of the uml model. Figure 3 shows an example of trace resulting from a complete specication of the ABS. This execution exhibits a violation of the specication because all the computations of the ABS itself, its sensors and actuators cannot be executed within the specied repetition rate of 5 ms. A complete analysis of this particular example is available [START_REF] Mallet | Marte CCSL to execute East-ADL timing requirements[END_REF].

MARTE and AADL

In this second example, we consider aadl and use a combination of marte and ccsl to build its software components, execution platform components, express the binding relationships, and its rich model of computations and communications. Our intent is to allow a uml marte representation of aadl models so as uml models can benet from the analysis tools (mainly for schedulability analysis) that accept aadl models as inputs.

AADL

Modeling elements aadl supports the modeling of application software components (thread, subprogram, and process), execution platform components (bus, memory, processor, and device) and the binding of software onto execution platform. Each model element (software or execution platform) must be dened by a type and comes with at least one implementation.

The latest aadl specication acknowledge that marte should be used to provide a uml-based front-end to aadl models and the marte specication provides a full annex on the matter [START_REF] Faugère | Marte: Also an UML prole for modeling AADL applications[END_REF]. However, even though the annex gives full details on syntactic equivalences between marte stereotypes and aadl concepts, it does not say much about the semantic equivalence.

AADL application software components

Threads are executed within the context of a process, therefore the process implementations must specify the number of executed threads and their interconnections. Type and implementation declarations also provide a set of properties that characterizes model elements. For threads, aadl standard properties include the dispatch protocol (periodic, aperiodic, sporadic, background), the period (if the dispatch protocol is periodic or sporadic), the deadline, the minimum and maximum execution times, along with many others.

We have created a uml library to model aadl application software components [START_REF] Lee | Dealing with AADL end-to-end ow latency with UML Marte[END_REF]. aadl threads are modeled using the stereotype SwSchedulableResource from the marte Software Resource Modeling sub-prole. Its metaattributes deadlineElements and periodElements explicitly identify the actual properties used to represent the deadline and the period. Using a metaattribute of type Property avoids a premature choice of the type of such properties. This makes it easier for the transformation tools to be language and domain independent. In our library, marte type NFP_Duration is used as an equivalent for aadl type Time.

AADL ows

aadl end-to-end ows explicitly identify a data-stream from sensors to the external environment (actuators). Fig. 4 shows an example previously used [START_REF] Feiler | Flow latency analysis with the architecture analysis and design language[END_REF] to discuss ow latency analysis with aadl models. This ow starts from a sensor (Ds, an aperiodic device instance) and sinks in an actuator (Da, also aperiodic) through two process instances. The rst process executes the rst two threads while the last thread is executed by the second process. The two devices are part of the execution platform and communicate via a bus (db1) with two processors (cpu1 and cpu2), which host the three threads with several possible bindings. All processes are executed by either the same processor, or any other combination. One possible binding is illustrated by the dashed arrows. The component declarations and implementations are not shown. Several congurations deriving from this example are modeled with marte and discussed in Section 5.2.

AADL ports

There are three kinds of ports: data, event and event-data. Data ports are for data transmissions without queueing. Connections between data ports are either immediate or delayed. Event ports are for queued communications. The queue size may induce transfer delays that must be taken into account when performing latency analysis. Event data ports are for message transmission with queueing. Here again the queue size may induce transfer delays. In our example, all components have data ports represented as a lled triangle. We have omitted the ports of the processes since they are required to be of the same type as the connected port declared within the thread declaration and are therefore redundant.

uml components are linked together through ports and connectors. No queues are specically associated with connectors. The queueing policy is better represented on a uml activity diagram that models the algorithm. A uml activity is the specication of parameterized behavior as the coordinated sequencing of actions. The sequencing is determined by token ows. A token contains an object, datum, or locus of control. A token is stored in an activity node and can move to another node through an edge. Nodes and edges have ow rules that dene their semantics. In uml, an object node (a special activity node) can contain 0 or many tokens. The number of tokens in a object node can be bounded by setting its property upperBound. The order in which the tokens present in the object node are oered to its outgoing edges can be imposed (property ordering). FIFO (First-In First-Out) is a predened ordering value. So, object nodes can be used to represent both event and event-data aadl communication links. The token ow represents the communication itself. The standard rule is that only a single token can be chosen at a time. This is fully compatible with the aadl dequeue protocol OneItem. The uml representation of the aadl dequeue protocol AllItems is also possible. This needs the advanced activity concept of edge weight, which allows any number of tokens to pass along the edge, in groups at one time. The weight attribute species the minimum number of tokens that must traverse the edge at the same time.

Setting this attribute to the unlimited weight (denoted `*') means that all the tokens at the source are oered to the target.

To model data ports, uml provides datastore object nodes. In these nodes, tokens are never consumed thus allowing multiple readings of the same token. Using a data store node with an upper bound equal to one is a good way to represent aadl data port communications.

Describing AADL models with MARTE AADL ows with MARTE

We choose to represent the aadl ows using a uml activity diagram. Fig. 5 gives the activity diagram equivalent to the aadl example described in Fig. 4.

The diagram was built with Papyrus (http://www.papyrusuml.org), an open-source uml graphical editor. As discussed previously, object nodes are used to represent the queues between two tasks. This uml diagram is untimed and we use marte Time Prole to add time information. This diagram is a priori polychronous since each aadl task is independent of the other tasks. The rst action to describe the time behavior of this model is to build ve logical clocks (ds, t1, t2, t3, da). This is done in two steps. Firstly, a logical, discrete, clock type called AADLTask is dened. Then, ve instances of this clock type are built. Fig. 6 shows the nal result. Secondly, the ve clocks must be associated with the activity, which is done by applying the stereotype TimedProcessing. As shown in Fig. 5, this stereotype is applied to the whole activity but also to the actions.

In our case, each action is associated with a dierent clock. In aadl, the same association is done when binding a subprogram to a task.

Application

Five aperiodic tasks

The ve clocks are a priori independent. The required time behavior is dened by applying clock constraints to these ve clocks. The clock constraints to use dier depending on the dispatch protocols of the tasks. Aperiodic tasks start their execution when the data is available on their input port in. This is the case for devices, which are aperiodic. The alternation relation ( ∼ ) can be used to model asynchronous communications. For instance, action Release starts when the data from Step3 is available in d3. t3 is the clock associated with Step3 and da is the clock associated with Release. The asynchronous communication is represented as follows: t3 ∼ da. Note that this is only an abstraction of the behavior where the task durations are neglected. Additionally, we did not enforce a run to completion execution of the whole activity. Therefore, the behavior is pipelined and ds occurs a second time before the rst occurrence of da. This is because the operator ∼ is not transitive. An additional constraint (ds ∼ da) would be The one applied here is the random policy that relies on a pseudorandom number generator. Consequently, the result is not deterministic, but the same simulation can be replayed by restoring the generator seed.

Mixing periodic and aperiodic tasks

Logical clocks are innite sets of instants but we do not assume any periodicity, i.e., the distance between successive instants is not relevant. The clock constraint isPeriodicOn allows the creation of a periodic clock from another one. This is a more general notion of periodicity than the general acceptation. A clock c1 is said to be periodic on another clock c2 with period P if c1 ticks every P th ticks of c2. In ccsl, this is expressed as follows:

c1 isPeriodicOn c2 period P offset δ.

To build a periodic clock with the usual meaning, the base clock must refer to the physical time, i.e., it must be a chronometric clock. As in Section 4, we can discretize idealClk for that purpose and build c 100 , a 100 Hz clock (Eq. 7).

c 100 = idealClk discretizedBy 0.01

Figure 8 illustrates an execution of the same application when the threads t1 and t3 are periodic. t1 and t3 are harmonic and t3 is twice as slow as t1. Coincidence instant relations imposed by the specication are shown with vertical edges with a diamond on one end. Depending on the simulation policy there may also be some opportunistic coincidences. Clock ds is not shown at all in this gure since it is completely independent from other clocks.

Note that, the rst execution of t3 is synchronous with the rst execution of t1 even before the rst execution of t2. Hence, the task Step3 has no data to consume. This is compatible with the uml semantics only when using data stores. The data stores are non-depleting so if we assume an initialization step to put one data in each data store, the data store can be read several times without any other writing. The execution is allowed, but the result may be dicult to anticipate and the same data will be read several times. When the task t1 is slower than t3, i.e., when oversampling, some data may be lost.

The complete ccsl specication for this conguration is available in another work [START_REF] Mallet | MARTE vs. AADL for Discrete-Event and Discrete-Time Domains[END_REF].

To interpret the result of the simulation, the timesquare VCD viewer annotates the VCD with additional information derived from the ccsl specication. We have already discussed the instant relations (dashed arrows and vertical edges). Fig. 8 also exhibits the ghost-tick feature. Ghosts may be hidden or shown at will and represent instants when the clock was enabled but not red. Having a close look at clock da, we can see that its rst occurrence is opportunistically coincident with the rst occurrence of t2. However, the second occurrences of the two clocks are not coincident. A ghost is displayed (at time 60) to show that both were enabled, but t2 was red alone, da was actually red at the next step. In that particular example, which is not the rule, the contrary could have been true also. Additionally, that specication is conict-free but it may happen that the ring of one clock disables others. These are classical problems, occurring when modeling with Petri nets, that appear with ccsl because we have dened precedence instant relations in addition to coincidence relations.

MARTE and SDF

This third and last example considers a purely logical case and builds a ccsl library for dening Synchronous Data Flow (sdf) [START_REF] Lee | Static scheduling of synchronous data ow programs for digital signal processing[END_REF] graphs. Subsection 6.1 recalls basics on Synchronous Data Flow (sdf) (syntax and execution rules). Section 6.2 proposes a modular ccsl specication to describe the behavioral semantics of this mocc. Finally, an example SDF graph is built using our library. The semantics is given with ccsl and the syntax is built by a uml model with Papyrus. We apply the very same semantic model to two dierent uml diagrams. The rst target is a uml activity, a popular notation to rep-resent data ows. The second target is a uml state machine, whose concrete syntax is close to the usual representation of sdf graphs.

Synchronous Data Flow

Data Flow graphs are directed graphs where each node represents a function or a computation and each arc represents a data path. sdf is a special case of data ow in which the number of data samples produced and consumed by each node is specied a priori. This simple formalism is well suited for expressing multi-rate DSP algorithms that deal with continuous streams of data. This is a restriction of Kahn process networks [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] to allow static scheduling and ease the parallelization. sdf graphs are essentially equivalent to Computation graphs [START_REF] Karp | Properties of a model for parallel computations: Determinacy, termination, queueing[END_REF] which have been proven to be a special case of conict-free Petri nets [START_REF] Petri | Concurrency theory[END_REF].

In sdf graphs, nodes (called actors) represent operations. Arcs carry tokens, which represent data values (of any data type) stored in a rst-in rstout queue. Actors have inputs and outputs. Each input (resp. output) has a weight that represents the number of tokens consumed (resp. produced) when the actor executes. sdf graphs obey the following rules:

An actor is enabled for execution when all inputs are enabled. An input is enabled when enough tokens are available on the incoming arc. Delay is a property of an arc. A delay of n samples means that n tokens are initially in the queue of the arc.

A CCSL library for SDF

With sdf graphs a local observation is enough to know the dependency on a given element. So it is possible to construct locally a set of ccsl constraints for each model element. This section describes the library of ccsl relations built for this purpose.

As illustrated in previous examples, the rst stage is to identify which ccsl clocks must be dened to create a time system conforming to the sdf semantics. For each actor A, one ccsl clock A is created. The instants of this clock represent the atomic execution instants of the operation related to the actor. For each arc T , two ccsl clocks write and read are created. Clock write ticks whenever a token is written into the arc queue. Clock read ticks whenever a token is read (and removed) from the queue. Note that, the actual number of available tokens is not directly represented and must be computed, if required, from the dierence in the number of read and write operations.

No specic clocks are created for inputs and outputs.

The second stage is to apply the right ccsl clock constraints so that the result of the clock calculus can be interpreted to apprehend the behavioral semantics of the SDF graph.

Actors

do not require any specic constraint.

Tokens are written into and read from the arc queues. A token cannot be read before having been written, hence, for a given arc, the i th tick of write must strictly precede the i th tick of read.

Here again, the packet-based precedence can be built with the ltering operator (Eq. 10). When weight = 1, it reduces to read ≺ actor.

read ▼ 0 weight-1 .1 ω ≺ actor

Arcs can globally be seen as a conjunction of one output, one token and one input.

The library relation denition arc (Eq. 12) species a complete set of constraints for an arc with a delay delay, from an actor source, with an output weight out to another actor target, with an input weight in.

| token(write, read, delay)

| input(target, read, in)

Applying the SDF semantics

The previous subsection denes, for each sdf model element, the ccsl clocks that must be created and the clock constraints to apply. This section illustrates the use of our ccsl library for sdf. Our purpose is to explicitly add to an existing model the sdf semantics. In this example, we use uml activities (Fig. 9.a) and state machines (Fig. By instantiating elements of our ccsl library for sdf, these two models can be given the execution semantics as classically understood for sdf graphs.

The idea is to add the semantics within the model explicitly without being implicitly bound to some external description. In our case, the semantics is given by the ccsl specication and by explicit associations between ccsl clocks and model elements.

When using the syntax of activities, ccsl clocks that represent actors are associated with actions and ccsl clocks that represent readings from (resp. Eq. 13 uses our library to give to the models on parts (a) and (c) the same semantics as understood when considering the sdf graph in the middle part (b). Clocks are named after the model elements with which they are associated, i.e., the clock for actor A is named A. However, this rule is for clarity only and the actual association is done explicitly in the ccsl model. The uml prole for marte extends the uml to model real-time and embedded systems, at the appropriate level of description. However, the real-time and embedded domain is vast and lots of eorts have already been done to provide dedicated proprietary uml extensions [START_REF] Douglass | Real-time UML[END_REF][START_REF] Graf | OMEGA: correct development of real time and embedded systems[END_REF][START_REF] Selic | The emerging real-time UML standard[END_REF]. marte clearly does not cover the whole domain and should be rened to tackle specic aspects, and provide a larger support for analysis and synthesis tools. Our contribution is to illustrate the use of logical time for system specication. This is done by using the marte time subprole conjointly with ccsl. Logical time is thus an integral part of the functional design that can be exploited by compilation/synthesis tools, not restricting time to annotations for performance evaluation or simulation.

At the same time, there is a large demand for standards because the community, tool vendors and manufacturers, wants to rely on industry-proven, perennial languages. Many specications in various subdomains are issued by various organizations to answer this demand (aadl, autosar, east-adl, ip-xact . . . ), even though these subdomains have covered for a long time separate markets and were addressed by dierent communities. With the emergence of large systems, systems of systems, we need to combine several aspects of these subdomains into a common modeling environment. The automotive and avionic industries, which were using dedicated processors are now integrating generic processors and need interoperability between their own models and models used by electronic circuits manufacturers. Therefore, we need formalisms able to compose these models both syntactically and semantically.

Having a common semantic framework is required to ensure interoperability of tools. By selecting several examples from some of these subdomains, we have shown that marte time prole and ccsl can be used to tackle dierent aspects of some of these emerging specications. We advocate that the composed model must provide structural composition rules but also a description of the intent semantics, so that some analysis can be done at the model level.

Then, this model can serve as a golden specication for equivalence comparison with other formal models suitable to apply specic analysis or synthesis techniques.

  and Exclusion (# ≜ ≺ ∪ ≻). The precedence relation represents causal dependency. The coincidence relation is a strong relation that forces simultaneous occurrences of instants from dierent clocks.

  binary words have already been successfully applied to N-Synchronous Kahn networks [3]. Clock constraints A ccsl specication consists of a set of Clocks and a conjunction of clock constraints. A clock constraint is a clock relation between two clocks or clock expressions. The stereotype ClockConstraint has Boolean meta-attributes (isCoincidenceBased and isPrecedenceBased) that indicate the kind of constraint. The coincidence-based constraints are also known as synchronous constraints, whereas the precedence-based constraints are called asynchronous.

  As a very simple example, we dene a ternary coincidence relation, denoted ≡ . The user-dened relation has three clock parameters (v1, v2 and v3). This denition contains two instances of the equality relation whose denition is given in the kernel library. The textual specication of the ternary coincidence relation as follows:

3. 2

 2 TimeSquare timesquare is a software environment dedicated to the resolution of ccsl constraints and computation of partial solutions. It has four main features: 1) definition/modeling of ccsl user-dened libraries that encapsulate the moccs, 2) specication/modeling of a ccsl model and its application to a specic uml-based or dsl model, 3) simulation of moccs and generation of a corresponding trace model, 4) based on a trace model, displaying and exploring the augmented timing diagram, animating uml-based model and storing the scheduling result in the model and sequence diagrams.

Fig. 1 .

 1 Fig. 1. Timing model of the ABS

Fig. 2 .

 2 Fig. 2. Example of the ABS

  r , o rl , o rr ); clock o sup = sup(o f l , o f r , o rl , o rr ); inf (a, b) denes the greatest lower bound of a and b for the precedence relation ≼ and sup(a, b) is the lowest upper bound. With these four new clocks,

Fig. 3 .

 3 Fig. 3. The east-adl specication of the ABS executed with timesquare

Fig. 4 .

 4 Fig. 4. The example in aadl.

Fig. 5 .

 5 Fig. 5. End to end ow with UML and MARTE.

Fig. 6 .

 6 Fig. 6. One logical clock for each aadl task.

Fig. 7

 7 represents the execution proposed by timesquare with only aperiodic tasks with the following constraints: ds ∼ t1, t1 ∼ t2, t2 ∼ t3, t3 ∼ da. The optional dashed arrows represent instant precedence relations induced by the applied clock constraints.

Fig. 7 .

 7 Fig. 7. Five aperiodic tasks.

Fig. 8 .

 8 Fig. 8. Mixing periodic and aperiodic tasks.

  Enough tokens means equal to or greater than the input weight. Actors with no inputs (Source actors) are always enabled. Enabling and execution never depend on the token values, i.e., the control is data-independent. When an actor executes, it always produces and consumes the same xed amount of tokens, in an atomic way. It produces on each output exactly the number of tokens specied by the output weight; these tokens are written into the queue of the outgoing arc. It consumes on each input exactly the number of tokens specied by the input weight, these tokens are read (and removed) from the queue of the incoming arc.

  the relation denition output, which has three parameters. The clock actor represents the actor with which the output is associated. The clock write represents the writing of tokens to the outgoing arc. The strictly positive integer weight represents the output weight. ccsl operator lteredBy is used (Eq. 11). When weight = 1, Eq. 11 simplies into actor = write. def output(clock actor, clock write, int weight) ≜ actor = write ▼ 1.0 weight-1 ω

Fig. 9 .

 9 Fig. 9. An example of SDF graph

  writings to) the arc queues are associated with input (resp. output) pins. All other ccsl clocks are left unbound and are just used as local clocks with no direct interpretation on the model. When using the syntax of state machines, only ccsl clocks that represent actors are bound to the states and other clocks are left unbound.

S

  Fig. 10 shows one possible execution of this specication produced by timesquare. Intermediate clocks are hidden and only actors are displayed. The relative execution of the actors is what matters when considering SDF graphs.

Fig. 10 .

 10 Fig. 10. A simulation output with TimeSquare

  All these parameters are modeled by timing requirements characterized by timing values or time intervals with jitters.

			H k-1			H k
	Lsk-1	Jiik-1	Liok-1	Jook-1	Lsk	Jiik	Liok	Jook
			ABS				ABS
	R k-1				R k
	H : Sampling Interval		Jii : Input Synchronization
	Ls : Sampling Latency		Joo : Output Synchronization
	Lio : Input-Output Latency	R : Trigger

  We build a ccsl relation denition called repetitionRate that has three parameters: element, rate and jitter. element is the clock that must be given a repetition rate. rate is an integer, the actual repetition rate. jitter is a real number, the jitter with which the repetition rate is expressed.

	Repetition rate
	A RepetitionRate concerns successive occurrences of the same event (data ar-
	riving to or departing from a port, triggering of a function). In all cases, it
	consists in giving a nominal duration between two successive occurrences/in-
	stants of the same event/clock.

def repetitionRate(clock element, int rate, real jitter) ≜ clock c 1 = idealClk discretizedBy 0.001

  The kernel ccsl relation strict precedence models such a constraint: write ≺ read. When delay > 0, delay tokens are initially available in the queue, which means that the i th read operation gets the data written at the (i -delay) th write operation, for i > delay. input, has three parameters. The clock actor represents the actor with which the input is associated. The clock read represents the reading of tokens on the incoming arc. The strictly positive integer weight represents the input

	(8)
	Inputs
	require a packet-based precedence (keyword by in Eq. 9). A relation denition,
	weight.
	def input(clock actor, clock read, int weight) ≜
	(read by weight) ≺ actor

The delay previous read operations actually get tokens initially available and that do not match an actual write operation. ccsl operator delayedFor can represent such a delay (Eq. 8). To represent sdf arcs, we propose to create in a library, a new relation denition, called token. Such a relation has three parameters: two clocks (write and read) and an integer (delay). The token relation applies the adequate constraint (Eq. 8). Note that, when delay = 0, Eq. 8 reduces to write ≺ read.

def token(clock write, clock read, int delay) ≜ write ≺ (read delayedFor delay) called

  In that case, ccsl clocks write and read are local clocks.

def arc(int delay, clock source, int out, clock target, int in) ≜ clock read, write output(source, write, out)

http://www.autosar.org