Formal Modeling with Verification of Smart Courtroom Building System (SMCBS) Using UML and TLA+ Specification

Shahbaz Ahmad; Nadeem Akhtar; Adeel Ahmad; Saima Abdulla; Saman Iftikhar

doi:10.2478/ijssis-2026-0016

.blurhash-client-img { display: none !important; }

Formal Modeling with Verification of Smart Courtroom Building System (SMCBS) Using UML and TLA+ Specification

International Journal on Smart Sensing and Intelligent Systems

Volume 19 (2026): Issue 1 (January 2026)

By: Shahbaz Ahmad, Nadeem Akhtar, Adeel Ahmad, Saima Abdulla and Saman Iftikhar

Open Access

|Mar 2026

Abstract

The growing trend of interconnected subsystems has brought significant interest in designing smart systems with the ability to build fully controlled attention upon them. Designing and verifying a smart building system presents unique challenges, including ensuring security for sensitive areas, managing diverse user access levels, and integrating multiple subsystems while maintaining system integrity and performance. There is also a need to work and focus on the goal of a smart, safe, and secure courtroom environment for all stakeholders, particularly in developing countries, such as Pakistan. There are also problems of security, safety, and energy saving in the infrastructure of the smart building systems. This study presents a proposed model for a secure, safe, and energy-saving courtroom building, and the model utilizes Unified Modeling Language (UML) diagrams to visualize the system’s components or objects and interaction sequences of actions. Additionally, formal methods are used, specifically Temporal Logic of Actions (TLA+), to write specifications as per the requirements of specifications and to rigorously verify the system’s properties to ensure its correctness. In the context of the smart courtroom building, security measures, such as password-protected entry, user access level, and safety, are implemented for the courtroom building. The system also manages building-wide lighting and temperature control while incorporating a subsystem of smoke detection to enhance safety during a fire in the courtroom. The model’s properties, such as correctness, are rigorously verified using the TLA+ toolbox and built-in Model Checker (TLC) after applying the specification as per the requirements of the infrastructure of a building. So, we have developed a novel integration of UML modeling and TLA+ specification for comprehensive system representation and verification. This is a robust set of formal specifications that address the unique security and functionality requirements of a courtroom environment. We have successfully verified the system properties using the TLC model checker, ensuring the correctness and safety of the proposed smart courtroom building system.

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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
A. Dennis, B. Wixom, and D. Tegarden, Systems analysis and design: An object-oriented approach with UML. John wiley & sons, 2015.
Search in Google Scholar Back to article
A. Clark and A. Evans, “Foundations of the Unified Modeling Language,” in Proceedigs of the 2nd Northern Formal Methods Workshop., 1997: Springer.
Search in Google Scholar Back to article
É. 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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
C. Newcombe, “Why amazon chose TLA+,” in International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014: Springer, pp. 25–39.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
D. Bjørner and M. C. Henson, Logics of specification languages. Springer Science & Business Media, 2007.
Search in Google Scholar Back to article
M. Krichen, “A survey on formal verification and validation techniques for internet of things,” Applied Sciences, vol. 13, no. 14, p. 8122, 2023.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
J. C. Knight, “Safety critical systems: challenges and directions,” in Proceedings of the 24th international conference on software engineering, 2002, pp. 547–550.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
L. Lamport, “Specifying systems: the TLA+ language and tools for hardware and software engineers,” 2002.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
D. Amaxilatis, I. Chatzigiannakis, and G. Mylonas, “Design and Implementation of a Platform for Smart Connected School Buildings,” in AmI (Workshops/Posters), 2015.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
G. Smith, The Object-Z specification language. Springer Science & Business Media, 2012.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
D. Jackson, “Alloy: a lightweight object modelling notation,” ACM Transactions on software engineering and methodology (TOSEM), vol. 11, no. 2, pp. 256–290, 2002.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
K. Lano, The B language and method: a guide to practical formal development. Springer Science & Business Media, 2012.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
C. Baier and J.-P. Katoen, Principles of model checking. MIT press, 2008.
Search in Google Scholar Back to article
R. Jhala and R. Majumdar, “Software model checking,” ACM Computing Surveys (CSUR), vol. 41, no. 4, pp. 1–54, 2009.
Search in Google Scholar Back to article
B. Bérard et al., Systems and software verification: model-checking techniques and tools. Springer Science & Business Media, 2013.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
K. Hofer-Schmitz and B. Stojanović, “Towards formal verification of IoT protocols: A Review,” Computer Networks, vol. 174, p. 107233, 2020.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
S. Amhaimedi, S. Naimi, and S. Alsallami, “Assessment of a decision-making model for monitoring the success of a project for smart buildings,” 2023.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.2478/ijssis-2026-0016 | Journal eISSN: 1178-5608

Journal RSS Feed

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:

TLA+,

UML,

Related subjects:

Introductions and overviews,

Engineering, other

© 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.

Volume 19 (2026): Issue 1 (January 2026)