Smart City Gnosys
Smart city article details
| Title | Nfa Based Formal Modeling Of Smart Parking System Using Tla + |
|---|---|
| ID_Doc | 39245 |
| Authors | Latif S.; Rehman A.; Zafar N.A. |
| Year | 2019 |
| Published | 2019 International Conference on Information Science and Communication Technology, ICISCT 2019 |
| DOI | http://dx.doi.org/10.1109/CISCT.2019.8777445 |
| Abstract | The smart objects are used to sense, communicate, send and to share information within a network. Everything which is connected directly or indirectly within a network for the sake of getting, analyze or interpreting data known as IoT. There are many proposed applications of IoT infrastructure in smart city. We have proposed model of smart parking system in this paper which is based on UML, automata-based model and formal methods. The depiction of real-world parking system is done in UML based models to indicate the flow and working of the system. Automata models are used to convert UML diagram into automated system which provides smart mechanism of parking system. Automated model of automata is represented in terms of states and transitions. Every state has unique identity and defined functionality. There are many operations of parking system which are modeled in this paper including find free spaces, search shortest path towards empty slot, car entrance and exit with in a region. A region is an area of parking system which is automated and use to sense a vehicle, car entrance, exit or to find a location. The formal method techniques are used to formally verify system properties using available facilities available in formal method tools. We have used Temporal Logic of Actions (TLA+) formal language to validate and verify system properties using formal techniques. TLA+ is mathematical based notation to describe a system using discrete mathematics concepts. We have integrated these three approaches to model parking system from depiction side, automation side and from the angle of verification and validation of the model. © 2019 IEEE. |
| Author Keywords | Formal methods; Parking; TLC; UML; Verification and validation |
Similar Articles
| Id | Similarity | Authors | Title | Published |
|---|---|---|---|---|
26920  | 0.935 | Jameel F.; Zafar N.A.; Tehseen A. | Formal Specification Ensuring Security At Entrance And Exit Of Smart Parking System | 3rd International Conference on Communication Technologies, ComTech 2021 (2021) |
| 26910 | 0.893 | Jameel F.; Zafar N.A. | Formal Modeling And Automation Of E-Payment Smart Parking System | 2021 International Conference on Digital Futures and Transformative Technologies, ICoDT2 2021 (2021) |
| 26903 | 0.872 | Roig P.J.; Alcaraz S.; Gilly K.; Filiposka S.; Aknin N. | Formal Algebraic Modelling Of A City-Wide Smart Parking System | 2nd International Conference on Electrical, Communication and Computer Engineering, ICECCE 2020 (2020) |
| 37586 | 0.865 | Latif S.; Rehman A.; Zafar N.A. | Modeling Of Sewerage System Linking Uml, Automata And Tla+ | 2018 International Conference on Computing, Electronic and Electrical Engineering, ICE Cube 2018 (2019) |
| 18888 | 0.854 | Keote M.L.; Ghodeswar U.S.; Gathibandhe B.; Khodankar S.; Shende A.; Zilpilwar T. | Design Of Mathematical Model And Implementation Of Iot Enabled Smart Secure Parking System | Communications on Applied Nonlinear Analysis, 31, 2S (2024) |