Formal Verification of an IoT-Based Railway Gate System

In recent years, the continuous increase of the complexity of the Internet of Things systems including the interaction of enormous physical objects emerges new challenges especially, for critical systems where safety is a significant concern. The transportation industry, especially the railway system, is one such field where the IoT is significantly accelerating its rapidity of innovation. Accidents are more dangerous in terms of death rate. Therefore more efforts are necessary to improve safety. Consequently, this article presents the level crossing verification of typical railroads enhanced by Internet of Things systems as proposed by some papers in the literature. Furthermore, we prove formally that the above-motioned systems are not safe and can lead to a collision.