{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:16:13Z","timestamp":1760058973838,"version":"build-2065373602"},"reference-count":38,"publisher":"MDPI AG","issue":"5","license":[{"start":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T00:00:00Z","timestamp":1746748800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China (NSFC)","doi-asserted-by":"publisher","award":["52178307","2023YFC3107100","BK20210439"],"award-info":[{"award-number":["52178307","2023YFC3107100","BK20210439"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012166","name":"National Key R&amp;D Program of China (NKRDP)","doi-asserted-by":"publisher","award":["52178307","2023YFC3107100","BK20210439"],"award-info":[{"award-number":["52178307","2023YFC3107100","BK20210439"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004608","name":"Natural Science Foundation of Jiangsu Province","doi-asserted-by":"publisher","award":["52178307","2023YFC3107100","BK20210439"],"award-info":[{"award-number":["52178307","2023YFC3107100","BK20210439"]}],"id":[{"id":"10.13039\/501100004608","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>As building information model technologies become more complex and interconnected, the validation of building information models remains critical to ensure their reliability and effectiveness in practical applications. However, most of the existing research focuses on the application of building information modeling in a single domain and lacks the collaborative validation of the overall behavior of complex dynamic systems. Therefore, how to ensure the correctness and reliability of complex building systems has become a challenging issue. To solve this problem, this paper proposes a symmetry-aware hybrid validation framework that combines Timed Automata (TA), Unified Modeling Language (UML), and AnyLogic simulation to enhance the logical correctness and practical reliability of complex building information systems; the framework inherently preserves structural and temporal symmetry between formal models and dynamic simulations, ensuring consistent validation across virtual\u2013physical interactions. Taking the Building Information Physical Model (BIPM) as an example, the method first solves the defects of traditional methods in logical consistency and reliability validation by firstly modeling the structural model and behavioral logic of the BIPM through UML normalization, transforming the behavioral logic of the BIPM into a network of TA, and realizing the formal validation of its dynamic interaction mechanism to enhance the logical correctness and practical reliability of the complex building information system. Secondly, AnyLogic is used to map the BIPM structural model into a visual simulation model, which supports the real-time dynamic display of building system behavior and performance analysis, enhances the interpretability of the model, and provides an intuitive decision-making platform for stakeholders. Finally, an empirical study of an air conditioning system as a case study shows that the method can effectively integrate formal verification and dynamic visualization techniques, providing a scalable solution for the collaborative verification of complex building systems.<\/jats:p>","DOI":"10.3390\/sym17050726","type":"journal-article","created":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T06:18:51Z","timestamp":1746771531000},"page":"726","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symmetry-Aware Hybrid Verification for Complex Building Information Systems"],"prefix":"10.3390","volume":"17","author":[{"given":"Linlin","family":"Kong","sequence":"first","affiliation":[{"name":"College of Defense Engineering, Army Engineering University of PLA, Nanjing 210000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3274-2119","authenticated-orcid":false,"given":"Qiliang","family":"Yang","sequence":"additional","affiliation":[{"name":"College of Defense Engineering, Army Engineering University of PLA, Nanjing 210000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yaoqin","family":"Zhang","sequence":"additional","affiliation":[{"name":"Lei Hua Institute of Electronic Technology, Aviation Industry Corporation of China, Wuxi 214125, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuewei","family":"Zhang","sequence":"additional","affiliation":[{"name":"College of Defense Engineering, Army Engineering University of PLA, Nanjing 210000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5509-0902","authenticated-orcid":false,"given":"Qizhen","family":"Zhou","sequence":"additional","affiliation":[{"name":"College of Defense Engineering, Army Engineering University of PLA, Nanjing 210000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2025,5,9]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"2224995","DOI":"10.1080\/08839514.2023.2224995","article-title":"Advancing bridge construction monitoring: AI-based building information modeling for intelligent structural damage recognition","volume":"37","author":"Yang","year":"2023","journal-title":"Appl. Artif. Intell."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"103999","DOI":"10.1016\/j.jobe.2022.103999","article-title":"Embedding knowledge into BIM: A Case Study of Extending BIM with Firefighting Plans","volume":"49","author":"Kong","year":"2022","journal-title":"J. Build. Eng."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"107551","DOI":"10.1016\/j.jobe.2023.107551","article-title":"Application of Building Information Modeling-Blockchain Integration in the Architecture. Engineering, and Construction\/Facilities Management Industry: A review","volume":"77","author":"Zhang","year":"2023","journal-title":"J. Build. Eng."},{"key":"ref_4","unstructured":"Markets, R.A. (2024, October 02). Building Information Modeling (BIM)\u2014Global Strategic Business Report. Available online: https:\/\/www.researchandmarkets.com\/reports\/4804704\/building-information-modeling-bim-global#product--description."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1016\/j.autcon.2007.08.003","article-title":"Impact of three-dimensional parametric modeling of buildings on productivity in structural engineering practice","volume":"17","author":"Sacks","year":"2008","journal-title":"Automat. Constr."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1016\/j.ijproman.2012.12.001","article-title":"The project benefits of Building Information Modeling (BIM)","volume":"31","author":"Bryde","year":"2013","journal-title":"Int. J. Project. Manage"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1016\/j.autcon.2015.07.002","article-title":"Forgues, Measuring the impact of BIM on labor productivity in a small specialty contracting enterprise through action-research","volume":"58","author":"Poirier","year":"2015","journal-title":"Automat. Constr."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"102667","DOI":"10.1016\/j.rcim.2023.102667","article-title":"A multi-dimensional evolution modeling method for digital twin process model","volume":"86","author":"Liu","year":"2024","journal-title":"Robot. Comput.-Integr. Manuf."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"121827","DOI":"10.1016\/j.eswa.2023.121827","article-title":"Prioritization of transfer centers using GIS and fuzzy Dombi Bonferroni weighted Assessment (DOBAS) model","volume":"238","author":"Pamucar","year":"2024","journal-title":"Expert Syst. Appl."},{"key":"ref_10","first-page":"222","article-title":"Building Information and Physical Model (BIPM): A novel form of information description for buildings","volume":"25","author":"Yang","year":"2023","journal-title":"Strateg. Study Chin. Acad. Eng."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"103761","DOI":"10.1016\/j.advengsoft.2024.103761","article-title":"Formal modeling and validation of a novel building information model","volume":"197","author":"Kong","year":"2024","journal-title":"Adv. Eng. Softw."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"106409","DOI":"10.1016\/j.jobe.2023.106409","article-title":"BIM based framework for building evacuation using Bluetooth Low Energy and crowd simulation","volume":"70","author":"Elsayed","year":"2023","journal-title":"J. Build. Eng."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"124204","DOI":"10.1016\/j.eswa.2024.124204","article-title":"An intelligent BIM-enabled digital twin framework for real-time structural health monitoring using wireless IoT sensing, digital signal processing, and structural analysis","volume":"252","author":"Hu","year":"2024","journal-title":"Expert Syst. Appl."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"109022","DOI":"10.1016\/j.jobe.2024.109022","article-title":"BIM-based automated fault detection and diagnostics of HVAC systems in commercial buildings","volume":"87","author":"Gourabpasi","year":"2024","journal-title":"J. Build. Eng."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"109088","DOI":"10.1016\/j.cie.2023.109088","article-title":"Horizontal collaboration between suppliers to mitigate supply chain disruption: A secure resource sharing strategy","volume":"177","author":"Hosseinnezhad","year":"2023","journal-title":"Comput. Ind. Eng."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Khan, M.S., Park, J., and Seo, J. (2021). Geotechnical property modeling and construction safety zoning based on GIS and BIM integration. Appl. Sci., 11.","DOI":"10.3390\/app11094004"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"101837","DOI":"10.1016\/j.rcim.2019.101837","article-title":"Digital Twin-driven smart manufacturing: Connotation, reference model, applications and research issues","volume":"61","author":"Lu","year":"2020","journal-title":"Robot. Comput.-Integr. Manuf."},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Zhou, L., Lin, J., Li, Y., and Zhang, Z. (2020). Innovation diffusion of mobile applications in social networks: A multi-agent system. Sustainability, 12.","DOI":"10.3390\/su12072884"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Zhang, H., Li, J., Fei, Y., Deng, C., and Yi, J. (2023). Capacity assessment and analysis of vertiports based on simulation. Sustainability, 15.","DOI":"10.3390\/su151813377"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Guo, W., Chen, S., and Lei, M. (2023). Evolutionary game and strategy analysis of carbon emission reduction in supply chain based on system dynamic model. Sustainability, 15.","DOI":"10.3390\/su15118933"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"103551","DOI":"10.1016\/j.cities.2021.103551","article-title":"Smart city trends: A focus on 5 countries and 15 companies","volume":"123","author":"Kim","year":"2022","journal-title":"Cities"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Xu, J.D., Jiong, P., Cui, T.R., Zhang, S., Yang, Y., and Ren, T.L. (2023). Recent progress of tactile and force sensors for human-machine interaction. Sensors, 23.","DOI":"10.3390\/s23041868"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Jiao, Z.D., Du, X.L., Liu, Z.S., Liu, L., Sun, Z., Shi, G.L., and Liu, R.R. (2023). A review of theory and application development of intelligent operation methods for large public buildings. Sustainability, 15.","DOI":"10.3390\/su15129680"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"103527","DOI":"10.1016\/j.advengsoft.2023.103527","article-title":"Mixed reality and the Internet of Things: Bridging the virtual with the real","volume":"185","author":"Papadopoulos","year":"2023","journal-title":"Adv. Eng. Softw."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/s10626-023-00375-x","article-title":"Mixed nondeterministic-probabilistic automata","volume":"33","author":"Benveniste","year":"2023","journal-title":"Discret. Event Dyn. Syst."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1134\/S0361768823050079","article-title":"Automata-based software engineering with Event-B","volume":"49","author":"Shelekhov","year":"2023","journal-title":"Program. Comput. Softw."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"e1828","DOI":"10.1002\/stvr.1828","article-title":"Comprehensive evaluation of file systems robustness with SPIN model checking","volume":"32","author":"Yuan","year":"2022","journal-title":"Softw. Test. Verif. Reliab."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Grobelna, I., and Szcze\u015bniak, P. (2022). Model checking autonomous components within electric power systems specified by interpreted Petri nets. Sensors, 22.","DOI":"10.3390\/s22186936"},{"key":"ref_29","first-page":"6685978","article-title":"Formal modeling, proving, and model checking of a flood warning, monitoring, and rescue system-of-systems","volume":"2021","author":"Rehman","year":"2021","journal-title":"Sci. Program."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/s11219-021-09559-w","article-title":"Learning and analysis of sensors behavior in IoT systems using statistical model checking","volume":"30","author":"Chehida","year":"2022","journal-title":"Softw. Qual. J."},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Li, S.L., Yang, Q.L., Xing, J.C., Chen, W.J., and Zou, R.W. (2022). A Foundation model for building digital twins: A case study of a chiller. Buildings, 12.","DOI":"10.3390\/buildings12081079"},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"26358","DOI":"10.1109\/ACCESS.2023.3257171","article-title":"Security analysis of a digital twin framework using probabilistic model checking","volume":"11","author":"Shaikh","year":"2023","journal-title":"IEEE Access"},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"103699","DOI":"10.1016\/j.compind.2022.103699","article-title":"Towards situational aware cyber-physical systems: A security-enhancing use case of blockchain-based digital twins","volume":"141","author":"Suhail","year":"2022","journal-title":"Comput. Ind."},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3604610","article-title":"Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way","volume":"32","author":"Do","year":"2023","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"102928","DOI":"10.1016\/j.sysarc.2023.102928","article-title":"Compositional verification of embedded real-time systems","volume":"142","author":"Foughali","year":"2023","journal-title":"J. Syst. Archit."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"2090","DOI":"10.1016\/j.procs.2024.06.396","article-title":"Structured methodologies vs UML artifacts revisited: A perspective from a developing country","volume":"239","author":"Alkhatib","year":"2024","journal-title":"Procedia Comput. Sci."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1016\/j.procs.2022.09.108","article-title":"A bounded model checker for Timed Automata and its application to LTL properties","volume":"207","author":"Okano","year":"2022","journal-title":"Procedia Comput. Sci."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1016\/j.trpro.2023.02.065","article-title":"System modeling in solving mineral complex logistic problems with the anylogic software environment","volume":"68","author":"Afanasyev","year":"2023","journal-title":"Transp. Res. Procedia"}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/5\/726\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:29:58Z","timestamp":1760030998000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/5\/726"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,9]]},"references-count":38,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2025,5]]}},"alternative-id":["sym17050726"],"URL":"https:\/\/doi.org\/10.3390\/sym17050726","relation":{},"ISSN":["2073-8994"],"issn-type":[{"type":"electronic","value":"2073-8994"}],"subject":[],"published":{"date-parts":[[2025,5,9]]}}}