Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

A Transformation Approach for Multiform Time Requirements

Nadia Menad 1 Philippe Dhaussy 2
2 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
STIC - Pôle STIC [Brest], Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
Abstract : Many of the timing constraints expressed in physical prescriptions of distributed systems and multi-clock electronic systems can be expressed in logical concepts. A logical time model has been developed as a part of the official OMG UML profile MARTE, in order to enrich the formalism of this profile and also to facilitate the description and analysis of temporal constraints. This time model is associated with CCSL (Clock Constraint Specification Language). Once the software is modeled, the difficulty lies in both expressing the relevant properties and in verifying them formally. We present an automatic transformation technique related to a method for verifying properties by model checking, thus exploiting both the CDL language (Context Description Language) and the OBP tool (Observerbased Prover). The technique is based on a translation ofMARTE models and the CCSL constraints into Fiacre code. CDL can express predicates and observers. These are verified during the exhaustive exploration of the complete model by OBP. We illustrate our contribution by an illustrative case.
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-00912857
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 2 décembre 2013 - 17:02:46
Dernière modification le : mercredi 24 juin 2020 - 16:19:20

Identifiants

  • HAL Id : hal-00912857, version 1

Citation

Nadia Menad, Philippe Dhaussy. A Transformation Approach for Multiform Time Requirements. SEFM'13, Sep 2013, Madrid, Spain. pp.16-30. ⟨hal-00912857⟩

Partager

Métriques

Consultations de la notice

598