Clocks Model for Specification and Analysis of Timing in Real-Time Embedded Systems
Iryna Zaretska, G. M. Zholtkevych, Grygoriy Zholtkevych, Frédéric Mallet · 2013
Problems concerning formal semantics for Clock Constraint Specification Language (CCSL) are considered in the paper. CCSL is intended for describing logical time models for real-time embedded sys- tems and the language is a part of UML profile for MARTE. There exist two approaches to introduce a denotational semantics for CCSL. A pure relational subset of CCSL is defined in the paper. The notion of time structure with clocks is introduced to refine describing denotational se- mantics for this CCSL subset, which authors called RCCSL. Semantic properties of RCCSL have been studied. Theorem about coincidence se- mantics of RCCSL for the two approaches is proved.