Logical Clock Constraint Specification in PVS

Abstract : The Clock Constraint Specification Language (CCSL), first introduced as a companion language for Modeling and Analysis of Real-Time and Embedded systems (MARTE), has now evolved beyond the time specification of MARTE, and has become a full-fledged domain specific modeling language widely used in many domains. This report demonstrates the encoded PVS (Prototype Verification System) theories for interpreting clock relation and clock expression based on schedules as a sequence of clock set. In order to ensure the correctness of the encodings, we prove some interesting properties about the clock constraint. Finally, we give an example to illustrate the approach.
Type de document :
Rapport
[Research Report] 8748, Inria Sophia Antipolis. 2015, pp.11
Liste complète des métadonnées


https://hal.inria.fr/hal-01192839
Contributeur : Team Aoste <>
Soumis le : jeudi 3 septembre 2015 - 16:24:57
Dernière modification le : samedi 17 septembre 2016 - 01:36:46
Document(s) archivé(s) le : vendredi 4 décembre 2015 - 11:55:36

Fichier

RR-8748.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01192839, version 1

Collections

Citation

Qingguo Xu, Robert De Simone, Julien Deantoni. Logical Clock Constraint Specification in PVS. [Research Report] 8748, Inria Sophia Antipolis. 2015, pp.11. <hal-01192839>

Partager

Métriques

Consultations de
la notice

199

Téléchargements du document

95