A Proposed Formal Verification Model for Card-controlled Doors Using PROMELA with SPIN Model Checker

Bryar Ahmad  Hassan; Shko Muhammed  Qader; Hawkar Saeed  Ezat; Hawkar Omar  Ahmed; Hozan Khalid  Hamarashid

doi:10.25098/6.1.30

Authors

Bryar Ahmad Hassan Department of Information Technology, Kurdistan Institution for Strategic Studies and Scientific Research, Sulaimani, Iraq
Shko Muhammed Qader Department of Information Technology, University College of Goizha, Sulaimani, Iraq , Information Technology Department, Computer Science Institute, Sulaimani Polytechnic University, Sulaymaniya, Iraq
Hawkar Saeed Ezat Department of Information Technology, Kurdistan Institution for Strategic Studies and Scientific Research, Sulaimani, Iraq
Hawkar Omar Ahmed Department of Information Technology, University College of Goizha, Sulaimani, Iraq, Department of Information Technology, College of Commerce, University of Sulaimani, Sulaimaniya, Iraq
Hozan Khalid Hamarashid Information Technology Department, Computer Science Institute, Sulaimani Polytechnic University, Sulaymaniya, Iraq

DOI:

https://doi.org/10.25098/6.1.30

Keywords:

Card-controlled doors, Formal verification, System verification, PROMELA, SPIN model checker

Abstract

One of the problems with the security building system is the use of card-controlled doors. When users are classified, card-controlled models provide them different access rights depending on their classification, allowing them to use just certain doors and not always in both directions. A formal verification of this system is needed in order to determine its validity. This is the process of demonstrating or disproving the correctness of a model in terms of a particular formal specification or feature. On the basis of this assumption, this study used the Protocol or Process Meta Language (PROMELA) in combination with SPIN to verify the features of the card-controlled model. Following an introduction to the model's requirements, this article provides a basic explanation of the model's assumptions as well as the definition of global variables. Following that, the variables are set to their original values. It is then explained in detail, along with a SPIN simulation, how case study 1 of the model is carried out, which includes the building of an underground structure fitted with a card-operated access system. Finally, job 2 is defined as a description and validation of the model's accuracy features, with the latter being the primary focus. Since the suggested model fulfils the requirements and can be applied to a wide range of building topologies, it has been deemed to be an optimal, generic, and parametric model for the management of building access.

References

R. Nardone et al., “Modeling railway control systems in Promela,” in International Workshop on Formal Techniques for Safety-Critical Systems, 2015, pp. 121–136.

S. Löffler and A. Serhrouchni, “Creating implementations from PROMELA models,” 1996.

D. J. C. A. P. Monteiro, “Coverage-based validation of embedded systems,” 2015.

H. E. H. Santoso, H. Saputra, A. Shofyan, K. Anam, and E. Supraptono, “The Use of RFID Sensors for Automatic Doorstop Application”.

A. Yacoub, M. E.-A. Hamri, and C. Frydman, “Using DEv-PROMELA for modelling and verification of software,” in Proceedings of the 2016 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, 2016, pp. 245–253.

Y. Choi, “Automated validation of IoT device control programs through domain-specific model generation,” in International Conference on Software Engineering and Formal Methods, 2018, pp. 254–268.

V. S. Burenkov and A. S. Kamkin, “Checking parameterized Promela models of cache coherence protocols,” Труды Института системного программирования РАН, vol. 28, no. 4, 2016.

N. Dilley and J. Lange, “Bounded verification of message-passing concurrency in Go using Promela and Spin,” arXiv preprint arXiv:2004.01323, 2020.

M. I. Abbasi and L. M. Mackenzie, “A Flexible Approach for Modelling and Analysis of Feature Interactions in Service-Oriented Product Lines.,” J. Softw., vol. 12, no. 10, pp. 823–830, 2017.

A. S. Alghamdi, “Features Interaction Detection and Resolution in Smart home systems Using Agent-Based Negotiation Approach,” 2015.

B. Vlaovič, A. Vreže, and Z. Brezočnik, “Applying automated model extraction for simulation and verification of real-life SDL specification with Spin,” IEEE Access, vol. 5, pp. 5046–5058, 2017.

Z. Soufiane, E.-N. Abdeslam, and B. Slimane, “An SDL to Discrete-Time PROMELA Transformation of Home Area Network model,” in Proceedings of the 12th International Conference on Intelligent Systems: Theories and Applications, 2018, pp. 1–5.

M. Dabaghchian and M. A. Azgomi, “Model checking the observational determinism security property using PROMELA and SPIN,” Formal Aspects of Computing, vol. 27, no. 5, pp. 789–804, 2015.

A. de Lucia, V. Deufemia, C. Gravino, and M. Risi, “Detecting the behavior of design patterns through model checking and dynamic analysis,” ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 26, no. 4, pp. 1–41, 2018.