Co-Algebraic Semantic Model for the Clock Constraint Specification Language

Frédéric Mallet 1, * Zholtkevych Grygoriy 2
* Auteur correspondant
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, COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : 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 model for CCSL based on the notion of “clock coalgebra”. Coalgebra promises to give a unified framework to study the behavior and semantics of reactive systems and, more generally, infinite data structures. They appear as being the adequate mathematical structure to capture the infinite nature of CCSL operators. This paper proposes a coalgebraic structure for CCSL, or rather a natural generalization of CCSL that we call generalized clock constraints: GenCCSL. We establish that GenCCSL covers the class of CCSL constraints and we give examples of GenCCSL constraints that cannot be expressed with classical CCSL. Then, we discuss the properties of the newly introduced class, including ways to detect valid and invalid GenCCSL behaviors, as well as deciding whether a GenCCSL constraint is also a CCSL one.
Type de document :
Communication dans un congrès
Formal Techniques for Safety-Critical Systems - ICFEM/FTSCS 2014, Nov 2014, Luxembourg, Luxembourg. Springer, <http://csaba.olveczky.se/ftscs14-preproceedings.pdf>
Liste complète des métadonnées

https://hal.inria.fr/hal-01096688
Contributeur : Frédéric Mallet <>
Soumis le : jeudi 18 décembre 2014 - 06:26:37
Dernière modification le : mardi 19 janvier 2016 - 01:05:28

Identifiants

  • HAL Id : hal-01096688, version 1

Collections

Citation

Frédéric Mallet, Zholtkevych Grygoriy. Co-Algebraic Semantic Model for the Clock Constraint Specification Language. Formal Techniques for Safety-Critical Systems - ICFEM/FTSCS 2014, Nov 2014, Luxembourg, Luxembourg. Springer, <http://csaba.olveczky.se/ftscs14-preproceedings.pdf>. <hal-01096688>

Partager

Métriques

Consultations de la notice

117