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