Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model

Authors

  • Nadia Chabbat LAAS Laboratory, , Department of Computer Science, University Badji Mokhtar, Annaba, Algeria
  • Djamel Eddine Saidouni MISC Laboratory, Department of Computer Science, University Abdelhamid Mehri, Constantine 2, Algeria
  • Radja Boukharrou MISC Laboratory, Department of Computer Science, University of Abdelhamid Mehri, Constantine 2, Algeria
  • Salim Ghanemi LAAS Laboratory, Laboratory, Department of Computer Science, University of Badji Mokhtar, Annaba, Algeria

DOI:

https://doi.org/10.31577/cai_2020_5_1022

Keywords:

Real-time embedded system, UML MARTE, DTPN, duration action timed automata, parallel computing, sequence diagram, formal verification

Abstract

The profile UML MARTE offers a general modeling framework for designing and analyzing real-time and embedded systems. Temporal aspects are critical criteria that should be taken into account during the design process. So, formal methods may be used to ensure the functional correctness of such systems. For this purpose, this paper defines an operational method for translating UML sequence diagrams annotated with MARTE stereotypes to time Petri nets with action duration specifications. The semantics of these specifications are defined in terms of duration action timed automata. This allows formal verification by means of several model checker tools like UPPAAL.

Downloads

Download data is not yet available.

Downloads

Published

2021-03-25

How to Cite

Chabbat, N., Saidouni, D. E., Boukharrou, R., & Ghanemi, S. (2021). Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model. Computing and Informatics, 39(5), 1022–1060. https://doi.org/10.31577/cai_2020_5_1022

Issue

Vol. 39 No. 5 (2020): Computing and Informatics

Section

Articles

Most read articles by the same author(s)