SAVE/GTS-VLT: Visual logic tool for geo-temporal specification and verification of safety requirements in smart IoT systems

Visual representation for operational requirements for Smart IoT Systems is desirable in process algebra, since it is more intuitive than textual representation. Further visual representation for safety requirements in the systems is more desirable in real-time logic since it reduces the complexity of verification of the requirements. However it is not well known that there are common logics for such visualization. In that purpose, this paper presents a visual logic, called GTS Visual Logic, to specify and verify the geo-temporal safety requirements for Smart IoT Systems specified with a process algebra, called dT-Calculus. The calculus is used to specify the operational requirements for the systems on some conceptual geographical space. Once they are specified, a set of simulations can be performed to construct all possible execution cases for the requirements, and a set of outputs are produced in terms of processes, their actions and interactions, and dependencies on the 2-dimentional geo-temporal space. Then the visual logic is used to specify and verify all the safety requirements for the systems in terms of dependencies, especially precedencies and conditions, among all the processes, their independent actions and synchronous interactions. For feasibility, a tool, called GTS-VLT, was developed on ADOxx as a basic component of the SAVE tool suite, which is the tool set to model Smart IoT Systems, in order to demonstrate the feasibility of the logic.