Formal Verification and Validation of IoT-based Railway Gate Controlling System at Level Crossing
- Resource Type
- Conference
- Authors
- Rashid, Muhammad; Qadeer, Muhammad; Raza, Husnain; Shabir, Ifra; Rasool, Imran; Zafar, Nazir Ahmad
- Source
- 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC) Humanitarian Technology Conference (KHI-HTC), 2024 IEEE 1st Karachi Section. :1-6 Jan, 2024
- Subject
- Bioengineering
Communication, Networking and Broadcast Technologies
Computing and Processing
Engineering Profession
General Topics for Engineers
Geoscience
Power, Energy and Industry Applications
Robotics and Control Systems
Signal Processing and Analysis
System verification
Unified modeling language
Logic gates
Control systems
Software systems
Rail transportation
Safety
Model Checking
Formal Methods
Spin
LTL
Railway Level Crossing
Internet of Things
- Language
The safety of railway level crossing is one of the major and foremost issues of railway traffic. Accidents related to railway level crossing led to a great loss of human life and major financial losses. To prevent these fatal circumstances safety of the gate control system at level crossing must be checked. Safety can be ensured by verifying correctness of systems handling gates at level crossing. A lot of research exists related to ensuring correctness using different formal verification tools but no one tried to ensure the safety of railway level crossing using the SPIN model checker. This study provides a solution to this problem by formally verifying the system by using SPIN. In this work, formal specification of the automatic gate control system using the formal specification language, i.e., Process or Protocol Meta Language (PROMELA). Create a program graph for this process through the SPIN Model checker and describe safety and liveness properties using linear temporal logic (LTL) in the form of a formula. The formal verification is performed to ensure correctness by giving the program graph and LTL formulas as input to the SPIN model checker to check whether the properties are satisfied with the program graph.