UML MARTE Time Model and Its Clock Constraint Specification Language

UML MARTE Time Model and Its Clock Constraint Specification Language

Frédéric Mallet (Université Nice Sophia Antipolis, I3S, UMR 7271, CNRS, INRIA, 06900 Sophia Antipolis, France), Marie-Agnès Peraldi-Frati (Université Nice Sophia Antipolis, I3S, UMR 7271, CNRS, INRIA, 06900 Sophia Antipolis, France), Julien Deantoni (Université Nice Sophia Antipolis, I3S, UMR 7271, CNRS, INRIA, 06900 Sophia Antipolis, France) and Robert de Simone (INRIA Sophia Antipolis Méditerranée, 06900 Sophia Antipolis, France)
Copyright: © 2014 |Pages: 23
DOI: 10.4018/978-1-4666-6194-3.ch002


The UML Profile for MARTE extends the UML with constructs dedicated to the modeling and analysis of real-time and embedded systems. Its time profile provides a rich model of time based on the notion of logical clocks that can be used consistently through all modeling elements/diagrams. The MARTE time profile comes with a companion language, called CCSL. CCSL is a formal declarative language used to handle the MARTE logical clocks and schedule the execution of the different parts of a model. This chapter gives a snapshot on modeling and analysis facilities that have been developed specifically around the time profile of MARTE and CCSL. A second objective is to show how MARTE can be combined with other profiles such as EAST-ADL. The last objective is the use of CCSL as a common language for specifying the semantics of models to allow their execution in a common framework. The MARTE and EAST-ADL constructs are illustrated on an example of a simplified cruise control. The example starts with a description of functional and timing requirements captured using a specific profile called EAST-ADL dedicated to the automotive domain. Then some of the requirements are refined with UML state machines and activities adorned with MARTE stereotypes. All these models rely on MARTE clocks. The semantics of these diagrams is given by a CCSL description that is automatically derived from the models. The resulting CCSL specification can be used to execute the UML/EAST-ADL specification, to animate the model, or to perform various kinds of analyses.
Chapter Preview


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.

Key Terms in this Chapter

CCSL: Clock Constraint Specification Language, a companion language defined as an annex of MARTE.

CTL: Computation Tree Logic, a branching time temporal logic.

OMG: The Object Management Group.

OCL: The Object Constraint Language, an OMG specification.

UML: The Unified Modeling Language, an OMG specification.

MARTE: Modeling and Analysis of Real-Time and Embedded systems, an OMG UML Profile.

SysML: The System engineering Modeling Language, an OMG UML Profile.

Cc: Cruise Control, the running example used in this chapter.

TADL: Timing Augmented Description Language.

ECL: Event Constraint Language, an OCL extension with events and synchronization constraints.

EAST-ADL: A domain-specific language defined by a succession of European projects and dedicated to the design of automotive systems.

Complete Chapter List

Search this Book: