Safety Property Analysis of Service-Oriented IoT Based on Interval Timed Coloured Petri Nets
V. Phartchayanusit, Songsakdi Rongviriyapanish · 2018
In recent years, the number of Internet of Things (IoT) systems has been increasing. Through design and analysis, IoT systems can be verified and monitored. However, it is difficult to find safety property with general-use models which we are familiar with such as UML model. In this paper, we proposed safety property analysis of service-oriented IoT based on Interval timed coloured Petri Nets (ITCPN). We model IoT design with StateMate which is easy to use and is similar to UML diagram. Then, transforming this diagram to ITCPN model which can be analysed and verified by model checking with Linear Temporal Logic (LTL). We also illustrated the usefulness of our approach with an example of infusion Pump.