A dual method to model ioT systems

This paper presents a dual method: 1) to specify both dynamic properties, such as operational requirements, and static properties, such as safety requirements, of IoT systems, whose services are distributed over a geographical space and are mobile over the space in time, and 2) verify the validation of the static properties over the dynamic properties. Firstly, the dynamic properties are specified with a process algebra, called δ-Calculus, and the static properties are specified a first-order logic, called GTS Logic. Secondly, once specifications are done, the static properties are verified for its validity over the dynamic properties. For example, safety requirements are verified to see its validity over operational requirements by checking whether or not the safety requirements are satisfied for all the possible simulation cases of the operational requirements. In order to demonstrate the feasibility of the method, a tool, namely SAVE, is developed on a meta-modeling platform, namely ADOxx. The method and the tool can be considered one of the most innovative approaches to model the IoT systems.