Inproceedings
Book title :
15th International Conference on Software Technologies (ICSOFT'2020)
Series :
Communications in Computer and Information Science book series (CCIS)
Address :
Online
ISBN : 978-3-030-83006-9
Publisher :
Information
Period : July 2020
Volume : 1447
Pages : 227-241
Details
Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop
Sohaib Soualah Mohamed Khalgui Allaoua Chaoui Laid Kahloul Yousra Hafidi
This paper deals with the modelling and verification of reconfigurable discrete event systems using model driven engineering Hadoop. Hadoop is therefore a platform for establishing a dialogue between several machines. Its objectives are to solve the main problems of Hard disk size and of computing powers limitations. 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. In this paper, we are interested in reconfigurable discrete event systems, which we formalise using Isabelle/HOL. The proposed method consists of formalising a reconfigurable discrete event system with Isabelle/HOL, using Hadoop, we apply the distributed verification to perform an efficient verification of systems. The reason of this choice consists in the fact that theorem proving deals with the verification of infinite systems while model checking deals with finite systems and suffers from the well known state space explosion problem. Furthermore, thanks to Hadoop it can apply the distributed verification, which means more reduction in verification time. We implement the contributions of this paper using Hadoop platform and Isabelle tool. Finally, we illustrate the proposed method through FESTO MPS case study.
Key words :
Reconfigurable discrete-event systems Hadoop Formal verification Theorem prover Isabelle/HOL
Ref. laboratory citation :
misc-lab-350
DOI :
10.1007/978-3-030-83007-6_11
Link :
Texte intégral
ACM :
S. Soualah, M. Khalgui, A. Chaoui, L. Kahloul and Y. Hafidi. 2020. Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop. In Proceedings of the 15th International Conference on Software Technologies (ICSOFT'2020), Online. Communications in Computer and Information Science book series (CCIS), 1447 (July 2020), Springer, 227-241. DOI: https://doi.org/10.1007/978-3-030-83007-6_11.
APA :
Soualah, S., Khalgui, M., Chaoui, A., Kahloul, L. & Hafidi, Y. (2020, July). Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop. In Proceedings of the 15th International Conference on Software Technologies (ICSOFT'2020), Online. Communications in Computer and Information Science book series (CCIS), 1447, Springer, 227-241. DOI: https://doi.org/10.1007/978-3-030-83007-6_11
IEEE :
S. Soualah, M. Khalgui, A. Chaoui, L. Kahloul and Y. Hafidi, "Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop". In Proceedings of the 15th International Conference on Software Technologies (ICSOFT'2020), Online. Communications in Computer and Information Science book series (CCIS), vol. 1447, Springer, pp. 227-241, July, 2020. DOI: https://doi.org/10.1007/978-3-030-83007-6_11.
BibTeX :
@inproceedings{misc-lab-350,
author = {Soualah, Sohaib and Khalgui, Mohamed and Chaoui, Allaoua and Kahloul, Laid and Hafidi, Yousra},
title = {Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop},
volume = {1447},
booktitle = {15th International Conference on Software Technologies (ICSOFT'2020)},
series = {Communications in Computer and Information Science book series (CCIS)},
location = {Online},
isbn = {978-3-030-83006-9},
pages = {227--241},
publisher = {Springer},
organization = {Eurosis},
year = {2020},
month = {July},
doi = {10.1007/978-3-030-83007-6\_11},
url = {https://www.eurosis.org/cms/files/proceedings/ESM/ESM2020contents.pdf},
keywords = {Reconfigurable discrete-event systems Hadoop Formal verification Theorem prover Isabelle/HOL}
}
RIS :
TY  - CONF
TI - Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop
AU - S. Soualah
AU - M. Khalgui
AU - A. Chaoui
AU - L. Kahloul
AU - Y. Hafidi
PY - 2020
VL - 1447
BT - 15th International Conference on Software Technologies (ICSOFT'2020), Online
SN - 978-3-030-83006-9
SP - 227
EP - 241
PB - Springer
AB - This paper deals with the modelling and verification of reconfigurable discrete event systems using model driven engineering Hadoop. Hadoop is therefore a platform for establishing a dialogue between several machines. Its objectives are to solve the main problems of Hard disk size and of computing powers limitations. 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. In this paper, we are interested in reconfigurable discrete event systems, which we formalise using Isabelle/HOL. The proposed method consists of formalising a reconfigurable discrete event system with Isabelle/HOL, using Hadoop, we apply the distributed verification to perform an efficient verification of systems. The reason of this choice consists in the fact that theorem proving deals with the verification of infinite systems while model checking deals with finite systems and suffers from the well known state space explosion problem. Furthermore, thanks to Hadoop it can apply the distributed verification, which means more reduction in verification time. We implement the contributions of this paper using Hadoop platform and Isabelle tool. Finally, we illustrate the proposed method through FESTO MPS case study.
KW - Reconfigurable discrete-event systems Hadoop Formal verification Theorem prover Isabelle/HOL
DO - 10.1007/978-3-030-83007-6_11
UR - https://www.eurosis.org/cms/files/proceedings/ESM/ESM2020contents.pdf
ID - misc-lab-350
ER -