Inproceedings
Book title :
International Conference on Software Technologies (ICSOFT'20)
Address :
Online Streaming
Information
Period : July 2020
Details
Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL
Sohaib Soualah Yousra Hafidi Mohamed Khalgui Allaoua Chaoui Laïd Kahloul
This paper deals with the modelling and verification of reconfigurable discrete event systems using model driven engineering (MDE) and Isabelle/HOL. MDE is a software development methodology followed by engineers. Isabelle/HOL is an interactive/automated theorem prover that combines the functional programming paradigm with high order logic (HOL), which makes it efficient for developing solid formalizations. We are interested in combining these two complementary technologies by mapping elements of MDE into Isabelle/HOL. In this paper, we present a transformation process from Ecore models, to functional data structures, used in proof assistants. This transformation method is based on Model-driven engineering and defined by a set of transformation rules that are described using formal presentations. Furthermore, in order to avoid redundant computations in RDESs, we propose a new algorithm for improved verification. We implement the contributions of this paper using Eclipse environment and Isabelle tool. Finally, we illustrate the proposed approach through FESTO MPS case study.
Key words :
Reconfigurable Discrete-event Systems Model Driven Engineering Model Transformation Meta-model Formal Verification Theorem Prover Isabelle/HOL
Texte intégral
ACM :
S. Soualah, Y. Hafidi, M. Khalgui, A. Chaoui and L. Kahloul. 2020. Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL. In Proceedings of the International Conference on Software Technologies (ICSOFT'20), Online Streaming (July 2020). https://www.insticc.org/node/TechnicalProgram/icsoft/2020/presentationDetails/98936.
APA :
Soualah, S., Hafidi, Y., Khalgui, M., Chaoui, A. & Kahloul, L. (2020, July). Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL. In Proceedings of the International Conference on Software Technologies (ICSOFT'20), Online Streaming.Retrieved from https://www.insticc.org/node/TechnicalProgram/icsoft/2020/presentationDetails/98936
IEEE :
S. Soualah, Y. Hafidi, M. Khalgui, A. Chaoui and L. Kahloul, "Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL". In Proceedings of the International Conference on Software Technologies (ICSOFT'20), Online Streaming, July, 2020, https://www.insticc.org/node/TechnicalProgram/icsoft/2020/presentationDetails/98936.
BibTeX :
@inproceedings{misc-lab-334,
author = {Soualah, Sohaib and Hafidi, Yousra and Khalgui, Mohamed and Chaoui, Allaoua and Kahloul, La\"{i}d},
title = {Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL},
booktitle = {International Conference on Software Technologies (ICSOFT'20)},
location = {Online Streaming},
year = {2020},
month = {July},
url = {https://www.insticc.org/node/TechnicalProgram/icsoft/2020/presentationDetails/98936},
keywords = {Reconfigurable Discrete-event Systems, Model Driven Engineering, Model Transformation, Meta-model Formal Verification, Theorem Prover, Isabelle/HOL}
}
RIS :
TY  - CONF
TI - Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL
AU - S. Soualah
AU - Y. Hafidi
AU - M. Khalgui
AU - A. Chaoui
AU - L. Kahloul
PY - 2020
BT - International Conference on Software Technologies (ICSOFT'20), Online Streaming
AB - This paper deals with the modelling and verification of reconfigurable discrete event systems using model driven engineering (MDE) and Isabelle/HOL. MDE is a software development methodology followed by engineers. Isabelle/HOL is an interactive/automated theorem prover that combines the functional programming paradigm with high order logic (HOL), which makes it efficient for developing solid formalizations. We are interested in combining these two complementary technologies by mapping elements of MDE into Isabelle/HOL. In this paper, we present a transformation process from Ecore models, to functional data structures, used in proof assistants. This transformation method is based on Model-driven engineering and defined by a set of transformation rules that are described using formal presentations. Furthermore, in order to avoid redundant computations in RDESs, we propose a new algorithm for improved verification. We implement the contributions of this paper using Eclipse environment and Isabelle tool. Finally, we illustrate the proposed approach through FESTO MPS case study.
KW - Reconfigurable Discrete-event Systems
KW - Model Driven Engineering
KW - Model Transformation
KW - Meta-model Formal Verification
KW - Theorem Prover
KW - Isabelle/HOL
UR - https://www.insticc.org/node/TechnicalProgram/icsoft/2020/presentationDetails/98936
ID - misc-lab-334
ER -