Non-Deterministic Formal Modeling of Registration System towards Smart Campus

摘要

The intelligent management of all the processes of registration and administrative services are managed by smart campus. Smart campus provides management of clearance, transportation, departments, classrooms, offices, accounts, parking, notification and registration management system. Researchers have proposed many models to automate smart campus system using IoT, Mobile networking, cloud computing and machine learning techniques. But there is a need of more investigation of smart campus system modeling, validation and simulation. We have focused on Smart Registration system based on ubiquitous computing which is modeled using Unified Modeling Language (UML), Non-Deterministic Finite Automata (NFA) and Vienna Development Method Specification Language (VDM-SL). Registration system has many operations and functions to manage all the registration purpose tasks of the users, teachers and administration. The functions of the system include register, add or delete course, check, and view or delete Prerequisite, add or drop course, update, view or delete scheme of study. All the working of functions from one state to another is depicted in UML diagram. UML based model is further converted into Automata theory using NFA models to validate system states and transaction. The NFA based model is further converted into mathematical notations to provide proof of correctness of the model using VDM-SL. The specification is checked against the facilities available in VDM-SL to provide validation, verification and proof of correctness of proposed model.