TOWARDS A TRANSFORMATION APPROACH OF TIMED UML MARTE SPECIFICATIONSFOR OBSERVER-BASED FORMAL VERIFICATION

International audienceModeling 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 thesesystems. To model the time requirements, a specification language with multipleclock domains called Clock Constraint Specifiation Language (CCSL) has been in-troduced, in order to enrich the formalisms of existing modeling tools and also tofacilitate the description and analysis of temporal constraints. Once the softwarehas been modeled, the difficulty lies in both expressing the relevant properties andverifying them formally. For that purpose formal transformation techniques mustbe introduced. However, it remains difficult to exploit initial models as such, and tointegrate them into a formal verification process. This paper introduces a method-ology and the original tool chain for exploiting UML MARTE models enriched withCCSL specification. These will be integrated together with a range of tools forexpressing and verifying time constraints. We propose a more general translationapproach that verifies not only CCSL constraints implementations but also prop-erties of the complete model including all the functional components. We evaluateour approach with a case study