{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:15:11Z","timestamp":1763968511058,"version":"build-2065373602"},"reference-count":40,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2023,2,22]],"date-time":"2023-02-22T00:00:00Z","timestamp":1677024000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Axioms"],"abstract":"<jats:p>Modern discrete-event systems (DESs) are often characterized by their dynamic structures enabling highly flexible behaviors that can respond in real time to volatile environments. On the other hand, timed automata (TA) are powerful tools used to design various DESs. However, they lack the ability to naturally describe dynamic-structure reconfigurable systems. Indeed, TA are characterized by their rigid structures, which cannot handle the complexity of dynamic structures. To overcome this limitation, we propose an extension to TA, called dynamic timed automata (DTA), enabling the modeling and verification of reconfigurable systems. Additionally, we present a new algorithm that transforms DTA into semantic-equivalent TA while preserving their behavior. We demonstrate the usefulness and applicability of this new modeling and verification technique using an illustrative example.<\/jats:p>","DOI":"10.3390\/axioms12030230","type":"journal-article","created":{"date-parts":[[2023,2,23]],"date-time":"2023-02-23T02:01:25Z","timestamp":1677117685000},"page":"230","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Dynamic Timed Automata for Reconfigurable System Modeling and Verification"],"prefix":"10.3390","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9093-1180","authenticated-orcid":false,"given":"Samir","family":"Tigane","sequence":"first","affiliation":[{"name":"LINFI Laboratory, Computer Science Department, University of Biskra, Biskra 07000, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6917-8032","authenticated-orcid":false,"given":"Fay\u00e7al","family":"Guerrouf","sequence":"additional","affiliation":[{"name":"LINFI Laboratory, Computer Science Department, University of Biskra, Biskra 07000, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6151-2585","authenticated-orcid":false,"given":"Nadia","family":"Hamani","sequence":"additional","affiliation":[{"name":"LTI Laboratory, University of Picardie Jules Verne, 02100 Saint-Quentin, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9739-7715","authenticated-orcid":false,"given":"Laid","family":"Kahloul","sequence":"additional","affiliation":[{"name":"LINFI Laboratory, Computer Science Department, University of Biskra, Biskra 07000, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6311-3588","authenticated-orcid":false,"given":"Mohamed","family":"Khalgui","sequence":"additional","affiliation":[{"name":"National Institute of Applied Sciences and Technology, University of Carthage, Tunis 1080, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1426-5339","authenticated-orcid":false,"given":"Masood Ashraf","family":"Ali","sequence":"additional","affiliation":[{"name":"Department of Industrial Engineering, College of Engineering, Prince Sattam bin Abdulaziz University, Al-Kharj 11942, Saudi Arabia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2023,2,22]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Dima, A., Bugheanu, A.M., Boghian, R., and Madsen, D.O. (2023). Mapping Knowledge Area Analysis in E-Learning Systems Based on Cloud Computing. Electronics, 12.","DOI":"10.3390\/electronics12010062"},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"2453","DOI":"10.1007\/s10586-019-03018-9","article-title":"A hybrid formal verification approach for QoS-aware multi-cloud service composition","volume":"23","author":"Souri","year":"2020","journal-title":"Clust. Comput."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Jasim, A.M., Jasim, B.H., Neagu, B.C., and Alhasnawi, B.N. (2023). Efficient Optimization Algorithm-Based Demand-Side Management Program for Smart Grid Residential Load. Axioms, 12.","DOI":"10.3390\/axioms12010033"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Ecer, F., B\u00f6y\u00fckaslan, A., and Hashemkhani Zolfani, S. (2022). Evaluation of Cryptocurrencies for Investment Decisions in the Era of Industry 4.0: A Borda Count-Based Intuitionistic Fuzzy Set Extensions EDAS-MAIRCA-MARCOS Multi-Criteria Methodology. Axioms, 11.","DOI":"10.3390\/axioms11080404"},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"26759","DOI":"10.1007\/s11042-021-10645-1","article-title":"Cloud manufacturing service composition in IoT applications: A formal verification-based approach","volume":"81","author":"Souri","year":"2022","journal-title":"Multimed. Tools Appl."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Awan, K.A., Ud Din, I., Almogren, A., Khattak, H.A., and Rodrigues, J.J.P.C. (2023). EdgeTrust: A Lightweight Data-Centric Trust Management Approach for IoT-Based Healthcare 4.0. Electronics, 12.","DOI":"10.3390\/electronics12010140"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1007\/s10009-020-00596-7","article-title":"Programming dynamic reconfigurable systems","volume":"23","author":"Bensalem","year":"2021","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Paterson, M.S. (1990). Automata, Languages and Programming, Proceedings of the 17th International Colloquium, Warwick University, UK, 16\u201320 July 1990, Springer.","DOI":"10.1007\/BFb0032016"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"e3808","DOI":"10.1002\/dac.3808","article-title":"Formal verification approaches in the web service composition: A comprehensive analysis of the current challenges for future research","volume":"31","author":"Souri","year":"2018","journal-title":"Int. J. Commun. Syst."},{"key":"ref_10","unstructured":"Vaandrager, F. (2011). Industrial Handbook, Available online: https:\/\/www.researchgate.net\/publication\/228919420_A_First_Introduction_to_Uppaal."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., and Larsen, K.G. (2004, January 13\u201318). A tutorial on UPPAAL. Proceedings of the Formal Methods for the Design of Real-Time Systems, Bertinoro, Italy.","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"75169","DOI":"10.1109\/ACCESS.2021.3081587","article-title":"Security Verification for Cyber-Physical Systems Using Model Checking","volume":"9","author":"Chan","year":"2021","journal-title":"IEEE Access"},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1109\/TSE.2016.2560842","article-title":"Timed Automata Modeling and Verification for Publish-Subscribe Structures Using Distributed Resources","volume":"43","author":"Valero","year":"2017","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"1324","DOI":"10.1007\/s11390-020-0537-8","article-title":"Modelling and verification of real-time publish and subscribe protocol using UPPAAL and Simulink\/Stateflow","volume":"35","author":"Lin","year":"2020","journal-title":"J. Comput. Sci. Technol."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/TII.2019.2943913","article-title":"An Extension to the Precision Time Protocol (PTP) to Enable the Detection of Cyber Attacks","volume":"16","author":"Moussa","year":"2020","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"33741","DOI":"10.1109\/ACCESS.2019.2903153","article-title":"Predictive Formal Analysis of Resilience in Cyber-Physical Systems","volume":"7","author":"Mouelhi","year":"2019","journal-title":"IEEE Access"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","article-title":"Petri nets: Properties, analysis and applications","volume":"77","author":"Murata","year":"1989","journal-title":"Proc. IEEE"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Kulcs\u00e1r, G., Lochau, M., and Sch\u00fcrr, A. (2018, January 25\u201326). Graph-rewriting Petri nets. Proceedings of the International Conference on Graph Transformation (ICGT 2018), Toulouse, France.","DOI":"10.1007\/978-3-319-92991-0_6"},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"102302","DOI":"10.1016\/j.scico.2019.102302","article-title":"Reconfigurable GSPNs: A modeling formalism of evolvable discrete-event systems","volume":"183","author":"Tigane","year":"2019","journal-title":"Sci. Comput. Program."},{"key":"ref_20","first-page":"2883","article-title":"Time-Variant Graph Classification","volume":"50","author":"Wang","year":"2020","journal-title":"IEEE Trans. Syst. Man Cybern. Syst."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Tigane, S., Kahloul, L., Hamani, N., Khalgui, M., and Ali, M.A. (2022). On Quantitative Properties Preservation in Reconfigurable Generalized Stochastic Petri Nets. IEEE Trans. Syst. Man Cybern. Syst., early access.","DOI":"10.1109\/TSMC.2022.3225280"},{"key":"ref_22","unstructured":"Heckel, R., K\u00fcster, J.M., and Taentzer, G. Confluence of Typed Attributed Graph Transformation Systems. Proceedings of the Graph Transformation."},{"key":"ref_23","unstructured":"Jayaraman, P., Whittle, J., Elkhodary, A.M., and Gomaa, H. (October, January 30). Model Composition in Product Lines and Feature Interaction Detection Using Critical Pair Analysis. Proceedings of the Model Driven Engineering Languages and Systems, Nashville, TN, USA."},{"key":"ref_24","unstructured":"Taentzer, G. (2004). Proceedings of the Applications of Graph Transformations with Industrial Relevance, Charlottesville, VA, USA, 27 September\u20131 October 2003, Springer."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"G\u00f6ttmann, H., Luthmann, L., Lochau, M., and Sch\u00fcrr, A. (2020, January 19\u201323). Real-Time-Aware Reconfiguration Decisions for Dynamic Software Product Lines. Proceedings of the 24th ACM Conference on Systems and Software Product Line, Montreal, QC, Canada.","DOI":"10.1145\/3382025.3414945"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"G\u00f6ttmann, H., Bacher, I., Gottwald, N., and Lochau, M. (2021, January 9\u201311). Static Analysis Techniques for Efficient Consistency Checking of Real-Time-Aware DSPL Specifications. Proceedings of the 15th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS \u201921), Krems, Austria.","DOI":"10.1145\/3442391.3442409"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"26721","DOI":"10.1109\/ACCESS.2019.2900473","article-title":"Toward Formal Modeling and Verification of Resource Provisioning as a Service in Cloud","volume":"7","author":"Zhou","year":"2019","journal-title":"IEEE Access"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"104653","DOI":"10.1016\/j.ic.2020.104653","article-title":"Dynamics of reputation in mobile agents systems and weighted timed automata","volume":"282","author":"Aman","year":"2022","journal-title":"Inf. Comput."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., and Vardi, M.Y. (1993, January 16\u201318). Parametric real-time reasoning. Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, San Diego, CA, USA.","DOI":"10.1145\/167088.167242"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Bundala, D., and Ouaknine, J. (2014, January 26\u201329). Advances in Parametric Real-Time Reasoning. Proceedings of the Mathematical Foundations of Computer Science 2014, Budapest, Hungary.","DOI":"10.1007\/978-3-662-44522-8_11"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/2362536.2362549","article-title":"Behavioural Modelling and Verification of Real-Time Software Product Lines","volume":"Volume 1","author":"Cordy","year":"2012","journal-title":"Proceedings of the 16th International Software Product Line Conference"},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1145\/3106195.3106204","article-title":"Modeling and Testing Product Lines with Unbounded Parametric Real-Time Constraints","volume":"Volume A","author":"Luthmann","year":"2017","journal-title":"Proceedings of the 21st International Systems and Software Product Line Conference (SPLC \u201917)"},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1016\/j.jss.2018.12.028","article-title":"Minimum\/maximum delay testing of product lines with unbounded parametric real-time constraints","volume":"149","author":"Luthmann","year":"2019","journal-title":"J. Syst. Softw."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"B\u00fcrdek, J., Lochau, M., Bauregger, S., Holzer, A., von Rhein, A., Apel, S., and Beyer, D. (2015, January 11\u201318). Facilitating Reuse in Multi-goal Test-Suite Generation for Software Product Lines. Proceedings of the Fundamental Approaches to Software Engineering, London, UK.","DOI":"10.1007\/978-3-662-46675-9_6"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"42","DOI":"10.4018\/ijertcs.2014070103","article-title":"RDTA: Recursive and Dynamic Timed Automata for Web Services Composition Analysis","volume":"5","author":"Latreche","year":"2014","journal-title":"Int. J. Embed.-Real-Time Commun. Syst. (IJERTCS)"},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Campana, S., Spalazzi, L., and Spegni, F. (2010, January 17\u201321). Dynamic Networks of Timed Automata for collaborative systems: A network monitoring case study. Proceedings of the 2010 International Symposium on Collaborative Technologies and Systems, Chicago, IL, USA.","DOI":"10.1109\/CTS.2010.5478517"},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1016\/j.ic.2016.03.008","article-title":"Dynamic input\/output automata: A formal and compositional model for dynamic systems","volume":"249","author":"Attie","year":"2016","journal-title":"Inf. Comput."},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Bettira, R., Kahloul, L., Khalgui, M., and Li, Z. (2019, January 6\u20139). Reconfigurable Hierarchical Timed Automata: Modeling and Stochastic Verification. Proceedings of the 2019 IEEE International Conference on Systems, Man and Cybernetics (SMC), Bari, Italy.","DOI":"10.1109\/SMC.2019.8913890"},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Bettira, R., Kahloul, L., and Khalgui, M. (2020, January 5\u20136). A Novel Approach for Repairing Reconfigurable Hierarchical Timed Automata. Proceedings of the 15th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2020), Online.","DOI":"10.5220\/0009408503980406"},{"key":"ref_40","doi-asserted-by":"crossref","unstructured":"Tigane, S., Kahloul, L., Baarir, S., and Bourekkache, S. (2020, January 18\u201320). Dynamic GSPNs: Formal Definition, Transformation towards GSPNs and Formal Verification. Proceedings of the 13th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS \u201920), Tsukuba, Japan.","DOI":"10.1145\/3388831.3388854"}],"container-title":["Axioms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2075-1680\/12\/3\/230\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T18:39:39Z","timestamp":1760121579000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2075-1680\/12\/3\/230"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,22]]},"references-count":40,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2023,3]]}},"alternative-id":["axioms12030230"],"URL":"https:\/\/doi.org\/10.3390\/axioms12030230","relation":{},"ISSN":["2075-1680"],"issn-type":[{"type":"electronic","value":"2075-1680"}],"subject":[],"published":{"date-parts":[[2023,2,22]]}}}