UML MARTE Time Model and Its Clock Constraint Specification Language

Introduction

The Unified Modeling Language (UML) (OMG, 2009b), and its SysML profile/variant have originally been conceived by recognizing and adopting common modeling concepts frequently used in practice for design: Components/structured classes for structural description, behavioral models for concurrent hierarchical finite state-machines, dataflow streaming diagrams, sequence and timing diagrams are well-known examples. Variants of such models were widely used in various forms before the advent of UML/SysML, which have then captured them as modeling artifacts. Still, despite their overall familiar look, most of these diagrams adopt distinct or unclear interpretations in their various forms, very often for good reasons (and some time for no reasons at all). This may lead to an incorrect or a context-dependent interpretation of a model and the impossibility to perform a strict verification. This point is a limitation for using plain UML in the domain of real-time and embedded systems. An even more important problem, in the case of real-time embedded systems, is the non-functional performance aspects. It soon appeared that extra specific annotations were needed to express the timing properties and constraints in a formal way, with appropriate syntax and expressivity. Time constraints could be used to define the precise timely semantics of a given profiled model, or the general description of a scheduling requirement setting, or the intrinsic time features of a given individual model.

MARTE 0, the dedicated UML profile for Modeling and Analysis of Real-Time Embedded systems and its Time Model (André et al., 2007) were specifically defined to serve this goal. They provide extensions for dealing with a multiform notion of Time, where local Logical Clocks may be completely, partially, or not inter-related at all. The central concern of scheduling can be then seen as the means to organize the ticks of these various clocks (of time threads) so as to respect provided constraints. This view (harmonizing local times provided by design into a consistent global solution) is strongly indebted to the theory of synchronous/polychronous languages (Benveniste et al., 2003)0, and of Tag Systems (Edward & Sangiovanni-Vincentelli, 1998).

MARTE 0 provides also as an annex a candidate language for expressing the relevant constraints, called the Clock Constraint Specification Language (CCSL) (André, 2009). In a collection of articles (Goknil et al., 2013a) we have shown in the past how the CCSL language could represent many distinctive patterns used for the definition of timed semantics of domain-specific Architecture Description Languages (e.g., AADL or EAST-ADL) (Peraldi-Frati et al., 2012), or for prominent scheduling policies, or again for Timed Processes formal analysis tools (such as UppAal for Timed Automata) (Goknil et al., 2013b). We address here an example to show how the different pieces can be put together and how the logical clocks are used to bring consistency between the different parts of the models, captured with different complementary formalisms.