Logical Clock Constraint Specification in PVS - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2015

Logical Clock Constraint Specification in PVS

Résumé

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.

Mots clés

Fichier principal
Vignette du fichier
RR-8748.pdf (1.02 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01192839 , version 1 (03-09-2015)

Identifiants

  • HAL Id : hal-01192839 , version 1

Citer

Qingguo Xu, Robert de Simone, Julien Deantoni. Logical Clock Constraint Specification in PVS. [Research Report] 8748, Inria Sophia Antipolis. 2015, pp.11. ⟨hal-01192839⟩
158 Consultations
99 Téléchargements

Partager

Gmail Facebook X LinkedIn More