A support tool to design IoT services with NuSMV
Kazuya Nakahori, Shingo Yamaguchi · 2017
In this paper, we developed a support tool to design IoT services, and proposed a model checking method with NuSMV. Using our tool, we can model an IoT service as an agent-oriented Petri net PN2(Petri nets in a Petri net), and simulate its behavior. We also can exhaustively and automatically verify whether the given model meets a given specification. We also illustrated its usefulness with an application example of drone delivery system and considered its scalability.