A GSPN-based formalism under infinite-server semantics for reconfigurable WANETs
Abstract
Reconfigurable wireless ad hoc networks (R-WANETs) constitute a well-known paradigm of networks that change their structure to fulfill dynamic requirements and/or respond to their volatile environments. Several formalisms have been exploited and extended for the modeling, verification, and performance evaluation of R-WANETs. Distinguishably, generalized stochastic Petri nets (GSPNs) have been extended to some formalisms involved in the design of various kinds of networks. However, these extensions show many shortcomings. In particular, dynamic GSPNs (D-GSPNs) only allow the modeling and verification of reconfigurations in GSPNs under single-server semantics. This restriction was imposed to enable the transformation of D-GSPNs into basic GSPNs. In this paper, we extend D-GSPNs to a new formalism called improved D-GSPNs (ID-GSPNs), enabling the modeling and verification of dynamic nets whose transitions follow infinite-, single-, or multi-server semantics. Furthermore, a new algorithm that unfolds ID-GSPNs towards basic GSPNs while preserving their stochastic behaviors is provided. Additionally, the proposed algorithm yields more compact models than those obtained by existing unfolding algorithms. Finally, the proposed formalism is exploited in the modeling, verification, and performance evaluation of R-WANETs.
References
[1]
Jiang D, Wang Z, Wang W, Lv Z, and Choo K-KR AI-assisted energy-efficient and intelligent routing for reconfigurable wireless networks IEEE Trans Netw Sci Eng 2022 9 1 78-88
[2]
Grichi H, Mosbahi O, Khalgui M, and Li Z New power-oriented methodology for dynamic resizing and mobility of reconfigurable wireless sensor networks IEEE Trans Syst Man Cybern Syst 2018 48 7 1120-1130
[3]
Ben Aissa Y, Bachir A, Khalgui M, Koubaa A, Li Z, and Qu T On feasibility of multichannel reconfigurable wireless sensor networks under real-time and energy constraints IEEE Trans Syst Man Cybern Syst 2021 51 3 1446-1461
[4]
Ma C, Li Y, Yang B, Zhang Y, and Guo F Relay node placement for building wireless sensor networks with reconfigurability provision Ad Hoc Netw 2020 107
[5]
Durán F, Krishna A, Le Pallec M, Mateescu R, and Salaün G Models and analysis for user-driven reconfiguration of rule-based IoT applications Internet of Things 2022
[6]
El Khediri S Wireless sensor networks: a survey, categorization, main issues, and future orientations for clustering protocols Computing 2022 104 8 1775-1837
[7]
El-Mougy A, Ibnkahla M, Hattab G, and Ejaz W Reconfigurable wireless networks Proc IEEE 2015 103 7 1125-1158
[8]
Fang Z, Fu H, Gu T, Qian Z, Jaeger T, Hu P, and Mohapatra P A model checking-based security analysis framework for IoT systems High-Confid Comput 2021 1 1
[9]
Alur R and Dill D Paterson MS Automata for modeling real-time systems Automata, languages and programming 1990 Berlin, Heidelberg Springer 322-335
[10]
Murata T Petri nets: properties, analysis and applications Proc IEEE 1989 77 4 541-580
[11]
Mocci A and Sangiorgio M Detecting component changes at run time with behavior models Computing 2013 95 191-221
[12]
Bettira R, Kahloul L, Khalgui M, Li Z (2019) Reconfigurable hierarchical timed automata: modeling and stochastic verification. In: 2019 IEEE international conference on systems, man and cybernetics (SMC), pp 2364–2371
[13]
Tigane S, Guerrouf F, Hamani N, Kahloul L, Khalgui M, and Ali MA Dynamic timed automata for reconfigurable system modeling and verification Axioms 2023
[14]
Marsan MA, Balbo G, Conte G, Donatelli S, and Franceschinis G Modelling with generalized stochastic Petri nets 1994 1 New York, NY, USA Wiley Inc
[15]
Babaie S, Khosrohosseini A, and Khadem-Zadeh A A new self-diagnosing approach based on Petri nets and correlation graphs for fault management in wireless sensor networks J Syst Archit 2013 59 8 582-600
[16]
Zhang Y, Wang W, Du W, Qian C, and Yang H Coloured Petri net-based active sensing system of real-time and multi-source manufacturing information for smart factory Int J Adv Manuf Technol 2018 94 9 3427-3439
[17]
Mendonça J, Andrade E, and Lima R Assessing mobile applications performance and energy consumption through experiments and stochastic models Computing 2019 101 1789-1811
[18]
Zhou M, Han L, Lu H, and Fu C Distributed collaborative intrusion detection system for vehicular ad hoc networks based on invariant Comput Netw 2020
[19]
Zroug S, Kahloul L, Benharzallah S, and Djouani K A hierarchical formal method for performance evaluation of WSNs protocol Computing 2021 103 6 1183-1208
[20]
Rodrigues L, Gonçalves I, Fé I, Endo PT, and Silva FA Performance and availability evaluation of an smart hospital architecture Computing 2021 103 10 2401-2435
[21]
Oukas N and Boulif M Sensor performance evaluation for long-lasting EH-WSNs by GSPN formulation, considering seasonal sunshine levels and dual standby strategy Arab J Sci Eng 2023 48 2 1677-1691
[22]
Vanson G, Marangé P, and Levrat E End-of-life decision making in circular economy using generalized colored stochastic Petri nets Auton Intell Syst 2022 2 1 3
[23]
Lin Y-N, Wang S-K, Chiou G-J, Yang C-Y, Shen VR, Juang TT-Y, and Huang T-J Novel deadlock control for smartphone manufacturing systems using Petri nets Int J Control Autom Syst 2022 20 3 877-887
[24]
Berger S, van Dun C, and Häckel B IT availability risks in smart factory networks-analyzing the effects of IT threats on production processes using Petri nets Inf Syst Front 2022
[25]
Camilli M and Capra L Formal specification and verification of decentralized self-adaptive systems using symmetric nets Discrete Event Dyn Syst 2021 31 609-657
[26]
Chiola G, Dutheillet C, Franceschinis G, and Haddad S Stochastic well-formed colored nets and symmetric modeling applications IEEE Trans Comput 1993 42 11 1343-1360
[27]
Li J, Dai X, Meng Z, Dou J, and Guan X Rapid design and reconfiguration of Petri net models for reconfigurable manufacturing cells with improved net rewriting systems and activity diagrams Comput Ind Eng 2009 57 4 1431-1451
[28]
Hafidi Y, Kahloul L, Khalgui M, Li Z, Alnowibet K, and Qu T On methodology for the verification of reconfigurable timed net condition/event systems IEEE Trans Syst Man Cybern Syst 2020 50 10 3577-3591
[29]
Tigane S, Kahloul L, Hamani N, Khalgui M, and Ali MA On quantitative properties preservation in reconfigurable generalized stochastic Petri nets IEEE Trans Syst Man Cybern Syst 2022
[30]
Tigane S, Kahloul L, Baarir S, Bourekkache S (2020) Dynamic GSPNs: formal definition, transformation towards GSPNs and formal verification. In: Proceedings of the 13th EAI international conference on performance evaluation methodologies and tools. VALUETOOLS ’20, pp 164–171. Association for Computing Machinery, New York, NY, USA
[31]
Balsamo S, Marin A, and Stojic I Agha G and Van Houdt B SPNPS: a tool for perfect sampling in stochastic Petri nets Quantitative evaluation of systems 2016 Cham Springer 163-166
[32]
Dufourd C, Finkel A, Schnoebelen P (1998) Reset nets between decidability and undecidability. Automata. Languages and Programming. Springer, Berlin, Heidelberg, pp 103–115
[33]
Baldan P, Corradini A, and Montanari U Relating SPO and DPO graph rewriting with Petri nets having read, inhibitor and reset arcs Electronic notes in theoretical computer science 2005 127 2 5-28
[34]
König B, Nolte D, Padberg J, Rensink A (2018) A Tutorial on Graph Transformation, pp. 83–104. Springer, Cham .
[35]
Kulcsár G, Lochau M, Schürr A (2018) Graph-rewriting Petri nets. In: Graph Transformation, pp. 79–96. Springer, Cham
[36]
Hoffmann K, Ehrig H, Mossakowski T (2005) High-level nets with nets and rules as tokens. In: Applications and theory of Petri nets 2005, pp. 268–288. Springer, Berlin, Heidelberg
[37]
Lambers L, Ehrig H, and Orejas F Conflict detection for graph transformation with negative application conditions Graph transformations 2006 Berlin, Heidelberg Springer 61-76
Recommendations
A semantics for every GSPN
PETRI NETS'13: Proceedings of the 34th international conference on Application and Theory of Petri Nets and ConcurrencyGeneralised Stochastic Petri Nets (GSPNs) are a popular modelling formalism for performance and dependability analysis. Their semantics is traditionally associated to continuous-time Markov chains (CTMCs), enabling the use of standard CTMC analysis ...
Reconfigurable GSPNs: A modeling formalism of evolvable discrete-event systems
AbstractNowadays, a wide range of systems are becoming structurally dynamic, variably interconnected, and highly complex. The use of classical formal approaches, such as Petri nets, in the design of such systems becomes neither convenient nor ...
Highlights- A new Petri nets based formalism is proposed for reconfigurable systems.
- The ...
Kripke modelling and verification of temporal specifications of a multiple UAV system
A verifiable multiple UAV system cooperatively monitoring a road network is presented in this paper. The focus is on formal modelling and verification which can guarantee correctness of concurrent reactive systems such as multi-UAV systems. Kripke ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s), under exclusive licence to Springer-Verlag GmbH Austria, part of Springer Nature 2023. Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 25 May 2023
Accepted: 02 May 2023
Received: 22 August 2022
Author Tags
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 27 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in