MALLET , Frédéric

The Object Management Group (OMG) Unified Modeling Manguage (UML) profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) aims at using the general-purpose modeling language UML in the domain of Real-Time and Embedded (RTE) systems. To achieve this goal, it is absolutely required to introduce inside the mainly untimed UML an...

ccsl has arisen from different inspiring models in an attempt to abstract away the data and the algorithms and to focus on events and control. Even though CCSL was initially defined as the time model of the UML profile for MARTE, it has now become a full-edged domain-specific modeling language for capturing causal, chronological and timed...

Cyber Physical Systems (CPS) combine digital computational systems with surrounding physical processes. Computations are meant to control and monitor the physical environment, which in turn affects the computations. The intrinsic heterogeneity of CPS demands the integration of diverse models to cover the different aspects of systems. The UML...

Logical time is a relaxed form of time promoted by synchronous languages that is functional, elastic (can be abstracted or refined), and multiform. All these properties make logical time adequate also at design time, whereas precise physical time annotations should only matter in later post-synthesis stages. The Clock Constraint Specification...

The UML (Unified Modeling Language) Profile for Modeling and Analysis of Real-Time and Embedded (MARTE) systems promises a general modeling framework to design and analyze embedded systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on verification techniques supported. The Clock Constraint...

CCSL has arisen from different inspiring models in an attempt to abstract away the data and the algorithms and to focus on events and control. Even though CCSL was initially defined as the time model of the UML profile for MARTE, it has now become a full-fledged domain-specific modeling language for capturing causal, chronological and timed...

International audience

This paper overviews the benefits of using logical time in the context of the RT-Simex project. We focus on the use of logical time to, first, graphically specify the functional and extra-functional system requirements; second, to verify that an execution is correct with regards to the requirements. The system requirements are expressed by...

UML goal of being a general-purpose modeling language discards the possibility to adopt too precise and strict a semantics. Users are to refine or define the semantics in their domain specific profiles. In the UML Profile for Modeling and Analysis of Real-Time and Embedded systems, we have defined a broadly expressive Time Model to provide a...

The AFADL days bring together academics and industrial researchers who are interested in the practical use of formal methods at all stages of the development of software or systems. In 2023, the days took place in Rennes from June 5th to June 8th in the same place of the annual days organized by GDR GPL.

Embedded System Design is becoming a field of choice for Model-Driven Engineering techniques. On the engineering side, models bring an abstraction of the code that can then be generated (and regenerated) at will. On the semantic side, they bring a reasoning framework to guarantee or verify properties on the generated code. We focus here on the...

Scheduling is a central yet challenging problem in real-time embedded systems. The Clock Constraint Specification Language (CCSL) provides a formalism to specify logical constraints of events in real-time embedded systems. A prerequisite for the events is that they must be schedulable under constraints. That is, there must be a schedule which...

The UML Profile for Modeling and Analysis of Real-Time and Embedded (RTE) systems has recently been adopted by the OMG. Its Time Model extends the informal and simplistic Simple Time package proposed by UML2 and others a broad range of capabilities required to model RTE systems including both discrete/dense and chronometric/logical time. MARTE...

International audience

Transforming a specification language into a language supported by a verification tool is a widely adopted way of doing formal verification. It enables the reuse of existing languages and tools. In this paper, we propose a correct transformation from CCSL to Promela to do formal verification by SPIN. To implement the transformation, we...

The Clock Constraint Specification Language (\ccsl) has been informally introduced in the specifications of the \uml Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE). In a previous report entitled ''Syntax and Semantics of the Clock Constraint Specification Language'', we equipped a kernel of \ccsl with an operational...

UML goal of being a general-purpose modeling language discards the possibility to adopt too precise and strict a semantics. Users are to refine or define the semantics in their domain specific profiles. In the UML Profile for Modeling and Analysis of Real-Time and Embedded systems, we have defined a broadly expressive Time Model to provide a...

Embedded System Design is becoming a field of choice for Model-Driven Engineering techniques. On the engineering side, models bring an abstraction of the code that can then be generated (and regenerated) at will. On the semantic side, they bring a reasoning framework to guarantee or verify properties on the generated code. We focus here on the...

The Clock Constraint Specification Language (CCSL) has initially been introduced as part of the UML Profile for Marte dedicated to the modeling and analysis of real-time and embedded systems. CCSL proposes a set of simple patterns classically used to specify causal and temporal properties of (UML/EMF) models. The paper proposes a new semantic...

La modélisation des systèmes répartis et des systèmes électroniques modernes nécessite des référentiels temporels multiples. Nous désignons ces systèmes sous le nom de "systèmes polychrones". Le profil UML pour les systèmes temps réel et embarqués (MARTE) permet leur modélisation ainsi que la spécification de contraintes temporelles avec CCSL...

The UML Profile for Modeling and Analysis of Real-Time and Embedded (RTE) systems has recently been adopted by the OMG. Its Time Model extends the informal and simplistic Simple Time package proposed by UML2 and offers a broad range of capabilities required to model RTE systems including both discrete/dense and chronometric/logical time. MARTE...

UML est un langage de modélisation largement utilisé mais qui offre peu de possibilités pour représenter des aspects liés au temps. Le profil UML Marte (Modeling and Analysis of Real-Time and Embedded systems) pallie cette insuffisance. Il offre la possibilité de modéliser du temps physique aussi bien que du temps logique. Un langage de...

Embedded System Design is becoming a field of choice for Model-Driven Engineering techniques. On the engineering side, models bring an abstraction of the code that can then be generated (and regenerated) at will. On the semantic side, they bring a reasoning framework to guarantee or verify properties on the generated code. We focus here on the...

TimeSquare is an Eclipse and model-based environment for the specification, analysis and verification of causal and temporal constraints. It implements the MARTE Time Model and its specification language, the Clock Constraint Specification Language (ccsl). Both MARTE and ccsl heavily reliy on logical time, made popular by its use in distributed...

The UML Profile for Modeling and Analysis of Real-Time and Embedded (RTE) systems has recently been adopted by the OMG. Its Time Model extends the informal and simplistic Simple Time package proposed by UML2 and offers a broad range of capabilities required to model RTE systems including both discrete/dense and chronometric/logical time. MARTE...