Skip to Main content Skip to Navigation

# Verification of clock constraints: CCSL Observers in Esterel

1 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
CRISAM - Inria Sophia Antipolis - Méditerranée , Inria Paris-Rocquencourt, Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : 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 semantics. In the present report we pursue this clarification effort by giving a mathematical characterization to each CCSL constructs. We also propose a systematic approach to the formal verification of CCSL constraints with dedicated Observers. A comprehensive library of Esterel modules, which supports this approach, is provided.
Keywords :
Document type :
Reports
Domain :
Complete list of metadatas

Cited literature [20 references]

https://hal.inria.fr/inria-00458847
Contributor : Charles André <>
Submitted on : Monday, February 22, 2010 - 2:36:42 PM
Last modification on : Monday, October 12, 2020 - 10:30:12 AM
Long-term archiving on: : Friday, June 18, 2010 - 9:36:40 PM

### File

RR-7211.pdf
Files produced by the author(s)

### Identifiers

• HAL Id : inria-00458847, version 1

### Citation

Charles André. Verification of clock constraints: CCSL Observers in Esterel. [Research Report] RR-7211, INRIA. 2010, pp.59. ⟨inria-00458847⟩

Record views

Files downloads