Formal verification of a UPPAALbased garage control system

Abstract

One of our society's major issues is citizen insecurity. Many homes currently lack a control system that allows them to operate an automatic garage door. Liftgate automation raises the issue of access security and system control. Because an intruder can corrupt the system and gain access to it. In other cases, opening and closing the door can result in an accident. Faced with this challenge, the goal is to create and test a system with formal specifications for controlling and accessing automatic sliding doors using UPPAAL. This system aims to ensure the system's proper operation and the safety of the environment that surrounds the sliding doors.