Behavioral verification of internet of things systems by Petri nets

Abstract

The rapid development, implementation in all spheres of human activity and the growing responsibility of the functions of the Internet of things systems tighten and complicate the requirements for the reliability of their design decisions at the development stages and operability during their implementations. Well-known methods for verifying projects and implementations rely on the means of system, structural, functional, design and technological analysis and synthesis of Internet of things systems. However, their capabilities do not underestimate the feasibility of developing formalized models and verification methods, in particular, their integration at the early   system-functional stages, where “manual” design is inevitable and essential. This paper presents elements of a comprehensive behavioral verification of projects at the  system-functional level for Internet of Things systems represented using input UML diagrams and designed Petri nets. Verification includes at the first stage a “manual” system analysis of the correctness of entities and relationships for input UML diagrams and simple Petri nets, performed as their cover when activated in visual modeling. For this stage, general estimates of the costs of redesigning in case of errors are given. At the second stage in the verification of the system-functional level, an automated analysis of the correctness of more complex Petri nets corresponding to real objects is performed in the CPN Tools environment with modeling of their behavior and construction of a graph of reachable states (markups). In this case, the result allows the dynamics of the Petri net to evaluate the presence of dead ends, hanging peaks, endless cycles, safety and liveliness properties, and, if necessary, redesign. The combined integrated use of system “manual” and functional automated verification for input UML models and projected models of Petri nets allows reducing the time of designing Internet of things systems by eliminating or timely eliminating design errors