Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL

R. Gascon 1 Frédéric Mallet 1 Julien Deantoni 1
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 UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) provides a means to specify embedded systems. The Clock Constraint Specification Language (CCSL) allows the specification of causal, chronological and timed properties of MARTE models. Due to its purposedly broad scope of use, CCSL has an expressiveness that can prevent formal verification. However, when addressing hardware electronic systems, formal verification is an important step of the development. The IEEE Property Specification Language (PSL) provides a formal notation for expressing temporal logic properties that can be automatically verified on electronic system models. We want to identify the part of MARTE/CCSL amenable to support the classical analysis methods from the Electronic Design Automation (EDA) community. In this paper, we contribute to this goal by comparing CCSL and PSL expressiveness. We show that none of these languages is subsumed by the other one. We identify the CCSL constructs that cannot be expressed in temporal logics and propose restrictions of these operators so that they become tractable in temporal logics. Conversely, we also identify the class of PSL formulas that can be encoded in CCSL. We define translations between these fragments of CCSL and PSL using automata as an intermediate representation.
Type de document :
Rapport
[Research Report] RR-7459, INRIA. 2011
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00540738
Contributeur : Regis Gascon <>
Soumis le : mercredi 5 janvier 2011 - 14:43:42
Dernière modification le : lundi 5 novembre 2018 - 15:36:03
Document(s) archivé(s) le : lundi 5 novembre 2012 - 15:35:48

Fichier

RR7459.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00540738, version 2

Citation

R. Gascon, Frédéric Mallet, Julien Deantoni. Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL. [Research Report] RR-7459, INRIA. 2011. 〈inria-00540738v2〉

Partager

Métriques

Consultations de la notice

597

Téléchargements de fichiers

257