Real-Time Model-Driven Engineering: An Overview

Abstract

After a maturing period of over a decade, Model-Driven Engineering (Mde) starts to extend to novel areas that include safetycritical or embedded, but also cyberphysical systems. These domains explicitly manipulate time. This paper proposes three dimensions to analyse how Mde frameworks integrate time: which transformation paradigm is used, how time is represented inside it, and which characteristics of time are considered. Without claiming for exhaustivity, we validate our approach by analysis several contributions from the literature, thus offering an overview of the current practice in Real-Time Mde.

Introduction

After a maturing period of over a decade, Model-Driven Engineering (Mde) has gained enough maturity to extend to novel areas that include safety-critical or embedded, but also cyber-physical systems. These domains make an explicit use of time, forcing language and Mde frameworks to progressively integrate time features to allow the speci cation of durations, deadlines, delays, etc. Simply borrowing low-level constructs from General-Purpose Programming Languages (Gpls) is not an option any more: this introduces a gap between the highlevel concepts captured by models, and the low-level constructs available for expressing time-related computations that become di cult to properly align. Time is not directly accessible to computer: integrating it into Mde frameworks requires to think about which aspects need to be explicitly represented and which could safely be forgotten.

However, one time model could not possibly satisfy all possible needs in Mde. As a rst attempt to properly classify Real-Time Mde approaches, this paper proposes a preliminary classi cation of some of the relevant dimensions, and confronts it against a panel of selected contributions from the literature, thus o ering an overview of the current theoretical foundations and practice in the domain. Section 2 explains the classi cation criteria, and Sections 3 and 4 overview literature contributions based on Meta-Programmed (Mpt) and Graph-Based Transformation (Gbt) Languages respectively. Section 5 concludes with a summary table relating the analysed contributions to the classi cation criteria.

Model Transformation, Time and Time Representation

This Section explores background material for Model Transformations and Time characteristics and representation to build an analysis grid for classifying the literature contributions (cf. Figure 1, Left). 2.1

Model Transformation: Paradigms and Units

Model Transformation (Mt) can be roughly categorised according to their underlying paradigm: operational or meta-programmed transformations (Mpt), adapting constructions from imperative Gpls to model-speci c constructions; and declarative, relying on rewriting techniques specifying graph-based transformations (Gbt) (as a rst approximation, see [ 1 ] for details). Two elements compose any Tl: transformation units that bring basic computational bricks expressing a meaningful, well-de ned model alteration; and scheduling mechanisms orchestrate these units in a more or less explicit fashion. For Mpts, statements constitute the units that are modularly organised into operations, and scheduled implicitly through the statement- and operation call-control ow de ned by the Tl. Rewriting rules are the basic units for Gbts, and are typically organised in layers, or prioritised; di erent scheduling mechanisms are possible, ranging from prede ned to explicit scheduling Dsls. Time information can appear directly attached to the model, integrated into the transformation units, or as part of the scheduling mechanism. 2.2

Time: Characteristics and Representation

Classical distinctions for real-time systems, such as the di erence between hard, soft and even rm real-time (indicating how often and critical deadlines might be missed), or the distinction between physical and logical time, are not discriminating enough: many systems fall in one or the other depending on the considered viewpoint. This Section attempts to provide a clearer description of the many dimensions of time, by retaining those aspects from Furia, Mandrioli, Morzenti and Rossi' contribution [ 16 ] that seems interesting for providing precise classi cation criteria. 2.2.1 Characteristics When abstracted for being represented within computers, time is interpreted over a speci c domain, and manipulated through a language that possesses speci c features: all these characteristics determine how one can reason on a real-time system. The Feature Diagram on the right of Figure 1 summarises these characteristics.

Domain The semantic domain for time consists of a mathematical, numerical set whose intrinsic properties in uences the way time can be manipulated by modellers through their language, and the scope of properties they can express. A dense set like the rational Q or real R numbers allows to nd (time) points between any arbitrary pair of points: these sets are perfect for representing \reallife" processes or phenomena in biology, chemistry, physics, etc. On the contrary, a discrete set like the integers (N or Z), allows to specify clock ticks, representing abstractions from the real phenomenon. By using sampling techniques, a dense set can be discretised. A hybrid domain makes use of both discrete and continuous time (for di erent parts in the system). Note that in [ 16 ] also appears the notion of boundedness: this mostly in uences the veri cation process; besides, none of the overviewed contributions explicitly mentions boundaries. Language Modellers manipulate the time domain only through their modelling language: it possess a structure, exposes a determinism model, and allows the speci cation of a range of properties following a speci c type.

Structure The states de ned by a timed language can be classi ed into two categories: linear formalisms arrange their states into a sequence, implying that state evolution is uniquely determined by the previous state; while branching languages organise states as trees where several possible future states may exist concurrently. Determinism A deterministic reactive system can be seen as a system that provides a unique response to an external stimulus in a given state. In several cases however, non-determinism is a powerful abstraction for hiding implementation details, or possible choices on the future states have no obvious reasons (e.g., at design time, it is not relevant to force one task over another), or when the environment (that may produce these inputs) is unsu ciently known (e.g., the chain reaction of a power plant). Stochastic systems bring another precision by associating a probability distribution for specifying undeterministic choices.

Property Type Some languages allow purely qualitative constraints, by specifying the relative ordering of some relevant events (e.g., car breaks should activate only after pedal is pushed), without specifying which time actually separate both events; whereas quantitative constraints enable a more precise speci cation (e.g., breaks should activate before 50 ms after pedal push).

Features From a time perspective, it is often practical to specify a system through its components. The language's features are the mechanisms available for specifying synchronicity and communication between these components. Synchronicity The synchronicity determines how di erent subsystems, or modules, are paced regarding their relative execution: synchronous systems impose changes in modules to occur at the same time, or at times rigidly related; while asynchronous systems allow independent progress for each module.

Communication For asynchronous systems (although this theoretically also applies to synchronous ones), a form of communication is needed between modules. Two classical ways are usually used: message passing, where communication is achieved by exchanging messages through communication channels; or resource sharing, where communication relies on a common resource, usually memory, used to pass information.

Several contributions, especially those targeting heterogeneous systems, actually mix these features together to obtain richer speci cation, at the expense of complicating the coordination between system modules or languages. 2.2.2 Representation Independently of the time characteristics, what really matters for the modeller is how time is accessible i.e. which Mde elements time information is attached to. We reuse the proposal of [ 10 ] as a generalised way of representing time information for all Mde framework (i.e. beyond Gbt only). Time as Data (TaD) , where time information resides inside the model itself, e.g.

by integrating clock counters or timers as attributes within speci c classes. Time as Control (TaC) where time information is integrated at the level of transformations, either by integrating it explicitly in the Tl, or by extending existing Tls with speci c constructions.

Time as Embedding (TaE) where time is not explicitly integrated at the modelling level, but rather implicitly present in an external, third-party language: the Tl only o ers an implicit represention of time, that only becomes explicit when the whole speci cation, model(s) + transformation(s), are translated into that external language.

Conceptually however, nothing prevents to mix these representation styles in various ways: indeed, many contributions borrows from two or even three of them. This classi cation nevertheless provides a good hint on the level of control each contribution o ers to modellers, and the following sections classi es the selected contributions by their most prominent approach. 3

Metaprogrammed Transformation Languages

In Uml, several diagrams already possess the capability to express time, but at various abstraction levels and in di erent avours that are hard to reconcile (cf. Douglass' book for a broad introduction of how time can be handled in the various Uml diagrams [ 14 ]). Two diagrams attracted the most attention: State Machines (or Statecharts) and Activity Diagrams. In parallel, a recent trend tends to separate the domain concepts, as captured by classical Mde artefacts, from the actual model of computation (MoC): this avoids overloading the model with details pertaining only to the computation; and allows to reason more precisely on the time features.

UML-Based Approaches Because of the many existing variants for Statecharts (von der Beeck mentions 21 variants in [ 42 ]), researchers focused on providing a clean semantics of a speci c variant [ 24,43,9 ], while others contributed with a uni ed semantic framework integrating several variants ([ 3,29,26 ] among others) for reconciling model execution and veri cation. In parallel, several extensions were explored to overcome existing limitations and addressing variation points: Liu et al. proposed a way to integrate explicit communication [ 25 ], extending the Uml time mechanism that prescribes time values to be solely attached to events; Shankar and Asa integrated time features in a way independent from the underlying diagrams used for model speci cation [ 37 ].

Activity Diagrams serve as a theoretical modelling basis in the Foundational Subset for Executable UML (f Uml) [ 30 ]. Again, a number of work aimed at clarifying fUml's semantics [ 23,34 ]. f Uml has been integrated into Mof to operate as a fully- edged Tl, resulting in the xMof framework [ 28 ], served as a semantics speci cation for Uml Pro les in [ 41 ], and was leveraged for specifying real-time systems based on f Uml concurrency, synchronicity and scheduling model [ 4 ].

The Marte Pro le [ 31 ] explicitly integrates a multiform notion of time. It can be physical, i.e., continuous or discrete; or logical, i.e. speci ed through events and clocks whose precise relationships are constrained by means of operators de ned in the Ccsl (Clock Constraint Speci cation) Language. No assumption is made a priori about the clocks' relative progression or pace. Ccsl's semantics is di cult to apprehend, but many contributions targeted a full semantics de nition in denotational and operational styles [ 2,45,12,44 ]). Ccsl has its own simulation tool, TimeSquare [ 13 ], which was used by Boulanger, Dogui et al. in [ 7 ] to de ne semantic adaptations between di erent models of computation.

HybridUml [ 5 ] is an Uml Pro le aiming at easing the description of hybrid systems (i.e. systems mixing both discrete and continuous time): it de nes new data types for handling both discrete and continuous time domains, and allows to describe systems through agents whose behaviour is speci ed with hybrid automata that communicate through shared variables.

Separating the MoC from the Model Formal System Design (ForSyDe) (cf. [ 35,36 ], and the website https://forsyde.ict.kth.se/) proposes a methodology for modelling and designing heterogeneous embedded and cyberphysical systems. ForSyDe focuses on semantic-preserving re nement into executable, low-level implementations obtained from high-level models. The re nement proceeds through controlled transformations, either by re ning the design, i.e. the system architecture, by introducing further details; or by preserving the model semantics, by integrating computational details. The methodology enforces determinism in order to perform the proofs guiding the transformation process. The MoC allows either synchronous or asynchronous behaviour. ForSyDe was combined with Uml in [ 21 ] through the CoMeta methodology [ 22 ] to ensure that the intended behaviour of a system is preserved, whatever tool is used to simulate it.

ModHel'X (cf. [ 18,19 ] and the website http://wwwdi.supelec.fr/software/ ModHelX) and GeMoC ([ 8 ], cf. the website for further information: http:// gemoc.org/) are the more advanced frameworks for executing heterogeneous models based on di erent Models of Computation (MoC). A ModHel'X specication consists of blocks, each with its own MoC, that communicate through well-speci ed interafaces called pins. The interaction between blocks is handled at the level of interface through adaptors: data is translated back and forth from the outside into the block's computation in a user-de ned way. Time constraints imposed by each block propagate through the hierarchical blocks organisation, and may be synchronised through interaction patterns.

GeMoC is more exible, because many dedicated Dsls allow to ne-tune each aspects of the overall infrastructure: the interaction between the MoC and the internal computation aimed at modifying the model's structure; but also the coordination between heterogeneous models obeying di erent MoC. However, from an abstract viewpoint, the time model relies on Ccsl to specify clock relationships, and on events (corresponding to speci c clock ticks) triggering internal model changes. GeMoC is di cult to classify, due to the expressive power of the many Dsls composing its core. By using Ccsl, the time domain is clearly heterogeneous, but only qualitative properties can be expressed. Since the communication is also explicitly modelled, both synchronous and asynchronous features can be used, through any of the communication features available. 4

Graph-Based Transformation Languages

Fundamentally, Gbt shares with Petri Nets the same algebraic foundations [ 27 ]: this provided a good starting point for integrating time into various Gbt formalisms, including the possibility to de ne stochastic transformations. Rewriting logics over algebraic speci cations, although similar to Petri Nets, is another distinct source for specifying time within Gbt.

Petri Nets-based Approaches Gyapay, Varro and Heckel [ 17 ] followed an existing approach for Environment-Relationship High-Level Petri Nets to integrate time into double pushout typed Gbt: they introduce dedicated attributes attached to graph vertices to keep track of time elapse; these attributes are updated along the transformation whenever rules are applied. This approach is designed as a quantitative time proposal naturally bound to Gbt: it allows to overcome the existing limitations for modelling time, while fully reusing existing tools and technologies for Gbt, assuming graphs are modelled from the beginning with time attributes.

Stochastic Gbts were explored by Heckel and his colleagues in [ 20 ]: transitions of a Petri Net-like formalism are triggered according to a probability distribution instead of a discrete boolean guard, introducing delays in Gbt rules execution. This approach was later enriched with localised events that are ordered through a graph hierarchy, allowing to specify probabilistic dependencies among events residing at di erent levels. Both contributions target stochastic simulation, although some analysis based on Prism remains possible.

De Lara and Vangheluwe [ 11 ] enrich Gbt prioritised rules with time intervals to model imprecise clocks and timeouts, allowing to delay rules execution to a future time speci ed by the interval. Rules then represent time elapse of domain-speci c actions attached to rules. Again, simulation and analysis are possible through a mapping into Petri Nets, with the results translated back to the original domain-speci c concepts.

Rewriting Logics Maude is the common external Gpl for Rewriting Logics, thus allowing simulation, reachability analysis and model-checking. Boronat and O lveczky [ 6 ] extended the Moment Framework with Real-Time capabilities by adding timers, clocks and timed values (corresponding to a rated basic clock) to Mof-compliant models. To avoid cluttering Mof-conformant models with time features, they use a kind of \dependency injection", so that model elements concerned with time are referenced by the classes embedding the time information. This approach is a hybrid between TaE/TaD: time information inside the model still has to be explicitly managed by transformations.

The e-Motions framework [ 33,32 ] is a visual framework for the modelling, animation and analysis of Real-Time Domain-Speci c Languages that provides a large variety of time constructs attached to rules (and therefore, considered as TaC). These constructs de ne domain-speci c actions: rules can be ongoing, meaning that they are constantly updating the model; or atomic with a duration and a period. Such a rich Tl requires a careful translation into Maude: atomic rules are translated into two rules, one when a match is found and the other for triggering the model changes; and ongoing rules are managed with low-level primitives in Real-Time Maude.

Other Approaches For the purpose of animating Dsls in (quantitative) realtime even when the model at hand presents several concurrent changes, Strobl and Minas propose another approach based on a Dsl aiming at facilitating the speci cation of animations [ 38 ], whose semantics is speci ed as Gbt. For obtaining a reactive system, time information is attached to states, and transitions are triggered by di erent kinds of events: internal events represent time elapse, making the global time progress; and external events represent user interaction. Events are organised in a queue: the next internal event is computed between all possible events in the graph, while taking into account possible external events that must have priority.

MechatronicUml [ 15 ] is a tool suite designed for the modelling and formal analysis of cyber-physical systems using time-dependent dynamic structures that need to be recon gured architecturally at runtime. Their modelling approach relies on components, whose internal behaviour is speci ed as real-time statecharts, and on patterns that specify how components communicate without breaking their internal logics. Gbt rules specify how the components and their communication ports and channels constituting the overall system architecture, are recon gured in response to stimuli. The clocks de ned in statecharts are accessible to the Gbt rules to guard an execution, add, remove or reset clock instances dynamically. By translating the statecharts and the Gbt rules as a Uppaal speci cation, they are able to perform model-checking.

AtomPm [ 40 ] is a web-based Mde framework relying on a mapping into Devs [ 39 ]: the transformation designer manipulate time directly, but the framework o ers concurrency primitives through a dedicated visual language, forcing the designer to handle classical concurrency issues by himself.

Contribution Statecharts Activity Diags./fUml Marte / Ccsl ptHybridUml MForSyDe ModHel'X GeMoC

Domain Language Features Representation

D B/D A/MP TaC D B/D A/MP TaC H B/D H/? TaD+TaC H B/D A/RS TaD+TaC H B/D A/RS TaC H B/D H/MP TaC

H B/D H/? TaC

5 Conclusion

Real-Time Mde is a recent application of Mde techniques and know-hows to new application domains such as embedded, safety-critical and cyber-physical systems for which time is a crucial components. We proposed in this paper a preliminary classi cation based on three criteria: the transformation language's paradigm (either Mpt or Gbt); the components characterising the time information available for the modeller; and the way time is represented in the Mde framework. We then overviewed several literature contributions: without aiming at full exhaustivity, the surveyed approaches are in our opinion representative enough for depicting the general picture of the current practice and the recent theoretical developments. Table 1 summarises the results by classifying each (group of) contributions according to our criteria.

We plan to pursue this e ort in three directions. First, we plan to collect more contributions than what was possible with this paper's space restriction. Second, we wish to re ne our criteria, in particular the Representation: this granularity is not enough to capture adequately the many variations encountered in approaches that handle coordination between models expressed with di erent MoCs, since this task is complex and happens at di erent levels. Third, we aim at studying the V&V capabilities of these contributions: functional as well as temporal correctness are crucial features for real-time applications. Acknowledgments. The authors would like to thank Hans Vangheluwe for pointing us to Furia, Mandrioli, Morzenti and Rossi's book, and James Ortiz for interesting discussions on metaprogrammed frameworks. This research was sponsored by a Ceruna scholarship from the University of Namur, Belgium.

References

1. M. Amrani , L. Lucio , G. Selim , B. Combemale , J. Dingel , H. Vangheluwe , Y. Le Traon , and J Cordy . Formal Veri cation Techniques for Model Transformations: A Tridimensional Classi cation . JoT , 2014 .

2. C. Andre . Syntax and Semantics of the Clock Constraint Speci cation Language . Technical report, Inria , 2009 .

3. D. Balasubramanian , C. Pasareanu , M. Whalen , G. Karsai, and M. Lowry . Polyglot: Modeling and Analysis for Multiple Statechart Formalisms . In Issta, 2011 .

4. A. Benyahia , A. Cuccuru , S. Taha , F. Terrier , F. Boulanger , and S. Gerard . Extending the Standard Execution Model of UML for Real-Time Systems . In Dipes, 2010 .

5. K. Berkenkotter, S. Bisanz, U. Hannemann , and J. Peleska . The HybridUML Pro le for UML 2.0 . Sttt , 2006 .

6. A. Boronat and P. Olveczky. Formal Real-Time Model Transformations in Moment2 . In Fase, pages 29 { 43 , 2010 .

7. F. Boulanger , A. Dogui , C. Hardebolle , C. Jacquet , D. Marcadet , and I. Prodan. Semantic Adapatation Using CCSL Clock Constraints . In Mpm Workshop, 2012 .

8. B. Combemale , C. Brun , J. Champeau , X. Cregut , J. Deantoni , and J. Le Noir . A Tool-Supported Approach for Concurrent Execution of Heterogeneous Models . In Erts, 2016 .

9. A. David , M.O. Mo ller, and W. Yi . Formal Veri cation of UML Statecharts with Real-Time Extensions . In Fase, 2002 .

10. J. De Lara , E. Guerra , A. Boronat , R. Heckel , and P. Torrini . Domain-Speci c Discrete Event Modelling and Simulation Using Graph Transformation . SoSyM , 2014 .

11. J. De Lara and H. Vangheluwe . Automating the Transformation-Based Analysis of Visual Languages. Formal Aspects of Computing , 22 ( 3 {4): 297 { 326 , 2010 .

12. J. Deantoni , C. Andre , and R. Gascon. CCSL Denotational Semantics . Technical report, Inria , 2014 .

13. J. Deantoni and F. Mallet . TimeSquare: Treat your Models with Logical Time . In Tools, 2012 .

14. B.P Douglass. Real Time UML : Advances in the UML for Real-Time Systems . Addison Wesley , 2004 .

15. S. Dziwok , C. Gerking , S. Becker , S. Thiele , C. Heinzemann , and U. Pohlmann . A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems . In Fse Symposium , 2014 .

16. C. Furia , D. Mandrioli , A. Morzenti , and M. Rossi . Modeling Time In Computing. Springer-Verlag, 2012 .

17. S. Gyapay , D. Varro , and R. Heckel . Graph Transformation with Time: Causality and Logical Clocks . Fundamenta Informaticae , 58 ( 1 ):1{ 22 , 2003 .

18. C. Hardebolle. Composition de Modeles Pour la Modelisation Multi-Paradigmes. PhD thesis , University of Paris-Sud XI - Orsay, 2008 .

19. C. Hardebolle and F. Boulanger . Multi-Formalism Modelling and Model Execution . Journal of Computers and their Applications , 31 ( 3 ): 193 { 203 , 2009 .

20. R. Heckel , G. Lajios, and S. Menge . Stochastic Graph Transformation Systems. Fundamenta Informaticae , 74 ( 1 ): 63 { 84 , 2006 .

21. P. Issa Diallo , J. Champeau , and L. Lagadec . Enhance the Reusability of Models and Their Behavioural Correctness . In GeMoC, 2013 .

22. P. Issa Diallo , J. Champeau , and V. Leilde . Model-Based Enginnering for the Support of Models of Computations: the CoMeta Approach . In Mpm, 2011 .

23. Q. Lai and A. Carpenter . Static Analysis and Testing of Executable DSL Speci - cation . In Modelsware, 2013 .

24. D. Latella , I. Majzik , and M. Massink . Towards a Formal Operational Semantics of UML Statechart Diagrams . In Fmoods, 1999 .

25. S. Liu, Y. Liu , E. Andre , C. Choppy , J. Sun , B. Wadhwa , and J. Song Dong . A Formal Semantics for Complete UML State Machines with Communications . In iFM, 2013 .

26. A. Maggiolo-Schettini , A. Peron , and S. Tini . A Comparison of Statecharts StepSemantics . Theoretical Computer Science , 2003 .

27. M. Maximova , H. Ehrig , and C. Ermel . Formal Relationship between Petri Net and Graph Transformation Systems Based on Functors between M-Adhesive Categories . In Pn-Gt, volume 40 , pages 23 { 40 , 2010 .

28. T. Mayerhofer. De ning Executable Modeling Languages with fUML . PhD thesis , Technical University of Vienna, 2014 .

29. J. Niu , J.M. Atlee , and N.A. Day . Template Semantics for Model-Based Notations . Transactions on Software Engineering , 29 ( 10 ): 866 { 882 , 2003 .

30. Object Management Group. Semantics of a Foundational Subset for Executable UML Models . Technical report , 2011 .

31. Object Management Group. UML Pro le for MARTE: Modeling and Analysis of Real-Time Embedded Systems . Technical report , 2011 .

32. J.E. Rivera . On the Semantics of Real-Time Domain-Speci c Modeling Languagues . PhD thesis , University of Malaga, 2010 .

33. J.E. Rivera , F. Duran , and A. Vallecillo . Formal Speci cation and Analysis of Domain-Speci c Models Using Maude . Simulation, 85 ( 11 {12), 2009 .

34. A. Romero , K. Schneider , and M.G. Vieira Ferreira . Using the Base Semantics Given by fUML for Veri cation . In Modelsware , 2014 .

35. I. Sander. System Modeling and Design Re nement in ForSyDe . PhD thesis , Royal Institute of Technology (Stockholm), 2003 .

36. I. Sander and A. Jantsch . System Modeling and Transformational Design Re nement in ForSyDe . IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , 23 ( 1 ): 17 { 32 , 2004 .

37. S. Shankar and S. Asa . Formal Semantics of UML with Real-Time Constructs . In Uml, 2003 .

38. T. Strobl and M. Minas . Generating Graph Transformation Rules from AML-GT State Machine Diagrams for Building Animated Model Editors . In Agtive , 2011 .

39. E. Syriani and H. Vangheluwe . De-/Re-Constructing Model Transformation Languages. In Gt-Vmt Workshop , 2010 .

40. E. Syriani, H. Vangheluwe , R. Mannadiar , C. Hansen , S. Van Mierlo , and H. Ergin . AToMPM: A Web-Based Modeling Environment . In Tool Demo Session | MoDELS Conference, 2013 .

41. J. Tatibou et, A. Cuccuru, S. Gerard , and F. Terrier . Formalizing Execution Semantics of UML Pro les with fUML Models . In MoDELS, 2014 .

42. M. von der Beeck. A Comparison of Statecharts Variants. In Formal Techniques in Real-Time and Fault-Tolerant Systems , 1994 .

43. M. von der Beeck. Formalisation of UML Statecharts . In Uml, 2001 .

44. M. Zhang and F. Mallet . An Executable Semantics of CCSL and its Applications . In Ftscs, 2015 .

45. G. Zholtkevych , F. Mallet , I. Zaretska , and G. Zholtkevych . Two Semantic Models for Clock Relations in the Clock Constraint Speci cation Language . In Icteri, 2013 .