Behavioral hidden testing of distributed information systems taking into account of energy

Abstract

The introduction of new energy-consuming properties for positions and transitions into the checked properties of the extended reference Petri net, for which the deviations of the tested Petri net are determined and a testing model is developed, provides new diagnostic possibilities. Keeping the class of checked properties in the composition of deviations of incidence relations, correspondences and marking functions of positions and transitions for the checked and reference Petri nets, the new properties make it possible to record the appearance of critical temperature regimes that are a consequence of errors or directly leading to their appearance. This versatility of testing helps to increase its completeness, accuracy and efficiency. The energy-heavy testing model is based on verification of incidence, correspondence, and markup functions. Checking the markup functions when generating events in positions, performing actions in transitions, as well as the proposed checking of the energy consumption indicators accumulated in the monitor tokens, is performed when checking the incidence, correspondences. The features of the testing model include the input of generalized energy-loaded Petri nets recorders, accumulating information about energy consumption in the behavior of positions/transitions, topological components and subnets, the entire Petri net in the process of its functioning. The testing model is also distinguished by the recognition of the reference energy-loaded behavior when checking the Petri net based on behavioral identification and coincidence of subsets of positions/transitions, the determination of behavior, the use of check primitives and transactions. The behavioral testing model defines the formal conditions for behavioral testing procedures, including the analysis of the correctness of energy consumption. The dimensionality of the testing model was estimated using the representation of Petri net graphs, special graphs of attainable states, including Rabin-Scott automata, using list structures. These estimates define the limits of applicability of the formal testing model