Verification of clock constraints: CCSL Observers in Esterel - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2010

Verification of clock constraints: CCSL Observers in Esterel

(1)
1

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.
Fichier principal
Vignette du fichier
RR-7211.pdf (1.3 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00458847 , version 1 (22-02-2010)

Identifiers

  • HAL Id : inria-00458847 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More