{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T08:30:56Z","timestamp":1777019456011,"version":"3.51.4"},"reference-count":38,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T00:00:00Z","timestamp":1773619200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems"],"abstract":"<jats:p>Cyber\u2013Physical Systems of Systems (CPSoS) integrate autonomous constituent systems to accomplish complex missions. Nonetheless, decentralized coordination and continuous evolution create intricate dependencies that make behavior difficult to analyze. Current semi-formal modeling approaches, despite being easy to understand and widely accessible, lack semantic precision and are not computationally checkable to guarantee time-critical properties. Furthermore, current formal methods are often fragmented: they analyze behavior either at the individual CPS level or the collective CPSoS level, failing to provide a multi-level specification. To address these limitations, we propose an integrated framework combining SysML and Maude rewriting logic. SysML provides structural and behavioral specification capabilities, while Maude enables rigorous semantics, executable models, and formal verification. First, our approach proposes MM-CPSoS, a meta-model that unifies CPS and CPSoS entities with explicit temporal constraints. Dynamic behavior is captured through evolution patterns governing mission progression across both levels. Then, we encode SysML models into Maude as object-oriented configurations and conditional rewrite rules, enabling linear temporal logic (LTL) model checking of temporal properties. Finally, we demonstrate our approach through a Time-Aware Road Crisis Management System (TaRCiMaS2).<\/jats:p>","DOI":"10.3390\/systems14030312","type":"journal-article","created":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T14:30:32Z","timestamp":1773671432000},"page":"312","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Modeling Framework for Time-Aware Cyber\u2013Physical Systems of Systems"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2689-5036","authenticated-orcid":false,"given":"Riad","family":"Helal","sequence":"first","affiliation":[{"name":"LIRE Laboratory, University of Constantine 2 Abdelhamid Mehri, Constantine 25000, Algeria"},{"name":"LIUPPA Laboratory, University of Pau, 64000 Pau, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4563-4061","authenticated-orcid":false,"given":"Faiza","family":"Belala","sequence":"additional","affiliation":[{"name":"LIRE Laboratory, University of Constantine 2 Abdelhamid Mehri, Constantine 25000, Algeria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3311-4146","authenticated-orcid":false,"given":"Nabil","family":"Hameurlain","sequence":"additional","affiliation":[{"name":"LIUPPA Laboratory, University of Pau, 64000 Pau, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1760-1932","authenticated-orcid":false,"given":"Akram","family":"Seghiri","sequence":"additional","affiliation":[{"name":"LIRE Laboratory, University of Constantine 2 Abdelhamid Mehri, Constantine 25000, Algeria"}]}],"member":"1968","published-online":{"date-parts":[[2026,3,16]]},"reference":[{"key":"ref_1","first-page":"161","article-title":"Cyber-physical systems","volume":"12","author":"Baheti","year":"2011","journal-title":"Impact Control Technol."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Jamaludin, J., and Rohani, J.M. (2018). Cyber-Physical System (CPS): State of the Art. Proceedings of the 2018 International Conference on Computing, Electronic and Electrical Engineering (ICE Cube), Quetta, Pakistan, 12\u201313 November 2018, IEEE.","DOI":"10.1109\/ICECUBE.2018.8610996"},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Rajkumar, R.R., Lee, I., Sha, L., and Stankovic, J. (2010). Cyber-physical systems: The next computing revolution. Proceedings of the 47th Design Automation Conference DAC\u201910, Anaheim, CA, USA, 13\u201318 June 2010, ACM.","DOI":"10.1145\/1837274.1837461"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1002\/(SICI)1520-6858(1998)1:4<267::AID-SYS3>3.0.CO;2-D","article-title":"Architecting principles for systems-of-systems","volume":"1","author":"Maier","year":"1998","journal-title":"Syst. Eng."},{"key":"ref_5","unstructured":"Friedenthal, S., Moore, A., and Steiner, R. (2014). A Practical Guide to SysML: The Systems Modeling Language, Morgan Kaufmann."},{"key":"ref_6","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., and Talcott, C. (2007). All About Maude\u2014A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic, Springer. Lecture Notes in Computer Science."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Younse, P. (2021). Comparative Analysis of Model-Based Systems Engineering and Traditional Systems Engineering Approaches for Architecting Robotic Space Systems through Knowledge Categorization, Automatic Information Transfer, and Automatic Knowledge Processing Measures. [Ph.D. Thesis, Colorado State University].","DOI":"10.1109\/ACCESS.2021.3096468"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Hossain, N.U.I., Lutfi, M., Ahmed, I., Akundi, A., and Cobb, D. (2022). Modeling and Analysis of Unmanned Aerial Vehicle System Leveraging Systems Modeling Language (SysML). Systems, 10.","DOI":"10.3390\/systems10060264"},{"key":"ref_9","first-page":"1","article-title":"Survey of model-based systems engineering (MBSE) methodologies","volume":"25","author":"Estefan","year":"2007","journal-title":"INCOSE MBSE Focus Group"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/s10270-019-00735-y","article-title":"Thirteen years of SysML: A systematic mapping study","volume":"19","author":"Wolny","year":"2019","journal-title":"Softw. Syst. Model."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Weilkiens, T. (2007). SysML\u2014The systems modeling language. Systems Engineering with SysML\/UML, Elsevier.","DOI":"10.1016\/B978-0-12-374274-2.00004-3"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"103363","DOI":"10.1016\/j.csi.2019.103363","article-title":"How are UML class diagrams built in practice? A usability study of two UML tools: MagicDraw and Papyrus","volume":"67","author":"Planas","year":"2020","journal-title":"Comput. Stand. Interfaces"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Lutfi, M., and Valerdi, R. (2025). Evaluating the Benefits and Drawbacks of Visualizing Systems Modeling Language (SysML) Diagrams in the 3D Virtual Reality Environment. Systems, 13.","DOI":"10.3390\/systems13040221"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"100497","DOI":"10.1016\/j.jlamp.2019.100497","article-title":"Programming and symbolic computation in Maude","volume":"110","author":"Eker","year":"2020","journal-title":"J. Log. Algebr. Methods Program."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Helal, R., Seghiri, A., Belala, F., and Hameurlain, N. (2024). Towards a Formal Modeling Approach for Cyber-Physical Systems Requirements. Proceedings of the 13th International Conference on Software and Computer Applications (ICSCA 2024), Bali Island, Indonesia, 1\u20133 February 2024, ACM.","DOI":"10.1145\/3651781.3651827"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Helal, R., Seghiri, A., Boukhelfa, K., Belala, F., and Hameurlain, N. (2024). FRAME-ArchSoS: A Model-based Framework for the Formal Specification of Reliable Systems of Systems. Proceedings of the 2024 International Conference on Advanced Aspects of Software Engineering (ICAASE), Constantine, Algeria, 9\u201310 November 2024, IEEE.","DOI":"10.1109\/ICAASE64542.2024.10850943"},{"key":"ref_18","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u0131-Oliet, N., Meseguer, J., Rubio, R., and Talcott, C. (2020). Maude Manual, SRI International. version 3.1."},{"key":"ref_19","unstructured":"Duran, F., Eker, S., Escobar, S., Meseguer, J., and Talcott, C. (June, January 30). Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6. Proceedings of the International Conference on Rewriting Techniques and Applications (RTA 2011), Novi Sad, Serbia."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/S1571-0661(05)82534-4","article-title":"The Maude LTL Model Checker","volume":"71","author":"Eker","year":"2004","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Gharib, M., Da Silva, L.D., Kavalionak, H., and Ceccarelli, A. (2018). A Model-Based Approach for Analyzing the Autonomy Levels for Cyber-Physical Systems-of-Systems. Proceedings of the 2018 Eighth Latin-American Symposium on Dependable Computing (LADC), Foz do Iguacu, Brazil, 8\u201310 October 2018, IEEE.","DOI":"10.1109\/LADC.2018.00024"},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/s13740-021-00129-8","article-title":"IQCPSoS: A Model-Based Approach for Modeling and Analyzing Information Quality Requirements for Cyber-Physical System-of-Systems","volume":"10","author":"Gharib","year":"2021","journal-title":"J. Data Semant."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Merino, J., Gomez, R., Posadas, H., and Villar, E. (2021). Modeling and Performance Estimation of Robotic Systems using ROS: Application to Drone-Based Services. Proceedings of the 2021 Forum on Specification & Design Languages (FDL), Antibes, France, 8\u201310 September 2021, IEEE.","DOI":"10.1109\/FDL53530.2021.9568374"},{"key":"ref_24","unstructured":"Mansfield, M. (2019). A Systematic Approach to Model-Based Engineering of Cyber-Physical Systems of Systems. [Ph.D. Thesis, Newcastle University]."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1049\/iet-sen.2018.5034","article-title":"Modelling and Verifying Time-Aware Processes for Cyber-Physical Environments","volume":"13","author":"Graja","year":"2019","journal-title":"IET Softw."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Graja, I., Kallel, S., Guermouche, N., and Kacem, A.H. (2018). Verification of the Consistency of Time-Aware Cyber-Physical Processes. Service-Oriented Computing\u2014ICSOC 2017 Workshops, Springer. Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-319-91764-1_6"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"20211","DOI":"10.48084\/etasr.9646","article-title":"A Multidimensional Approach for Formal Modeling and Analyzing Medical Cyber-Physical Systems","volume":"15","author":"Bouheroum","year":"2025","journal-title":"Eng. Technol. Appl. Sci. Res."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Zhang, L. (2018, January 19\u201323). Specification and Design of Cyber Physical Systems Based on System of Systems Engineering Approach. Proceedings of the 17th International Symposium on Distributed Computing and Applications for Business Engineering and Science (DCABES), Wuxi, China.","DOI":"10.1109\/DCABES.2018.00084"},{"key":"ref_29","unstructured":"Zhan, B., Xu, X., Gao, Q., Ji, Z., Jin, X., Wang, S., and Zhan, N. (2024). Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems. arXiv."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1007\/s10009-022-00665-z","article-title":"Modeling and Formal Analysis of Virtually Synchronous Cyber-Physical Systems in AADL","volume":"24","author":"Lee","year":"2022","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1007\/s10009-025-00831-z","article-title":"MR-HybridSynchAADL: Formal modeling and analysis of multirate CPSs with advanced control programs and continuous dynamics","volume":"27","author":"Lee","year":"2025","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_32","first-page":"22","article-title":"MLTL Multi-Type: A Typed Logic for Cyber-Physical Systems","volume":"25","author":"Hariharan","year":"2024","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Bujorianu, M.L. (2024). Cyber-Physical Ecosystems: Modelling and Verification. Proceedings of the Engineering of Computer-Based Systems, Springer.","DOI":"10.1007\/978-3-031-49252-5_17"},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Khosrowjerdi, H., and Meinke, K. (2018). Learning-Based Testing for Autonomous Systems Using Spatial and Temporal Requirements. Proceedings of the 1st International Workshop on Machine Learning and Software Engineering in Symbiosis (MaLTeS), ACM.","DOI":"10.1145\/3243127.3243129"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"92733","DOI":"10.1109\/ACCESS.2024.3422660","article-title":"A Method for Building Trustworthy Hybrid Performance Models for Cyber-Physical Systems of Systems","volume":"12","author":"Modaber","year":"2024","journal-title":"IEEE Access"},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Wilson, K., Arafat, A.A., Baugh, J., Yu, R., Liu, X., and Guo, Z. (2025). Soteria: A Formal Digital-Twin-Enabled Framework for Safety-Assurance of Latency-Aware Cyber-Physical Systems. Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control, Irvine, CA, USA, 6\u20139 May 2025, ACM.","DOI":"10.1145\/3716863.3718028"},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Helal, R., Boukhelfa, K., Seghiri, A., Hameurlain, N., and Belala, F. (2025). Towards Specification and Analysis of Dependable Cyber-Physical Systems. Model and Data Engineering; Lecture Notes in Computer Science, Springer.","DOI":"10.1007\/978-3-031-87719-3_5"},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1145\/182.358434","article-title":"Maintaining knowledge about temporal intervals","volume":"26","author":"Allen","year":"1983","journal-title":"Commun. ACM"}],"container-title":["Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2079-8954\/14\/3\/312\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T05:11:44Z","timestamp":1773897104000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2079-8954\/14\/3\/312"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,16]]},"references-count":38,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2026,3]]}},"alternative-id":["systems14030312"],"URL":"https:\/\/doi.org\/10.3390\/systems14030312","relation":{},"ISSN":["2079-8954"],"issn-type":[{"value":"2079-8954","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,16]]}}}