GASCON , Régis

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...

The UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) has been recently adopted. The Clock Constraint Specification Language (CCSL) allows the specification of causal, chronological and timed properties of MARTE models. Due to its purposely broad scope of use, CCSL has an expressiveness that can prevent formal...

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an...

The Clock Constraint Specification Language (CCSL) offers constructs for expressing chronological and causal relations on events of an embedded system. CCSL simulator, TimeSquare allows one to visualize executions of the specified systems by determining step by step sets of synchronously occurring events. When several different sets of events...