Formal Modeling with Verification of Smart Courtroom Building System (SMCBS) Using UML and TLA+ Specification
References
- R. S. Kumar, P. L. Pugalhanthi, N. Dhanyaa, V. Kaviyanjali, K. Dinesh, and K. Kathirvel, “IoT-based smart monitoring topologies for energy-efficient smart buildings,” in Modern Computational Techniques for Engineering Applications: CRC Press, 2024, pp. 79–106.
- E. Kamel, S. Habibi, and A. M. Memari, “State of the practice review of moisture management in residential buildings through sensors,” in Structures, 2024, vol. 59: Elsevier, p. 105698.
- M. Tunzi, T. Benakopoulos, Q. Yang, and S. Svendsen, “Demand side digitalisation: A methodology using heat cost allocators and energy meters to secure low-temperature operations in existing buildings connected to district heating networks,” Energy, vol. 264, p. 126272, 2023.
- G. Liu, H. Meng, G. Qu, L. Wang, L. Ren, and H. Lu, “Real-time monitoring and prediction method of commercial building fire temperature field based on distributed optical fiber sensor temperature measurement system,” Journal of Building Engineering, vol. 70, p. 106403, 2023.
- D. Wang, Y. Chen, W. Wang, C. Gao, and Z. Wang, “Field test of Model Predictive Control in residential buildings for utility cost savings,” Energy and Buildings, vol. 288, p. 113026, 2023.
- A. Dennis, B. Wixom, and D. Tegarden, Systems analysis and design: An object-oriented approach with UML. John wiley & sons, 2015.
- A. Clark and A. Evans, “Foundations of the Unified Modeling Language,” in Proceedigs of the 2nd Northern Formal Methods Workshop., 1997: Springer.
- É. André, S. Liu, Y. Liu, C. Choppy, J. Sun, and J. S. Dong, “Formalizing UML State Machines for Automated Verification–A Survey,” ACM Computing Surveys, 2023.
- C. Zhang, B. Li, T. N. Sainath, T. Strohman, and S.-y. Chang, “UML: A Universal Monolingual Output Layer For Multilingual Asr,” in ICASSP 2023-2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), 2023: IEEE, pp. 1–5.
- S. Tasiran, Y. Yu, B. Batson, and S. Kreider, “Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor,” in In Proceedings of the 3rd IEEE Workshop on Microprocessor Test and Verification, Common Challenges and Solutions, 2002.
- C. Newcombe, “Why amazon chose TLA+,” in International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014: Springer, pp. 25–39.
- C. Kern and M. R. Greenstreet, “Formal verification in hardware design: a survey,” ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 4, no. 2, pp. 123–193, 1999.
- V. Mascardi, M. Martelli, and L. Sterling, “Logic-based specification languages for intelligent software agents,” Theory and Practice of Logic Programming, vol. 4, no. 4, pp. 429–494, 2004.
- D. Bjørner and M. C. Henson, Logics of specification languages. Springer Science & Business Media, 2007.
- M. Krichen, “A survey on formal verification and validation techniques for internet of things,” Applied Sciences, vol. 13, no. 14, p. 8122, 2023.
- B. Andersson, D. de Niz, W. Vance, J. Ross, M. Wotell, and T. Bui, “Methodology of Combining Empirical Stress Testing and Formal-Methods Based Schedulability Analysis for Real-Time Multicore Software,” in 2023 IEEE/AIAA 42nd Digital Avionics Systems Conference (DASC), 2023: IEEE, pp. 1–10.
- J. C. Knight, “Safety critical systems: challenges and directions,” in Proceedings of the 24th international conference on software engineering, 2002, pp. 547–550.
- Z. Liu, X. Zhang, Y. Sun, and Y. Zhou, “Advanced controls on energy reliability, flexibility and occupant-centric control for smart and energy-efficient buildings,” Energy and Buildings, vol. 297, p. 113436, 2023/10/15/ 2023, doi:
https://doi.org/10.1016/j.enbuild.2023.113436 . - Z. Liu et al., “Incentive initiatives on energy-efficient renovation of existing buildings towards carbon–neutral blueprints in China: Advancements, challenges and prospects,” Energy and Buildings, vol. 296, p. 113343, 2023/10/01/ 2023, doi:
https://doi.org/10.1016/j.enbuild.2023.113343 . - D. Rodríguez-Gracia, M. d. l. M. Capobianco-Uriarte, E. Terán-Yépez, J. A. Piedra-Fernández, L. Iribarne, and R. Ayala, “Review of artificial intelligence techniques in green/smart buildings,” Sustainable Computing: Informatics and Systems, vol. 38, p. 100861, 2023/04/01/ 2023, doi:
https://doi.org/10.1016/j.suscom.2023.100861 . - A. A. Khan, M. A. Khan, K. Leung, X. Huang, M. Luo, and A. Usmani, “A review of critical fire event library for buildings and safety framework for smart firefighting,” International Journal of Disaster Risk Reduction, vol. 83, p. 103412, 2022/12/01/ 2022, doi:
https://doi.org/10.1016/j.ijdrr.2022.103412 . - Z. Liu et al., “A review of data-driven smart building-integrated photovoltaic systems: Challenges and objectives,” Energy, vol. 263, p. 126082, 2023/01/15/ 2023, doi:
https://doi.org/10.1016/j.energy.2022.126082 . - H. Xia, Z. Liu, M. Efremochkina, X. Liu, and C. Lin, “Study on city digital twin technologies for sustainable smart city design: A review and bibliometric analysis of geographic information system and building information modeling integration,” Sustainable Cities and Society, vol. 84, p. 104009, 2022/09/01/ 2022, doi:
https://doi.org/10.1016/j.scs.2022.104009 . - G. Pinto, Z. Wang, A. Roy, T. Hong, and A. Capozzoli, “Transfer learning for smart buildings: A critical review of algorithms, applications, and future perspectives,” Advances in Applied Energy, vol. 5, p. 100084, 2022/02/01/ 2022, doi:
https://doi.org/10.1016/j.adapen.2022.100084 . - R. Dwivedi, D. Mehrotra, and S. Chandra, “Potential of Internet of Medical Things (IoMT) applications in building a smart healthcare system: A systematic review,” Journal of Oral Biology and Craniofacial Research, vol. 12, no. 2, pp. 302–318, 2022/03/01/ 2022, doi:
https://doi.org/10.1016/j.jobcr.2021.11.010 . - G. F. Huseien and K. W. Shah, “A review on 5G technology for smart energy management and smart buildings in Singapore,” Energy and AI, vol. 7, p. 100116, 2022/01/01/ 2022, doi:
https://doi.org/10.1016/j.egyai.2021.100116 . - J. Aguilar, A. Garces-Jimenez, M. D. R-Moreno, and R. García, “A systematic literature review on the use of artificial intelligence in energy self-management in smart buildings,” Renewable and Sustainable Energy Reviews, vol. 151, p. 111530, 2021/11/01/ 2021, doi:
https://doi.org/10.1016/j.rser.2021.111530 . - A. Malagnino, T. Montanaro, M. Lazoi, I. Sergi, A. Corallo, and L. Patrono, “Building Information Modeling and Internet of Things integration for smart and sustainable environments: A review,” Journal of Cleaner Production, vol. 312, p. 127716, 2021/08/20/ 2021, doi:
https://doi.org/10.1016/j.jclepro.2021.127716 . - H. Stopps, B. Huchuk, M. F. Touchie, and W. O’Brien, “Is anyone home? A critical review of occupant-centric smart HVAC controls implementations in residential buildings,” Building and Environment, vol. 187, p. 107369, 2021/01/01/ 2021, doi:
https://doi.org/10.1016/j.buildenv.2020.107369 . - J. Al Dakheel, C. Del Pero, N. Aste, and F. Leonforte, “Smart buildings features and key performance indicators: A review,” Sustainable Cities and Society, vol. 61, p. 102328, 2020/10/01/ 2020, doi:
https://doi.org/10.1016/j.scs.2020.102328 . - B. Dong, V. Prakash, F. Feng, and Z. O’Neill, “A review of smart building sensing system for better indoor environment control,” Energy and Buildings, vol. 199, pp. 29–46, 2019/09/15/ 2019, doi:
https://doi.org/10.1016/j.enbuild.2019.06.025 . - M. Jia, A. Komeily, Y. Wang, and R. S. Srinivasan, “Adopting Internet of Things for the development of smart buildings: A review of enabling technologies and applications,” Automation in Construction, vol. 101, pp. 111–126, 2019/05/01/ 2019, doi:
https://doi.org/10.1016/j.autcon.2019.01.023 . - L. Lamport, “Specifying systems: the TLA+ language and tools for hardware and software engineers,” 2002.
- A. Rehman, S. Latif, and N. A. Zafar, “Formal modeling of smart office using activity diagram and non deterministic finite automata,” in 2019 International Conference on Information Science and Communication Technology (ICISCT), 2019: IEEE, pp. 1–5.
- S. Latif, A. Rehman, and N. A. Zafar, “Modeling of sewerage system linking UML, automata and TLA+,” in 2018 international conference on computing, electronic and electrical engineering (ICE Cube), 2018: IEEE, pp.1–6.
- R. Adner and D. Levinthal, “Demand heterogeneity and technology evolution: implications for product and process innovation,” Management science, vol. 47, no. 5, pp. 611–628, 2001.
- F. K. Santoso and N. C. Vun, “Securing IoT for smart home system,” in 2015 international symposium on consumer electronics (ISCE), 2015: IEEE, pp. 1–2.
- Z. Yu, Y. Liang, B. Xu, Y. Yang, and B. Guo, “Towards a smart campus with mobile social networking,” in 2011 International Conference on Internet of Things and 4th International Conference on Cyber, Physical and Social Computing, 2011: IEEE, pp. 162–169.
- K. Furdik, G. Lukac, T. Sabol, and P. Kostelnik, “The network architecture designed for an adaptable IoT-based smart office solution,” International Journal of Computer Networks and Communications Security, vol. 1, no. 6, pp. 216–224, 2013.
- Y. Geng and C. G. Cassandras, “New “smart parking” system based on resource allocation and reservations,” IEEE Transactions on intelligent transportation systems, vol. 14, no. 3, pp. 1129–1139, 2013.
- A. Zanella, N. Bui, A. Castellani, L. Vangelista, and M. Zorzi, “Internet of things for smart cities,” IEEE Internet of Things journal, vol. 1, no. 1, pp. 22–32, 2014.
- L. Pocero, D. Amaxilatis, G. Mylonas, and I. Chatzigiannakis, “Open source IoT meter devices for smart and energy-efficient school buildings,” HardwareX, vol. 1, pp. 54–67, 2017.
- D. Amaxilatis, I. Chatzigiannakis, and G. Mylonas, “Design and Implementation of a Platform for Smart Connected School Buildings,” in AmI (Workshops/Posters), 2015.
- Y. Qu, H. Wang, S.-M. Lun, H.-D. Chiang, and T. Wang, “Design and implementation of a Web-based Energy Management Application for smart buildings,” in 2013 IEEE Electrical Power & Energy Conference, 2013: IEEE, pp. 1–6.
- M. Brogan and A. Galata, “The Veryschool project: Valuable energy for a smart school-intelligent ISO 50001 energy management decision making in school buildings In Proceedings of the Special Tracks and Workshops at the 11th International Conference on Artificial Intelligence Applications and Innovations (AIAI 2015), Bayonne, France, September 14–17, 2015,” ed, 2015.
- B. Hirsch and J. W. Ng, “Education beyond the cloud: Anytime-anywhere learning in a smart campus environment,” in 2011 international conference for internet technology and secured transactions, 2011: IEEE, pp. 718–723.
- R. Huang, J. Zhang, Y. Hu, and J. Yang, “Smart campus: The developing trends of digital campus,” Open education research, vol. 4, no. 004, 2012.
- M. Veeramanickam and M. Mohanapriya, “Iot enabled futurus smart campus with effective e-learning: i-campus,” GSTF journal of Engineering Technology (JET), vol. 3, no. 4, pp. 8–87, 2016.
- G. Smith, The Object-Z specification language. Springer Science & Business Media, 2012.
- P. G. Larsen and W. Pawlowski, “The formal semantics of ISO VDM-SL,” Computer standards & interfaces, vol. 17, no. 5-6, pp. 585–601, 1995.
- D. Jackson, “Alloy: a lightweight object modelling notation,” ACM Transactions on software engineering and methodology (TOSEM), vol. 11, no. 2, pp. 256–290, 2002.
- S. Latif, A. Rehman, and N. A. Zafar, “NFA based formal modeling of smart parking system using TLA+,” in 2019 international conference on information science and communication technology (ICISCT), 2019: IEEE, pp. 1–6.
- T. De Champs, M. Ouenzar, B. Abdulrazak, M. Frappier, H. Pigot, and B. Fraikin, “Pervasive safety application with model checking in smart houses: The INOVUS intelligent oven,” in 2011 IEEE International Conference on Pervasive Computing and Communications Workshops (PERCOM Workshops), 2011: IEEE, pp. 630–635.
- E. Cohen et al., “VCC: A practical system for verifying concurrent C,” in Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17–20, 2009. Proceedings 22, 2009: Springer, pp. 23–42.
- K. Lano, The B language and method: a guide to practical formal development. Springer Science & Business Media, 2012.
- J.-R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta, and L. Voisin, “Rodin: an open toolset for modelling and reasoning in Event-B,” International journal on software tools for technology transfer, vol. 12, pp. 447–466, 2010.
- H. Koç, A. M. Erdoğan, Y. Barjakly, and S. Peker, “UML diagrams in software engineering research: a systematic literature review,” in Proceedings, 2021, vol. 74, no. 1: MDPI, p. 13.
- E. B. Purnama, N. Azizah, M. Nuraminudin, and M. M. Dewi, “Analysis and Design of Queue Service Information System Integrated with WhatsApp using UML Method,” International Journal of Computer and Information System (IJCIS), vol. 5, no. 1, pp. 1–7, 2024.
- E. M. Clarke, “Model checking,” in Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17, 1997: Springer, pp.54–56.
- Clarke, E. M, and Emerson, E. A. (1981, May). Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on logic of programs (pp. 52–71). Berlin, Heidelberg: Springer Berlin Heidelberg.
- C. Baier and J.-P. Katoen, Principles of model checking. MIT press, 2008.
- R. Jhala and R. Majumdar, “Software model checking,” ACM Computing Surveys (CSUR), vol. 41, no. 4, pp. 1–54, 2009.
- B. Bérard et al., Systems and software verification: model-checking techniques and tools. Springer Science & Business Media, 2013.
- I. Bouziane, H. Belmokadem, and M. Moussaoui, “A Review of Formal Security Verification of Common Internet of Things (IoT) Communication Protocols,” in 2023 7th IEEE Congress on Information Science and Technology (CiSt), 2023: IEEE, pp. 334–341.
- M. Shafiq, Z. Gu, O. Cheikhrouhou, W. Alhakami, and H. Hamam, “The rise of “Internet of Things”: review and open research issues related to detection and prevention of IoT-based security attacks,” Wireless Communications and Mobile Computing, vol. 2022, pp. 1–12, 2022.
- K. Hofer-Schmitz and B. Stojanović, “Towards formal verification of IoT protocols: A Review,” Computer Networks, vol. 174, p. 107233, 2020.
- A. Souri and M. Norouzi, “A state-of-the-art survey on formal verification of the internet of things applications,” Journal of Service Science Research, vol. 11, no. 1, pp. 47–67, 2019.
- J. Sun and Y. Liu, “Design of 360° Dead-Angle- Free Smart Desk Lamp based on Visual Tracking,” HighTech and Innovation Journal, vol. 4, no. 4, pp. 761–767, 2023.
- S. Amhaimedi, S. Naimi, and S. Alsallami, “Assessment of a decision-making model for monitoring the success of a project for smart buildings,” 2023.
- M. S. Sayeed, H. Abdulrahim, S. F. A. Razak, U. A. Bukar, and S. Yogarayan, “IoT Raspberry Pi Based Smart Parking System with Weighted K-Nearest Neighbours Approach,” Civil Engineering Journal, vol. 9, no. 8, pp. 1991–2011, 2023.
- C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon web services uses formal methods,” Communications of the ACM, vol. 58, no. 4, pp. 66–73, 2015.
- M. Nielsen, K. Havelund, K. R. Wagner, and C. George, “The RAISE language, method and tools,” Formal aspects of computing, vol. 1, pp. 85–114, 1989.
- N. Plat and P. G. Larsen, “An overview of the ISO/VDM-SL standard,” ACM Sigplan Notices, vol. 27, no. 8, pp. 76–82, 1992.
DOI: https://doi.org/10.2478/ijssis-2026-0016 | Journal eISSN: 1178-5608
Language: English
Submitted on: Jul 4, 2024
Published on: Mar 12, 2026
Published by: Macquarie University, Australia
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Keywords:
Related subjects:
© 2026 Shahbaz Ahmad, Nadeem Akhtar, Adeel Ahmad, Saima Abdulla, Saman Iftikhar, published by Macquarie University, Australia
This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.