Towards a Transformation Approach of Timed UML MARTE Specifications for Observer-Based Formal Verification

Authors

  • Nadia Menad University of Science and Technology of Oran Mohamed Boudiaf, Department of Computer Science, Faculty of Mathematics and Computer Science
  • Philippe Dhaussy UEB, Lab-STICC Laboratory UMR CNRS 6285, ENSTA Bretagne
  • Zoé Drey UEB, Lab-STICC Laboratory UMR CNRS 6285, ENSTA Bretagne
  • Rachida Mekki University of Science and Technology of Oran Mohamed Boudiaf, Department of Computer Science, Faculty of Mathematics and Computer Science

Keywords:

Formal verification, model-checking, CCSL time constraints, observer automata

Abstract

Modeling timing constraints of distributed systems and multi-clock electronic systems aims to describe different time requirements aspects at a higher abstraction 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 Specification Language (CCSL) has been introduced, 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 methodology 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 properties of the complete model including all the functional components. We evaluate our approach with a case study.

Downloads

Download data is not yet available.

Author Biography

Philippe Dhaussy, UEB, Lab-STICC Laboratory UMR CNRS 6285, ENSTA Bretagne

Professor

Downloads

Published

2016-07-11

How to Cite

Menad, N., Dhaussy, P., Drey, Z., & Mekki, R. (2016). Towards a Transformation Approach of Timed UML MARTE Specifications for Observer-Based Formal Verification. COMPUTING AND INFORMATICS, 35(2), 338–368. Retrieved from http://www.cai.sk/ojs/index.php/cai/article/view/2381