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 the implementation of implementations. Well-known methods of verification of projects and implementations are based on the means of systemic, 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. This study presents the elements of technology and the steps of the behavioral verification methodology of functional level projects for Internet of things systems represented using Petri nets. General verification is represented by three stages

- the analysis of the correctness of the general structural and functional properties, the actual verification of inter-level and inter- component interactions, behavioral online and offline testing in the class of functional type errors. In the proposed analysis, the basic entities and relationships of the Internet of things systems are determined and verified architectural level, defining the structure, components, functions, interfaces, asynchronous-event interactions and represent elements of Petri nets - their positions, transitions, arcs, functions, markup. Online and offline testing for dynamic verification of the behavior of the Internet of things systems is carried out on the basis of, respectively, the background or special formation of many process threads in the Petri net, activated during its modeling and covering the Petri net objects. This paper presents general estimates of resource and time costs for the design of Internet of things systems without verification and with verification, showing their reduction in the event of design errors, redesign and application of verification. Verification is illustrated by the example of Petri nets simulating an automatic lighting system.