Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL

被引:0
作者
Soualah, Sohaib [1 ,2 ]
Khalgui, Mohamed [3 ]
Chaoui, Allaoua [4 ]
机构
[1] Univ Tunis El Manar, Fac Sci Tunis, Tunis 2092, Tunisia
[2] Univ Carthage, Natl Inst Appl Sci & Technol, LISI Lab, Tunis 1080, Tunisia
[3] Univ Carthage, Natl Inst Appl Sci & Technol, Tunis 1080, Tunisia
[4] Univ Constantine 2 Abdelhamid Mehri, Fac NTIC, MISC Lab, Constantine, Algeria
来源
ADVANCED INFORMATION NETWORKING AND APPLICATIONS, VOL 2, AINA 2024 | 2024年 / 200卷
关键词
Discrete-event Systems; Reconfiguration; Theorem prover; Isabelle/HOL; Parallel Computing Formal Verification;
D O I
10.1007/978-3-031-57853-3_17
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
This paper addresses the formal verification of reconfigurable discrete event systems (RDESs) using Isabelle/HOL proof assistant. A reconfigurable system transitions from one mode to another during its operation to adapt its behavior to the relevant environment. By including such a feature, RDESs become complex and are often costly in terms of computation time and memory. The verification of RDESs consists of two main steps: state space generation and state space analysis. In order to improve these two steps, we propose in this paper, a new approach for verifying system properties that is performed on a developed distributed architecture. The proposed approach allows to avoid redundant computation and reduce execution time by considering the relationships between properties and creating a parallel algorithm that ensures a suitable execution order for each property that is not costly and efficient. The proposed approach is evaluated by exploiting a case study that illustrates the impact of using this approach. The results demonstrate the significance of this paper.
引用
收藏
页码:199 / 212
页数:14
相关论文
共 13 条
[1]   CTL Model Checking in the Cloud Using MapReduce [J].
Camilli, Matteo ;
Bellettini, Carlo ;
Capra, Lorenzo ;
Monga, Mattia .
16TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2014), 2014, :333-340
[2]   On Decomposing Formal Verification of CTL-based Properties on IaaS Cloud Environment [J].
Choucha, Chams Eddine ;
Ramdani, Mohamed ;
Khalgui, Mohamed ;
Kahloul, Laid .
ICSOFT: PROCEEDINGS OF THE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TECHNOLOGIES, 2020, :544-551
[3]   On the Improvement of R-TNCESs Verification using Distributed Cloud-based Architecture [J].
Eddine, Choucha Chams ;
Ben Salem, Mohamed Oussama ;
Khalgui, Mohamed ;
Kahloul, Laid ;
Ougouti, Naima Souad .
ICSOFT: PROCEEDINGS OF THE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TECHNOLOGIES, 2020, :339-349
[4]   On Methodology for the Verification of Reconfigurable Timed Net Condition/Event Systems [J].
Hafidi, Yousra ;
Kahloul, Laid ;
Khalgui, Mohamed ;
Li, Zhiwu ;
Alnowibet, Khalid ;
Qu, Ting .
IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2020, 50 (10) :3577-3591
[5]  
Khalgui M, 2011, ICSOFT 2011: PROCEEDINGS OF THE 6TH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATABASE TECHNOLOGIES, VOL 2, P105
[6]   Automatic NCES-based specification and SESA-based verification of feasible control components in benchmark production systems [J].
Khalgui, Mohamed ;
Hanisch, Hans-Michael .
INTERNATIONAL JOURNAL OF MODELLING IDENTIFICATION AND CONTROL, 2011, 12 (03) :223-243
[7]  
Koubâa A, 2017, IEEE INT CONF AUTON, P329, DOI 10.1109/ICARSC.2017.7964096
[8]  
Ramdani M., 2018, P 13 INT C SOFTW TEC, P625
[9]  
Soualah S., 2021, P 35 ANN EUR SIM MOD
[10]  
Soualah S, 2020, 34TH ANNUAL EUROPEAN SIMULATION AND MODELLING CONFERENCE 2020, ESM 2020, P139