Article
Journal :
Computing and Informatics
ISSN : 2585-8807
Information
Period : March 2020
Volume : 39 Number : 5
Pages : 1022-1060
Details
Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model
Nadia Chabbat Djamel Eddine Saidouni Radja Boukharrou Salim Ghanemi
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.
Key words :
Real-time embedded system UML MARTE DTPN Duration action timed automata Parallel computing Sequence diagram Formal verification
Ref. laboratory citation :
misc-lab-358
DOI :
10.31577/cai_2020_5_1022
Link :
Texte intégral
ACM :
N. Chabbat, D. E. Saidouni, R. Boukharrou and S. Ghanemi. 2020. Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model. Computing and Informatics, 39, 5 (March 2020), 1022-1060. DOI: https://doi.org/10.31577/cai_2020_5_1022.
APA :
Chabbat, N., Saidouni, D. E., Boukharrou, R. & Ghanemi, S. (2020, March). Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model. Computing and Informatics, 39(5), 1022-1060. DOI: https://doi.org/10.31577/cai_2020_5_1022
IEEE :
N. Chabbat, D. E. Saidouni, R. Boukharrou and S. Ghanemi, "Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model". Computing and Informatics, vol. 39, no. 5, pp. 1022-1060, March, 2020. DOI: https://doi.org/10.31577/cai_2020_5_1022.
BibTeX :
@article{misc-lab-358,
author = {Chabbat, Nadia and Saidouni, Djamel Eddine and Boukharrou, Radja and Ghanemi, Salim},
title = {Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model},
journal = {Computing and Informatics},
volume = {39},
number = {5},
issn = {2585-8807},
pages = {1022--1060},
year = {2020},
month = {March},
doi = {10.31577/cai\_2020\_5\_1022},
url = {http://www.cai.sk/ojs/index.php/cai/article/view/2020\_5\_1022},
keywords = {Real-time embedded system, UML MARTE, DTPN, duration action timed automata, parallel computing, sequence diagram, formal verification}
}
RIS :
TI  - Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model
AU - N. Chabbat
AU - D. E. Saidouni
AU - R. Boukharrou
AU - S. Ghanemi
PY - 2020
SN - 2585-8807
JO - Computing and Informatics
VL - 39
IS - 5
SP - 1022
EP - 1060
AB - 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.
KW - Real-time embedded system
KW - UML MARTE
KW - DTPN
KW - duration action timed automata
KW - parallel computing
KW - sequence diagram
KW - formal verification
DO - 10.31577/cai_2020_5_1022
UR - http://www.cai.sk/ojs/index.php/cai/article/view/2020_5_1022
ID - misc-lab-358
ER -