TY - JOUR
T1 - RCTL
T2 - New Temporal Logic for Improved Formal Verification of Reconfigurable Discrete-Event Systems
AU - Ramdani, Mohamed
AU - Kahloul, Laid
AU - Khalgui, Mohamed
AU - Li, Zhiwu
AU - Zhou, Meng Chu
N1 - Funding Information:
Manuscript received February 25, 2020; accepted June 18, 2020. Date of publication July 27, 2020; date of current version July 2, 2021. This article was recommended for publication by Associate Editor V. Stojanovic and Editor B. Vogel-Heuser upon evaluation of the reviewers’ comments. This work was supported in part by the National Natural Science Foundation of China, in part by the National Key R&D Program of China under Grant 2018YFB1700104, in part by the Science and Technology Development Fund, Macao Special Administrative Region (MSAR), under Grant 078/2015/A3 and Grant 106/20156/A3, and in part by the General Directorate of Scientific Research and Technological Development DGRSDT/MESRS, Algeria. (Corresponding authors: Mohamed Khalgui; Zhiwu Li.) Mohamed Ramdani is with the School of Electrical and Information Engineering, Jinan University (Zhuhai Campus), Zhuhai 519070, China, also with the Laboratoire d’INFormatique Intelligente (LINFI) Laboratory, Biskra University, Biskra 07000, Algeria, also with the National Institute of Applied Sciences and Technology, University of Carthage, Tunis 1080, Tunisia, and also with the Faculty of Sciences of Tunis, University of Tunis El Manar, Tunis 2092, Tunisia (e-mail: ramdani.moh19@gmail.com).
Publisher Copyright:
© 2004-2012 IEEE.
PY - 2021/7
Y1 - 2021/7
N2 - This article deals with improved formal verification of reconfigurable discrete-event systems (DESs) modeled by reconfigurable timed net condition event systems (R-TNCESs). An R-TNCES consists of a set of timed net condition event systems, each of which represents a particular behavior of a DES, and a reconfiguration scenario is a switching mode from a timed net condition event system to another. However, the verification with the classical computation tree logic (CTL) as well as the related extensions increases the number of properties for complete verification of a complex R-TNCES. We propose reconfigurable CTL as a new extension of CTL to reduce such a number. New connectors of reconfigurable CTL are proposed, with their formal syntax and semantics, and a set of new algorithms is proposed to control the complexity of model checking. We use a benchmark production system for the performance evaluation of the proposed approach. Reduction in the number of properties to be checked is shown, and consequently, the related validation time is reduced. Note to Practitioners - This research represents a new orientation for guiding efficiently the model checking of reconfigurable discrete-event systems. A classification of properties described in computation tree logic (CTL), according to their dominance and equivalence relations, allows one to conduct an efficient verification by avoiding inefficient calculation due to redundant properties. In this case, giving a verification order for these properties allows one to shorten their verification time. An extension named reconfigurable CTL describes the new syntax of the proposed classification. This approach can be applied in modeling and verification of advanced reconfigurable systems arising from smart grids, adaptive sensor networks, intelligent transportation, reconfigurable manufacturing, and embedded systems.
AB - This article deals with improved formal verification of reconfigurable discrete-event systems (DESs) modeled by reconfigurable timed net condition event systems (R-TNCESs). An R-TNCES consists of a set of timed net condition event systems, each of which represents a particular behavior of a DES, and a reconfiguration scenario is a switching mode from a timed net condition event system to another. However, the verification with the classical computation tree logic (CTL) as well as the related extensions increases the number of properties for complete verification of a complex R-TNCES. We propose reconfigurable CTL as a new extension of CTL to reduce such a number. New connectors of reconfigurable CTL are proposed, with their formal syntax and semantics, and a set of new algorithms is proposed to control the complexity of model checking. We use a benchmark production system for the performance evaluation of the proposed approach. Reduction in the number of properties to be checked is shown, and consequently, the related validation time is reduced. Note to Practitioners - This research represents a new orientation for guiding efficiently the model checking of reconfigurable discrete-event systems. A classification of properties described in computation tree logic (CTL), according to their dominance and equivalence relations, allows one to conduct an efficient verification by avoiding inefficient calculation due to redundant properties. In this case, giving a verification order for these properties allows one to shorten their verification time. An extension named reconfigurable CTL describes the new syntax of the proposed classification. This approach can be applied in modeling and verification of advanced reconfigurable systems arising from smart grids, adaptive sensor networks, intelligent transportation, reconfigurable manufacturing, and embedded systems.
KW - Computation tree logic (CTL)
KW - Petri net
KW - discrete-event system (DES)
KW - model checking
KW - reconfigurable CTL (RCTL)
KW - reconfigurable timed net condition event system (R-TNCES)
KW - reconfiguration
UR - http://www.scopus.com/inward/record.url?scp=85112697442&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85112697442&partnerID=8YFLogxK
U2 - 10.1109/TASE.2020.3006435
DO - 10.1109/TASE.2020.3006435
M3 - Article
AN - SCOPUS:85112697442
SN - 1545-5955
VL - 18
SP - 1392
EP - 1405
JO - IEEE Transactions on Automation Science and Engineering
JF - IEEE Transactions on Automation Science and Engineering
IS - 3
M1 - 9149784
ER -