 |
Article dans une revue
TOWARDS A TRANSFORMATION APPROACH OF TIMED UML MARTE SPECIFICATIONS FOR OBSERVER-BASED FORMAL VERIFICATION
Abstract : Modeling timing constraints of distributed systems and multi-clock elec-
tronic systems aims to describe different time requirements aspects at a higher ab-
straction level. An important aspect is the logical time of the behavior of these
systems. To model the time requirements, a specification language with multiple
clock domains called Clock Constraint Specifiation Language (CCSL) has been in-
troduced, in order to enrich the formalisms of existing modeling tools and also to
facilitate the description and analysis of temporal constraints. Once the software
has been modeled, the difficulty lies in both expressing the relevant properties and
verifying them formally. For that purpose formal transformation techniques must
be introduced. However, it remains difficult to exploit initial models as such, and to
integrate them into a formal verification process. This paper introduces a method-
ology and the original tool chain for exploiting UML MARTE models enriched with
CCSL specification. These will be integrated together with a range of tools for
expressing and verifying time constraints. We propose a more general translation
approach that verifies not only CCSL constraints implementations but also prop-
erties of the complete model including all the functional components. We evaluate
our approach with a case study.
https://hal.archives-ouvertes.fr/hal-01326351
Contributeur : Annick Billon-Coat <>
Soumis le : vendredi 3 juin 2016 - 14:52:03
Dernière modification le : mercredi 24 juin 2020 - 16:19:25
Contributeur : Annick Billon-Coat <>
Soumis le : vendredi 3 juin 2016 - 14:52:03
Dernière modification le : mercredi 24 juin 2020 - 16:19:25