A Proposed Formal Verification Model for Card-controlled Doors Using PROMELA with SPIN Model Checker - Hassan, Bryar Ahmad; Qader, Shko Muhammed; Ezat, Hawkar Saeed; Ahmed , Hawkar Omar; Hamarashid, Hozan Khalid (The Scientific Journal of Cihan University– Sulaimaniya, 2022)
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.