Article
المجلة العلمية :
International Journal of Computational Vision and Robotics
ISSN : 1752-9131
الناشر :
معلومات
الفترة : April 2019
المجلد : 9 العدد : 2
الصفحات : 172-191
التفاصيل
A technique to validate automatic generation of Büchi automata from UML 2 sequence diagrams based on multi layer transformations
Nabil Messaoudi Allaoua Chaoui Mohamed Bettaz
Several approaches have been proposed in the literature to transform UML models to formal methods for verification reason. However, few of these approaches take into account the validation of such transformations. This paper is a proposal in this context. It has two parts; first, we propose a technique to control the output of a transformational tool, in order to obtain safe transformational rules, and second, we propose a way to generate the formal model Büchi automata. More particularly, we show how to use multi layer transformations to obtain Büchi automata From UML2SD. The validation technique is based on the algebraic graph transformations and on the use of AGG tool. A scenario of telephone system is taken as a case study to illustrate our validation technique.
الكلمات المفتاحية :
UML 2 sequence diagrams Semantics Model transformations validation Büchi automata AGG
مرجع الإقتباس :
misc-lab-221
DOI :
10.1504/IJCVR.2019.098799
الرابط :
Texte intégral
ACM :
N. Messaoudi, A. Chaoui and M. Bettaz. 2019. A technique to validate automatic generation of Büchi automata from UML 2 sequence diagrams based on multi layer transformations. International Journal of Computational Vision and Robotics, 9, 2 (April 2019), Inderscience, 172-191. DOI: https://doi.org/10.1504/IJCVR.2019.098799.
APA :
Messaoudi, N., Chaoui, A. & Bettaz, M. (2019, April). A technique to validate automatic generation of Büchi automata from UML 2 sequence diagrams based on multi layer transformations. International Journal of Computational Vision and Robotics, 9(2), Inderscience, 172-191. DOI: https://doi.org/10.1504/IJCVR.2019.098799
IEEE :
N. Messaoudi, A. Chaoui and M. Bettaz, "A technique to validate automatic generation of Büchi automata from UML 2 sequence diagrams based on multi layer transformations". International Journal of Computational Vision and Robotics, vol. 9, no. 2, Inderscience, pp. 172-191, April, 2019. DOI: https://doi.org/10.1504/IJCVR.2019.098799.
BibTeX :
@article{misc-lab-221,
author = {Messaoudi, Nabil and Chaoui, Allaoua and Bettaz, Mohamed},
title = {A technique to validate automatic generation of Büchi automata from UML 2 sequence diagrams based on multi layer transformations},
journal = {International Journal of Computational Vision and Robotics},
volume = {9},
number = {2},
issn = {1752-9131},
pages = {172--191},
publisher = {Inderscience},
year = {2019},
month = {April},
doi = {10.1504/IJCVR.2019.098799},
url = {https://www.inderscience.com/info/inarticle.php?artid=98799},
keywords = {UML 2 sequence diagrams, semantics, model transformations validation, Büchi automata, AGG}
}
RIS :
TI  - A technique to validate automatic generation of Büchi automata from UML 2 sequence diagrams based on multi layer transformations
AU - N. Messaoudi
AU - A. Chaoui
AU - M. Bettaz
PY - 2019
SN - 1752-9131
JO - International Journal of Computational Vision and Robotics
VL - 9
IS - 2
SP - 172
EP - 191
PB - Inderscience
AB - Several approaches have been proposed in the literature to transform UML models to formal methods for verification reason. However, few of these approaches take into account the validation of such transformations. This paper is a proposal in this context. It has two parts; first, we propose a technique to control the output of a transformational tool, in order to obtain safe transformational rules, and second, we propose a way to generate the formal model Büchi automata. More particularly, we show how to use multi layer transformations to obtain Büchi automata From UML2SD. The validation technique is based on the algebraic graph transformations and on the use of AGG tool. A scenario of telephone system is taken as a case study to illustrate our validation technique.
KW - UML 2 sequence diagrams
KW - semantics
KW - model transformations validation
KW - Büchi automata
KW - AGG
DO - 10.1504/IJCVR.2019.098799
UR - https://www.inderscience.com/info/inarticle.php?artid=98799
ID - misc-lab-221
ER -